fof(t36_rfunct_3,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( m1_subset_1(B,A) => ! [C] : ( m2_finseq_1(C,k4_rfunct_3(A,k1_numbers)) => ( r1_rfunct_3(A,k1_numbers,C,B) => k2_seq_1(A,k1_numbers,k15_rfunct_3(A,C),B) = k15_rvsum_1(k18_rfunct_3(A,C,B)) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d4_subset_1,t32_finseq_1,t21_rfunct_3,t13_funcop_1,d8_rfunct_3,t32_finseq_1,t102_rvsum_1,t29_nat_1,t80_finseq_1,d8_rfunct_3,d3_finseq_1,t38_nat_1,t27_finseq_3,t13_finseq_2,t20_rfinseq,t23_rfunct_3,d9_rfunct_3,t57_finseq_1,d8_rfunct_3,t57_finseq_1,t27_finseq_3,t4_finseq_1,d1_tarski,d8_rfunct_3,t57_finseq_1,t10_finseq_2,t22_rfunct_3,t103_rvsum_1,t29_rfunct_3,t31_rfunct_3,d3_xboole_0,d3_seq_1,d8_rfunct_3,d3_seq_1,t32_rfunct_3,t104_rvsum_1,t20_rfinseq,s1_nat_1]), [file(rfunct_3,t36_rfunct_3),interesting(1.00)]). fof(t76_rfunct_3,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( ( v1_funct_1(B) & m2_relset_1(B,A,k1_numbers) ) => ! [C] : ( m1_subset_1(C,k1_numbers) => ! [D,E] : ( v1_finset_1(E) => ( E = k4_relset_1(A,k1_numbers,k2_partfun1(A,k1_numbers,B,D)) => k22_rfunct_3(A,k21_rfunct_3(A,B,C),D) = k7_rvsum_1(k22_rfunct_3(A,B,D),k4_finseqop(k1_numbers,k4_card_1(E),C)) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t59_card_2,t66_rfunct_3,t71_rfunct_3,t49_rvsum_1,t68_funct_1,d12_rfunct_3,t68_funct_1,t66_rfunct_3,t71_rfunct_3,t68_funct_1,d12_rfunct_3,t68_funct_1,d14_rfunct_3,t1_rfinseq,t38_nat_1,t70_rfunct_3,t27_finseq_3,d5_funct_1,t26_partfun1,t68_funct_1,t75_rfunct_3,t73_rfunct_3,t20_rfinseq,t46_finseq_1,t68_funct_1,t20_rfinseq,t33_rfinseq,t69_rfunct_3,t2_rfinseq,t14_rfinseq,t36_rfinseq,t68_funct_1,t37_zfmisc_1,d3_tarski,d3_xboole_0,d4_xboole_0,d3_xboole_0,d4_xboole_0,d10_xboole_0,d3_tarski,d4_xboole_0,d3_xboole_0,d4_xboole_0,d3_xboole_0,t16_finset_1,t63_card_2,t79_card_1,d3_xboole_0,d12_rfunct_3,t50_rvsum_1,t69_finseq_2,t70_rfunct_3,d6_rvsum_1,t86_finseq_2,t86_finseq_2,t57_finseq_1,d6_rvsum_1,t86_finseq_2,t35_finseq_1,d3_finseq_1,t6_finseq_1,d3_finseq_1,t3_finseq_1,t38_nat_1,d3_finseq_1,t70_finseq_2,d3_finseq_1,t37_finseq_1,t47_rvsum_1,t47_rvsum_1,t3_finseq_1,d5_real_1,t38_nat_1,t3_finseq_1,d7_finseq_1,t70_finseq_2,t2_xreal_1,t29_nat_1,t3_finseq_1,t70_finseq_2,t19_rfinseq,d3_finseq_1,d3_finseq_1,t47_rvsum_1,t47_rvsum_1,t10_finseq_2,s1_nat_1]), [file(rfunct_3,t76_rfunct_3),interesting(0.91)]). fof(t28_rfunct_3,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( m2_finseq_1(B,k4_rfunct_3(A,k1_numbers)) => ! [C] : ( m2_finseq_1(C,k4_rfunct_3(A,k1_numbers)) => ( r1_rfinseq(B,C) => k15_rfunct_3(A,B) = k15_rfunct_3(A,C) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t32_finseq_1,t16_rfinseq,t32_finseq_1,t1_rfinseq,t16_rfinseq,t38_nat_1,t27_finseq_3,t13_finseq_2,d5_funct_1,t11_finseq_2,t21_rfinseq,t27_finseq_3,t4_finseq_2,t5_finseq_2,t80_finseq_1,t3_finseq_1,t19_rfinseq,t20_rfinseq,t29_nat_1,t7_finseq_1,d15_finseq_1,d15_finseq_1,t100_relat_1,t28_xboole_1,d15_finseq_1,t29_nat_1,t80_finseq_1,t20_rfinseq,d1_rfinseq,t63_finseq_3,t63_finseq_3,t63_finseq_3,t63_finseq_3,d1_rfinseq,t24_rfunct_3,t24_rfunct_3,t19_rfunct_1,t24_rfunct_3,t24_rfunct_3,s1_nat_1]), [file(rfunct_3,t28_rfunct_3),interesting(0.89)]). fof(t83_rfunct_3,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( ( v1_funct_1(B) & m2_relset_1(B,A,k1_numbers) ) => ! [C,D] : ( m1_subset_1(D,k1_numbers) => ! [E] : ( v1_finset_1(E) => ( E = k4_relset_1(A,k1_numbers,k2_partfun1(A,k1_numbers,B,C)) => k24_rfunct_3(A,k21_rfunct_3(A,B,D),C) = k5_real_1(k24_rfunct_3(A,B,C),k4_real_1(D,k4_card_1(E))) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t76_rfunct_3,t70_rfunct_3,t69_finseq_2,t110_finseq_2,t120_rvsum_1,t110_rvsum_1]), [file(rfunct_3,t83_rfunct_3),interesting(0.85)]). fof(t79_rfunct_3,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( ( v1_funct_1(B) & m2_relset_1(B,A,k1_numbers) ) => ! [C,D] : ( ( v1_finset_1(k4_relset_1(A,k1_numbers,k2_partfun1(A,k1_numbers,B,k2_xboole_0(C,D)))) & r1_xboole_0(C,D) ) => r1_rfinseq(k22_rfunct_3(A,B,k2_xboole_0(C,D)),k8_finseq_1(k1_numbers,k22_rfunct_3(A,B,C),k22_rfunct_3(A,B,D))) ) ) ) ), inference(mizar_proof,[status(thm)],[t7_xboole_1,t104_relat_1,t25_relat_1,t13_finset_1,t68_funct_1,t23_xboole_1,t68_funct_1,t68_funct_1,t7_xboole_1,t13_finset_1,t59_card_2,t66_rfunct_3,t66_rfunct_3,t47_finseq_1,t71_rfunct_3,t66_rfunct_3,t68_funct_1,t23_xboole_1,t68_funct_1,t68_funct_1,t47_card_1,d3_tarski,t36_xboole_1,t13_xboole_1,t27_xboole_1,t68_funct_1,t68_funct_1,t13_finset_1,t27_xboole_1,t3_xboole_1,t47_card_1,t37_zfmisc_1,t68_funct_1,d3_tarski,d3_xboole_0,d4_xboole_0,d3_xboole_0,d4_xboole_0,d10_xboole_0,d3_tarski,d4_xboole_0,d3_xboole_0,d4_xboole_0,d3_xboole_0,t16_finset_1,t63_card_2,t79_card_1,t14_rfinseq,t45_finseq_1,t69_rfunct_3,t47_card_1,d14_rfunct_3,t2_rfinseq,t14_rfinseq,t15_rfinseq,t2_rfinseq,t2_rfinseq,t2_rfinseq,t47_card_1,d3_xboole_0,d3_xboole_0,t65_zfmisc_1,t42_xboole_1,t47_card_1,d2_xboole_0,t69_rfunct_3,d14_rfunct_3,t2_rfinseq,t2_rfinseq,s1_nat_1,d7_xboole_0]), [file(rfunct_3,t79_rfunct_3),interesting(0.75)]). fof(t21_rfunct_3,theorem,( ! [A] : ( ~ v1_xboole_0(A) => k15_rfunct_3(A,k6_finseq_1(k4_rfunct_3(A,k1_numbers))) = k5_rfunct_3(A,k1_numbers,k2_subset_1(A),0) ) ), inference(mizar_proof,[status(thm)],[t16_rfunct_3,t17_rfunct_3,t19_rfunct_3,t20_rfunct_3,t11_finsop_1]), [file(rfunct_3,t21_rfunct_3),interesting(0.74)]). fof(t31_rfunct_3,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( m1_subset_1(B,A) => ! [C] : ( m2_finseq_1(C,k4_rfunct_3(A,k1_numbers)) => ( k3_finseq_1(C) != 0 => ( r1_rfunct_3(A,k1_numbers,C,B) <=> r2_hidden(B,k4_relset_1(A,k1_numbers,k15_rfunct_3(A,C))) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d3_finseq_1,t27_finseq_3,t13_finseq_2,t57_finseq_1,t22_rfunct_3,d9_rfunct_3,t4_finseq_1,d1_tarski,d9_rfunct_3,t38_nat_1,t29_nat_1,t80_finseq_1,t27_finseq_3,t38_nat_1,t27_finseq_3,t13_finseq_2,t20_rfinseq,t23_rfunct_3,t29_rfunct_3,d9_rfunct_3,d3_xboole_0,d3_seq_1,d3_seq_1,d3_xboole_0,t27_finseq_3,d3_xboole_0,d5_real_1,t38_nat_1,t3_finseq_1,d3_finseq_1,t19_rfinseq,d9_rfunct_3,d9_rfunct_3,s1_nat_1]), [file(rfunct_3,t31_rfunct_3),interesting(0.72)]). fof(t62_rfunct_3,theorem,( ! [A] : ( ( v1_funct_1(A) & m2_relset_1(A,k1_numbers,k1_numbers) ) => ! [B,C] : ( m1_subset_1(C,k1_numbers) => ( r2_rfunct_3(A,B) => r2_rfunct_3(k19_rfunct_3(k1_numbers,k21_rfunct_3(k1_numbers,A,C)),B) ) ) ) ), inference(mizar_proof,[status(thm)],[d12_rfunct_3,d10_rfunct_3,d13_rfunct_3,d13_rfunct_3,d13_rfunct_3,t11_xreal_1,t7_rfunct_3,d13_rfunct_3,d12_rfunct_3,d12_rfunct_3,t5_rfunct_3,t21_xreal_1,t4_rfunct_3,t2_xreal_1,d12_rfunct_3,d10_rfunct_3,d10_rfunct_3,d10_rfunct_3]), [file(rfunct_3,t62_rfunct_3),interesting(0.69)]). fof(t63_rfunct_3,theorem,( ! [A] : ( ( v1_funct_1(A) & m2_relset_1(A,k1_numbers,k1_numbers) ) => ! [B] : ( r2_rfunct_3(A,B) => r2_rfunct_3(k19_rfunct_3(k1_numbers,A),B) ) ) ), inference(mizar_proof,[status(thm)],[t62_rfunct_3,t51_rfunct_3]), [file(rfunct_3,t63_rfunct_3),interesting(0.68)]). fof(t2_rfunct_3,theorem,( ! [A] : ( v1_xreal_0(A) => k18_complex1(A) = k3_real_1(k2_rfunct_3(A),k3_rfunct_3(A)) ) ), inference(mizar_proof,[status(thm)],[d2_square_1,t26_xreal_1,d2_square_1,d1_absvalue,d2_square_1,t60_xreal_1,d2_square_1,d1_absvalue]), [file(rfunct_3,t2_rfunct_3),interesting(0.66)]). fof(t86_rfunct_3,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( ( v1_funct_1(B) & m2_relset_1(B,A,k1_numbers) ) => ! [C,D] : ( ( v1_finset_1(k4_relset_1(A,k1_numbers,k2_partfun1(A,k1_numbers,B,k2_xboole_0(C,D)))) & r1_xboole_0(C,D) ) => k24_rfunct_3(A,B,k2_xboole_0(C,D)) = k3_real_1(k24_rfunct_3(A,B,C),k24_rfunct_3(A,B,D)) ) ) ) ), inference(mizar_proof,[status(thm)],[t79_rfunct_3,t22_rfinseq,t105_rvsum_1]), [file(rfunct_3,t86_rfunct_3),interesting(0.66)]). fof(t1_rfunct_3,theorem,( ! [A] : ( v1_xreal_0(A) => A = k5_real_1(k2_rfunct_3(A),k3_rfunct_3(A)) ) ), inference(mizar_proof,[status(thm)],[d2_square_1,t26_xreal_1,d2_square_1,d2_square_1,t60_xreal_1,d2_square_1]), [file(rfunct_3,t1_rfunct_3),interesting(0.65)]). fof(t7_rfunct_3,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ! [C] : ( v1_xreal_0(C) => ! [D] : ( v1_xreal_0(D) => ( ( r1_xreal_0(A,C) & r1_xreal_0(B,D) ) => r1_xreal_0(k2_square_1(A,B),k2_square_1(C,D)) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t46_square_1,t2_xreal_1,t50_square_1]), [file(rfunct_3,t7_rfunct_3),interesting(0.65)]). fof(t5_rfunct_3,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => r1_xreal_0(k2_rfunct_3(k2_xcmplx_0(A,B)),k3_real_1(k2_rfunct_3(A),k2_rfunct_3(B))) ) ) ), inference(mizar_proof,[status(thm)],[t46_square_1,d2_square_1,t9_xreal_1,d2_square_1,t9_xreal_1]), [file(rfunct_3,t5_rfunct_3),interesting(0.65)]). fof(t51_rfunct_3,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( ( v1_funct_1(B) & m2_relset_1(B,A,k1_numbers) ) => k21_rfunct_3(A,B,0) = B ) ) ), inference(mizar_proof,[status(thm)],[d12_rfunct_3,d12_rfunct_3,t34_partfun1]), [file(rfunct_3,t51_rfunct_3),interesting(0.65)]). fof(t4_rfunct_3,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ( r1_xreal_0(0,A) => k2_rfunct_3(k3_xcmplx_0(A,B)) = k3_xcmplx_0(A,k2_rfunct_3(B)) ) ) ) ), inference(mizar_proof,[status(thm)],[t129_xreal_1,d2_square_1,d2_square_1,t133_xreal_1,d2_square_1]), [file(rfunct_3,t4_rfunct_3),interesting(0.64)]). fof(t64_rfunct_3,theorem,( r2_rfunct_3(k1_partfun2(k1_numbers,k2_subset_1(k1_numbers)),k1_numbers) ), inference(mizar_proof,[status(thm)],[d4_subset_1,t34_funct_1,d13_rfunct_3,t34_funct_1]), [file(rfunct_3,t64_rfunct_3),interesting(0.64)]). fof(t18_rfunct_3,theorem,( ! [A] : ( ~ v1_xboole_0(A) => r3_binop_1(k4_rfunct_3(A,k1_numbers),k5_rfunct_3(A,k1_numbers,k2_subset_1(A),0),k14_rfunct_3(A)) ) ), inference(mizar_proof,[status(thm)],[d4_subset_1,t19_funcop_1,t16_rfunct_3,t28_xboole_1,d3_seq_1,d3_seq_1,t13_funcop_1,t34_partfun1,d4_rfunct_3,t13_binop_1]), [file(rfunct_3,t18_rfunct_3),interesting(0.62)]). fof(t20_rfunct_3,theorem,( ! [A] : ( ~ v1_xboole_0(A) => v1_setwiseo(k14_rfunct_3(A),k4_rfunct_3(A,k1_numbers)) ) ), inference(mizar_proof,[status(thm)],[d2_setwiseo,t18_rfunct_3]), [file(rfunct_3,t20_rfunct_3),interesting(0.62)]). fof(t19_rfunct_3,theorem,( ! [A] : ( ~ v1_xboole_0(A) => k3_binop_1(k4_rfunct_3(A,k1_numbers),k14_rfunct_3(A)) = k5_rfunct_3(A,k1_numbers,k2_subset_1(A),0) ) ), inference(mizar_proof,[status(thm)],[t18_rfunct_3,d8_binop_1]), [file(rfunct_3,t19_rfunct_3),interesting(0.62)]). fof(t16_rfunct_3,theorem,( ! [A] : ( ~ v1_xboole_0(A) => v1_binop_1(k14_rfunct_3(A),k4_rfunct_3(A,k1_numbers)) ) ), inference(mizar_proof,[status(thm)],[d13_binop_1,d4_rfunct_3,d4_rfunct_3]), [file(rfunct_3,t16_rfunct_3),interesting(0.61)]). fof(t80_rfunct_3,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( ( v1_funct_1(B) & m2_relset_1(B,A,k1_numbers) ) => ! [C,D] : ( m1_subset_1(D,k1_numbers) => ( v1_finset_1(k4_relset_1(A,k1_numbers,k2_partfun1(A,k1_numbers,B,C))) => k24_rfunct_3(A,k13_seq_1(A,k1_numbers,B,D),C) = k4_real_1(D,k24_rfunct_3(A,B,C)) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t29_finset_1,t18_rfinseq,t68_funct_1,t100_relat_1,t97_relat_1,t76_funct_1,t1_rfinseq,d4_finseq_1,d14_rfunct_3,t2_rfinseq,t22_rfinseq,t68_funct_1,d6_seq_1,t68_funct_1,t1_rfinseq,t65_rfunct_1,d6_seq_1,t29_finset_1,d7_rvsum_1,t37_finseq_2,l11_rfunct_3,t65_rfunct_1,t26_partfun1,d6_seq_1,d5_funct_1,t11_finseq_2,t31_finseq_3,t66_rvsum_1,d5_funct_1,l11_rfunct_3,t11_finseq_2,t66_rvsum_1,t38_rfinseq,t9_rfunct_3,t65_rfunct_1,t10_rfinseq,t37_rfinseq,t65_rfunct_1,t8_rfunct_3,t11_rfinseq,t11_rfinseq,d14_rfunct_3,t2_rfinseq,t22_rfinseq,t117_rvsum_1]), [file(rfunct_3,t80_rfunct_3),interesting(0.61)]). fof(t17_rfunct_3,theorem,( ! [A] : ( ~ v1_xboole_0(A) => v2_binop_1(k14_rfunct_3(A),k4_rfunct_3(A,k1_numbers)) ) ), inference(mizar_proof,[status(thm)],[d14_binop_1,d4_rfunct_3,d4_rfunct_3,t19_rfunct_1,d4_rfunct_3,d4_rfunct_3]), [file(rfunct_3,t17_rfunct_3),interesting(0.60)]). fof(t71_rfunct_3,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( ( v1_funct_1(B) & m2_relset_1(B,A,k1_numbers) ) => k22_rfunct_3(A,B,k1_xboole_0) = k6_finseq_1(k1_numbers) ) ) ), inference(mizar_proof,[status(thm)],[t68_funct_1,t70_rfunct_3,t78_card_1,t32_finseq_1]), [file(rfunct_3,t71_rfunct_3),interesting(0.59)]). fof(t47_rfunct_3,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( ( v1_funct_1(B) & m2_relset_1(B,A,k1_numbers) ) => ! [C] : k2_partfun1(A,k1_numbers,k19_rfunct_3(A,B),C) = k19_rfunct_3(A,k2_partfun1(A,k1_numbers,B,C)) ) ) ), inference(mizar_proof,[status(thm)],[t68_funct_1,d10_rfunct_3,t68_funct_1,d10_rfunct_3,d3_xboole_0,t68_funct_1,d10_rfunct_3,t68_funct_1,d10_rfunct_3,t34_partfun1]), [file(rfunct_3,t47_rfunct_3),interesting(0.58)]). fof(t33_rfunct_3,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( ( v1_relat_1(B) & v1_funct_1(B) & v1_finseq_1(B) ) => ! [C] : ( m1_subset_1(C,A) => r1_rfunct_3(A,k1_numbers,k16_rfunct_3(A,B),C) ) ) ) ), inference(mizar_proof,[status(thm)],[d9_rfunct_3,d6_rfunct_3,t77_rfunct_1]), [file(rfunct_3,t33_rfunct_3),interesting(0.57)]). fof(t3_rfunct_3,theorem,( ! [A] : ( v1_xreal_0(A) => k4_real_1(2,k2_rfunct_3(A)) = k2_xcmplx_0(A,k18_complex1(A)) ) ), inference(mizar_proof,[status(thm)],[t1_rfunct_3,t2_rfunct_3]), [file(rfunct_3,t3_rfunct_3),interesting(0.56)]). fof(l11_rfunct_3,theorem,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) ) => ! [B] : ( ~ r2_hidden(B,k2_relat_1(A)) => k10_relat_1(A,k1_tarski(B)) = k1_xboole_0 ) ) ), inference(mizar_proof,[status(thm)],[d7_xboole_0,d3_xboole_0,d1_tarski,t173_relat_1]), [file(rfunct_3,l11_rfunct_3),interesting(0.56)]). fof(t65_rfunct_3,theorem,( ! [A] : ( m1_subset_1(A,k1_numbers) => r2_rfunct_3(k19_rfunct_3(k1_numbers,k21_rfunct_3(k1_numbers,k1_partfun2(k1_numbers,k2_subset_1(k1_numbers)),A)),k1_numbers) ) ), inference(mizar_proof,[status(thm)],[t62_rfunct_3,t64_rfunct_3]), [file(rfunct_3,t65_rfunct_3),interesting(0.55)]). fof(t34_rfunct_3,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( m1_subset_1(B,A) => ! [C] : ( m2_finseq_1(C,k4_rfunct_3(A,k1_numbers)) => ! [D] : ( m2_finseq_1(D,k1_numbers) => ( r1_rfunct_3(A,k1_numbers,C,B) => r1_rfunct_3(A,k1_numbers,k17_rfunct_3(A,C,D),B) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d9_rfunct_3,t35_square_1,d7_rfunct_3,t27_finseq_3,t2_xreal_1,t27_finseq_3,t13_finseq_2,d7_rfunct_3,d9_rfunct_3,d6_seq_1]), [file(rfunct_3,t34_rfunct_3),interesting(0.54)]). fof(t81_rfunct_3,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( ( v1_funct_1(B) & m2_relset_1(B,A,k1_numbers) ) => ! [C] : ( ( v1_funct_1(C) & m2_relset_1(C,A,k1_numbers) ) => ! [D,E] : ( v1_finset_1(E) => ( ( E = k4_relset_1(A,k1_numbers,k2_partfun1(A,k1_numbers,B,D)) & k4_relset_1(A,k1_numbers,k2_partfun1(A,k1_numbers,B,D)) = k4_relset_1(A,k1_numbers,k2_partfun1(A,k1_numbers,C,D)) ) => k24_rfunct_3(A,k6_seq_1(A,k1_numbers,B,C),D) = k3_real_1(k24_rfunct_3(A,B,D),k24_rfunct_3(A,C,D)) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t59_card_2,t65_relat_1,d14_rfunct_3,t1_rfinseq,t27_finseq_1,t102_rvsum_1,d14_rfunct_3,t1_rfinseq,t27_finseq_1,t102_rvsum_1,t60_rfunct_1,d3_seq_1,t59_card_2,t65_relat_1,d14_rfunct_3,t1_rfinseq,t27_finseq_1,t102_rvsum_1,t47_card_1,d3_tarski,t47_card_1,t68_funct_1,t37_zfmisc_1,t47_card_1,d3_xboole_0,d3_xboole_0,t37_zfmisc_1,d3_seq_1,d3_xboole_0,t68_funct_1,t60_rfunct_1,d3_seq_1,d3_tarski,d3_xboole_0,d4_xboole_0,d3_xboole_0,d4_xboole_0,d10_xboole_0,d3_tarski,d4_xboole_0,d3_xboole_0,d4_xboole_0,d3_xboole_0,t63_card_2,t79_card_1,d3_tarski,d3_xboole_0,d4_xboole_0,d3_xboole_0,d3_xboole_0,d3_xboole_0,d10_xboole_0,d3_tarski,d3_xboole_0,d4_xboole_0,d3_xboole_0,d3_xboole_0,d3_xboole_0,t69_rfunct_3,t47_card_1,d14_rfunct_3,t2_rfinseq,t22_rfinseq,t104_rvsum_1,t69_rfunct_3,t47_card_1,d14_rfunct_3,t2_rfinseq,t69_rfunct_3,d14_rfunct_3,t2_rfinseq,t22_rfinseq,t104_rvsum_1,d3_seq_1,t104_rvsum_1,t22_rfinseq,s1_nat_1]), [file(rfunct_3,t81_rfunct_3),interesting(0.52)]). fof(t44_rfunct_3,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( ~ v1_xboole_0(B) => ! [C] : ( ( v1_funct_1(C) & m2_relset_1(C,A,k1_numbers) ) => ! [D] : ( ( v1_funct_1(D) & m2_relset_1(D,B,k1_numbers) ) => ( r1_rfinseq(C,D) => r1_rfinseq(k19_rfunct_3(A,C),k19_rfunct_3(B,D)) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d10_rfunct_3,t38_rfunct_3,t5_rfinseq,t39_rfunct_3,t4_rfinseq,t26_partfun1,t40_rfunct_3,l11_rfunct_3,t26_partfun1,t40_rfunct_3,l11_rfunct_3,t5_rfinseq]), [file(rfunct_3,t44_rfunct_3),interesting(0.51)]). fof(t45_rfunct_3,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( ~ v1_xboole_0(B) => ! [C] : ( ( v1_funct_1(C) & m2_relset_1(C,A,k1_numbers) ) => ! [D] : ( ( v1_funct_1(D) & m2_relset_1(D,B,k1_numbers) ) => ( r1_rfinseq(C,D) => r1_rfinseq(k20_rfunct_3(A,C),k20_rfunct_3(B,D)) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d11_rfunct_3,t41_rfunct_3,t5_rfinseq,t42_rfunct_3,t4_rfinseq,t26_partfun1,t43_rfunct_3,l11_rfunct_3,t26_partfun1,t43_rfunct_3,l11_rfunct_3,t5_rfinseq]), [file(rfunct_3,t45_rfunct_3),interesting(0.51)]). fof(t87_rfunct_3,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( ( v1_funct_1(B) & m2_relset_1(B,A,k1_numbers) ) => ! [C,D] : ( ( v1_finset_1(k4_relset_1(A,k1_numbers,k2_partfun1(A,k1_numbers,B,k2_xboole_0(C,D)))) & r1_xboole_0(k4_relset_1(A,k1_numbers,k2_partfun1(A,k1_numbers,B,C)),k4_relset_1(A,k1_numbers,k2_partfun1(A,k1_numbers,B,D))) ) => k24_rfunct_3(A,B,k2_xboole_0(C,D)) = k3_real_1(k24_rfunct_3(A,B,C),k24_rfunct_3(A,B,D)) ) ) ) ), inference(mizar_proof,[status(thm)],[t68_funct_1,t23_xboole_1,t68_funct_1,t68_funct_1,t7_xboole_1,t13_finset_1,t66_rfunct_3,t68_funct_1,t68_funct_1,t16_xboole_1,t68_funct_1,t79_rfunct_3,t22_rfinseq,t105_rvsum_1]), [file(rfunct_3,t87_rfunct_3),interesting(0.51)]). fof(t29_rfunct_3,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( ~ v1_xboole_0(B) => ! [C] : ( m2_finseq_1(C,k4_rfunct_3(A,B)) => ! [D] : ( m1_subset_1(D,A) => ! [E] : ( m2_subset_1(E,k1_numbers,k5_numbers) => ( r1_rfunct_3(A,B,C,D) => ( E = 0 | r1_rfunct_3(A,B,k16_finseq_1(k4_rfunct_3(A,B),C,E),D) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d9_rfunct_3,l10_rfunct_3,d9_rfunct_3,t80_finseq_1,d3_finseq_1,t38_nat_1,t27_finseq_3,t19_rfinseq,d9_rfunct_3]), [file(rfunct_3,t29_rfunct_3),interesting(0.50)]). fof(t57_rfunct_3,theorem,( ! [A] : ( ( v1_funct_1(A) & m2_relset_1(A,k1_numbers,k1_numbers) ) => ! [B,C] : ( ( r2_rfunct_3(A,B) & r1_tarski(C,B) ) => r2_rfunct_3(A,C) ) ) ), inference(mizar_proof,[status(thm)],[d13_rfunct_3,t1_xboole_1,d13_rfunct_3,d13_rfunct_3]), [file(rfunct_3,t57_rfunct_3),interesting(0.49)]). fof(t49_rfunct_3,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( ( v1_funct_1(B) & m2_relset_1(B,A,k1_numbers) ) => ( ! [C] : ( m1_subset_1(C,A) => ( r2_hidden(C,k4_relset_1(A,k1_numbers,B)) => r1_xreal_0(0,k2_seq_1(A,k1_numbers,B,C)) ) ) => k19_rfunct_3(A,B) = B ) ) ) ), inference(mizar_proof,[status(thm)],[d10_rfunct_3,d10_rfunct_3,d2_square_1,t34_partfun1]), [file(rfunct_3,t49_rfunct_3),interesting(0.47)]). fof(t84_rfunct_3,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( ( v1_funct_1(B) & m2_relset_1(B,A,k1_numbers) ) => k24_rfunct_3(A,B,k1_xboole_0) = 0 ) ) ), inference(mizar_proof,[status(thm)],[t71_rfunct_3,t102_rvsum_1]), [file(rfunct_3,t84_rfunct_3),interesting(0.47)]). fof(t40_rfunct_3,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( ( v1_funct_1(B) & m2_relset_1(B,A,k1_numbers) ) => ! [C] : ( m1_subset_1(C,A) => ( r2_hidden(C,k4_relset_1(A,k1_numbers,B)) => r1_xreal_0(0,k2_seq_1(A,k1_numbers,k19_rfunct_3(A,B),C)) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d10_rfunct_3,d10_rfunct_3,t46_square_1]), [file(rfunct_3,t40_rfunct_3),interesting(0.45)]). fof(t43_rfunct_3,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( ( v1_funct_1(B) & m2_relset_1(B,A,k1_numbers) ) => ! [C] : ( m1_subset_1(C,A) => ( r2_hidden(C,k4_relset_1(A,k1_numbers,B)) => r1_xreal_0(0,k2_seq_1(A,k1_numbers,k20_rfunct_3(A,B),C)) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d11_rfunct_3,d11_rfunct_3,t46_square_1]), [file(rfunct_3,t43_rfunct_3),interesting(0.45)]). fof(t58_rfunct_3,theorem,( ! [A] : ( ( v1_funct_1(A) & m2_relset_1(A,k1_numbers,k1_numbers) ) => ! [B,C] : ( m1_subset_1(C,k1_numbers) => ( r2_rfunct_3(A,B) <=> r2_rfunct_3(k21_rfunct_3(k1_numbers,A,C),B) ) ) ) ), inference(mizar_proof,[status(thm)],[d12_rfunct_3,d13_rfunct_3,d13_rfunct_3,d13_rfunct_3,t11_xreal_1,d12_rfunct_3,d12_rfunct_3,d12_rfunct_3,d12_rfunct_3,d13_rfunct_3,d13_rfunct_3,d13_rfunct_3,d12_rfunct_3,d12_rfunct_3,d12_rfunct_3,t11_xreal_1]), [file(rfunct_3,t58_rfunct_3),interesting(0.45)]). fof(t67_rfunct_3,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( ( v1_funct_1(B) & m2_relset_1(B,A,k1_numbers) ) => ! [C] : ( v1_finset_1(k4_relset_1(A,k1_numbers,k2_partfun1(A,k1_numbers,B,C))) => k22_rfunct_3(A,k2_partfun1(A,k1_numbers,B,C),C) = k22_rfunct_3(A,B,C) ) ) ) ), inference(mizar_proof,[status(thm)],[d14_rfunct_3,t101_relat_1,d14_rfunct_3]), [file(rfunct_3,t67_rfunct_3),interesting(0.45)]). fof(t35_rfunct_3,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( ( v1_relat_1(B) & v1_funct_1(B) & v1_finseq_1(B) ) => ! [C] : ( m2_finseq_1(C,k1_numbers) => ! [D] : ( m1_subset_1(D,A) => r1_rfunct_3(A,k1_numbers,k17_rfunct_3(A,k16_rfunct_3(A,B),C),D) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t33_rfunct_3,t34_rfunct_3]), [file(rfunct_3,t35_rfunct_3),interesting(0.44)]). fof(t74_rfunct_3,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( ( v1_funct_1(B) & m2_relset_1(B,A,k1_numbers) ) => ! [C,D] : ( ( v1_finset_1(k4_relset_1(A,k1_numbers,k2_partfun1(A,k1_numbers,B,C))) & r1_tarski(D,C) & ! [E] : ( m1_subset_1(E,A) => ! [F] : ( m1_subset_1(F,A) => ( ( r2_hidden(E,k4_relset_1(A,k1_numbers,k2_partfun1(A,k1_numbers,B,D))) & r2_hidden(F,k4_relset_1(A,k1_numbers,k2_partfun1(A,k1_numbers,B,k4_xboole_0(C,D)))) ) => r1_xreal_0(k2_seq_1(A,k1_numbers,B,F),k2_seq_1(A,k1_numbers,B,E)) ) ) ) ) => k22_rfunct_3(A,B,C) = k8_finseq_1(k1_numbers,k22_rfunct_3(A,B,D),k22_rfunct_3(A,B,k4_xboole_0(C,D))) ) ) ) ), inference(mizar_proof,[status(thm)],[s1_nat_1,l90_rfunct_3,l91_rfunct_3,t104_relat_1,t25_relat_1,t13_finset_1]), [file(rfunct_3,t74_rfunct_3),interesting(0.44)]). fof(t70_rfunct_3,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( ( v1_funct_1(B) & m2_relset_1(B,A,k1_numbers) ) => ! [C,D] : ( v1_finset_1(D) => ( D = k4_relset_1(A,k1_numbers,k2_partfun1(A,k1_numbers,B,C)) => k3_finseq_1(k22_rfunct_3(A,B,C)) = k4_card_1(D) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t29_finset_1,d14_rfunct_3,d3_finseq_1,t10_rfinseq,t78_finseq_1]), [file(rfunct_3,t70_rfunct_3),interesting(0.43)]). fof(t15_rfunct_3,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( ~ v1_xboole_0(B) => ! [C] : ( ( v1_funct_1(C) & m2_relset_1(C,A,k1_numbers) ) => ! [D] : ( ( v1_funct_1(D) & m2_relset_1(D,B,k1_numbers) ) => ( r1_rfinseq(C,D) => r1_rfinseq(k21_seq_1(A,k1_numbers,C),k21_seq_1(B,k1_numbers,D)) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t10_rfunct_3,t4_rfinseq,t11_rfunct_3,t4_rfinseq,t12_rfunct_3,t5_rfinseq]), [file(rfunct_3,t15_rfunct_3),interesting(0.42)]). fof(t14_rfunct_3,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( ~ v1_xboole_0(B) => ! [C] : ( ( v1_funct_1(C) & m2_relset_1(C,A,k1_numbers) ) => ! [D] : ( ( v1_funct_1(D) & m2_relset_1(D,B,k1_numbers) ) => ( r1_rfinseq(C,D) <=> r1_rfinseq(k16_seq_1(A,k1_numbers,C),k16_seq_1(B,k1_numbers,D)) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t38_rfunct_1,t13_rfunct_3]), [file(rfunct_3,t14_rfunct_3),interesting(0.41)]). fof(l10_rfunct_3,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( ~ v1_xboole_0(B) => ! [C] : ( m2_finseq_1(C,B) => ( r1_xreal_0(k3_finseq_1(C),A) => k16_finseq_1(B,C,A) = C ) ) ) ) ), inference(mizar_proof,[status(thm)],[d3_finseq_1,d15_finseq_1,t7_finseq_1,t97_relat_1]), [file(rfunct_3,l10_rfunct_3),interesting(0.41)]). fof(t48_rfunct_3,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( ( v1_funct_1(B) & m2_relset_1(B,A,k1_numbers) ) => ! [C] : k2_partfun1(A,k1_numbers,k20_rfunct_3(A,B),C) = k20_rfunct_3(A,k2_partfun1(A,k1_numbers,B,C)) ) ) ), inference(mizar_proof,[status(thm)],[t68_funct_1,d11_rfunct_3,t68_funct_1,d11_rfunct_3,d3_xboole_0,t68_funct_1,d11_rfunct_3,t68_funct_1,d11_rfunct_3,t34_partfun1]), [file(rfunct_3,t48_rfunct_3),interesting(0.41)]). fof(t54_rfunct_3,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( ~ v1_xboole_0(B) => ! [C] : ( ( v1_funct_1(C) & m2_relset_1(C,A,k1_numbers) ) => ! [D] : ( ( v1_funct_1(D) & m2_relset_1(D,B,k1_numbers) ) => ! [E] : ( m1_subset_1(E,k1_numbers) => ( r1_rfinseq(C,D) <=> r1_rfinseq(k21_rfunct_3(A,C,E),k21_rfunct_3(B,D,E)) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t53_rfunct_3,t5_rfinseq,t53_rfunct_3,t5_rfinseq,t53_rfunct_3,t5_rfinseq,t53_rfunct_3,t5_rfinseq]), [file(rfunct_3,t54_rfunct_3),interesting(0.41)]). fof(t22_rfunct_3,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( m2_rfunct_3(B,A,k1_numbers,k4_rfunct_3(A,k1_numbers)) => k15_rfunct_3(A,k12_finseq_1(k4_rfunct_3(A,k1_numbers),B)) = B ) ) ), inference(mizar_proof,[status(thm)],[t12_finsop_1]), [file(rfunct_3,t22_rfunct_3),interesting(0.40)]). fof(t6_rfunct_3,theorem,( ! [A] : ( v1_xreal_0(A) => ( r1_xreal_0(0,k2_rfunct_3(A)) & r1_xreal_0(0,k3_rfunct_3(A)) ) ) ), inference(mizar_proof,[status(thm)],[t46_square_1]), [file(rfunct_3,t6_rfunct_3),interesting(0.40)]). fof(t52_rfunct_3,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( ( v1_funct_1(B) & m2_relset_1(B,A,k1_numbers) ) => ! [C] : ( m1_subset_1(C,k1_numbers) => ! [D] : k21_rfunct_3(A,k2_partfun1(A,k1_numbers,B,D),C) = k2_partfun1(A,k1_numbers,k21_rfunct_3(A,B,C),D) ) ) ) ), inference(mizar_proof,[status(thm)],[d12_rfunct_3,t68_funct_1,d12_rfunct_3,t68_funct_1,d3_xboole_0,d12_rfunct_3,d12_rfunct_3,t71_funct_1,d12_rfunct_3,t68_funct_1,t34_partfun1]), [file(rfunct_3,t52_rfunct_3),interesting(0.39)]). fof(t85_rfunct_3,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( ( v1_funct_1(B) & m2_relset_1(B,A,k1_numbers) ) => ! [C] : ( m1_subset_1(C,A) => ( r2_hidden(C,k4_relset_1(A,k1_numbers,B)) => k24_rfunct_3(A,B,k2_setwiseo(A,C)) = k2_seq_1(A,k1_numbers,B,C) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t72_rfunct_3,t103_rvsum_1]), [file(rfunct_3,t85_rfunct_3),interesting(0.39)]). fof(t10_rfunct_3,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( ( v1_funct_1(B) & m2_relset_1(B,A,k1_numbers) ) => ! [C] : ( m1_subset_1(C,k1_numbers) => ( ~ r1_xreal_0(C,0) => k11_relset_1(A,k1_numbers,k21_seq_1(A,k1_numbers,B),k2_setwiseo(k1_numbers,C)) = k11_relset_1(A,k1_numbers,B,k3_setwiseo(k1_numbers,k1_real_1(C),C)) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d10_seq_1,d3_tarski,d13_funct_1,d10_seq_1,d1_tarski,d1_absvalue,d2_tarski,d13_funct_1,d1_absvalue,d2_tarski,d13_funct_1,d10_xboole_0,d3_tarski,d13_funct_1,d1_absvalue,t138_complex1,d10_seq_1,d1_tarski,d13_funct_1,d1_absvalue,d10_seq_1,d1_tarski,d13_funct_1,d2_tarski]), [file(rfunct_3,t10_rfunct_3),interesting(0.37)]). fof(t59_rfunct_3,theorem,( ! [A] : ( ( v1_funct_1(A) & m2_relset_1(A,k1_numbers,k1_numbers) ) => ! [B,C] : ( m1_subset_1(C,k1_numbers) => ( ~ r1_xreal_0(C,0) => ( r2_rfunct_3(A,B) <=> r2_rfunct_3(k13_seq_1(k1_numbers,k1_numbers,A,C),B) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d6_seq_1,d13_rfunct_3,d13_rfunct_3,d13_rfunct_3,d13_rfunct_3,t66_xreal_1,d6_seq_1,d6_seq_1,d6_seq_1,d13_rfunct_3,d6_seq_1,d13_rfunct_3,d13_rfunct_3,d6_seq_1,d6_seq_1,d6_seq_1,t73_real_1,t90_xcmplx_1,t90_xcmplx_1]), [file(rfunct_3,t59_rfunct_3),interesting(0.37)]). fof(t61_rfunct_3,theorem,( ! [A] : ( ( v1_funct_1(A) & m2_relset_1(A,k1_numbers,k1_numbers) ) => ! [B] : ( ( v1_funct_1(B) & m2_relset_1(B,k1_numbers,k1_numbers) ) => ! [C] : ( ( r2_rfunct_3(A,C) & r2_rfunct_3(B,C) ) => r2_rfunct_3(k6_seq_1(k1_numbers,k1_numbers,A,B),C) ) ) ) ), inference(mizar_proof,[status(thm)],[d3_seq_1,d13_rfunct_3,t19_xboole_1,d13_rfunct_3,d13_rfunct_3,t9_xreal_1,d3_seq_1,d3_seq_1,d3_seq_1]), [file(rfunct_3,t61_rfunct_3),interesting(0.37)]). fof(t69_rfunct_3,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( m1_subset_1(B,A) => ! [C,D] : ( ( v1_funct_1(D) & m2_relset_1(D,A,k1_numbers) ) => ( ( v1_finset_1(k4_relset_1(A,k1_numbers,k2_partfun1(A,k1_numbers,D,C))) & r2_hidden(B,k4_relset_1(A,k1_numbers,k2_partfun1(A,k1_numbers,D,C))) ) => r1_rfinseq(k8_finseq_1(k1_numbers,k22_rfunct_3(A,D,k4_xboole_0(C,k2_setwiseo(A,B))),k12_finseq_1(k1_numbers,k2_seq_1(A,k1_numbers,D,B))),k2_partfun1(A,k1_numbers,D,C)) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t68_funct_1,t100_relat_1,t97_relat_1,t68_funct_1,t37_zfmisc_1,d3_tarski,d3_xboole_0,d4_xboole_0,d3_xboole_0,d4_xboole_0,d10_xboole_0,d3_tarski,d4_xboole_0,d3_xboole_0,d4_xboole_0,d3_xboole_0,t16_finset_1,t68_rfunct_3,t66_rfunct_3]), [file(rfunct_3,t69_rfunct_3),interesting(0.36)]). fof(t30_rfunct_3,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( ~ v1_xboole_0(B) => ! [C] : ( m2_finseq_1(C,k4_rfunct_3(A,B)) => ! [D] : ( m1_subset_1(D,A) => ! [E] : ( m2_subset_1(E,k1_numbers,k5_numbers) => ( r1_rfunct_3(A,B,C,D) => r1_rfunct_3(A,B,k1_rfinseq(k4_rfunct_3(A,B),C,E),D) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d9_rfunct_3,d2_rfinseq,t26_finseq_1,d3_finseq_1,d2_rfinseq,t27_finseq_3,t29_nat_1,t2_xreal_1,t21_xreal_1,t27_finseq_3,d9_rfunct_3]), [file(rfunct_3,t30_rfunct_3),interesting(0.35)]). fof(t60_rfunct_3,theorem,( ! [A] : ( ( v1_funct_1(A) & m2_relset_1(A,k1_numbers,k1_numbers) ) => ! [B] : ( r1_tarski(B,k4_relset_1(k1_numbers,k1_numbers,A)) => r2_rfunct_3(k13_seq_1(k1_numbers,k1_numbers,A,0),B) ) ) ), inference(mizar_proof,[status(thm)],[d6_seq_1,d6_seq_1,d13_rfunct_3,d6_seq_1,d6_seq_1,d6_seq_1]), [file(rfunct_3,t60_rfunct_3),interesting(0.33)]). fof(t73_rfunct_3,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( ( v1_funct_1(B) & m2_relset_1(B,A,k1_numbers) ) => ! [C,D] : ( m1_subset_1(D,A) => ( ( v1_finset_1(k4_relset_1(A,k1_numbers,k2_partfun1(A,k1_numbers,B,C))) & r2_hidden(D,k4_relset_1(A,k1_numbers,k2_partfun1(A,k1_numbers,B,C))) & k2_seq_1(k5_numbers,k1_numbers,k22_rfunct_3(A,B,C),k3_finseq_1(k22_rfunct_3(A,B,C))) = k2_seq_1(A,k1_numbers,B,D) ) => k22_rfunct_3(A,B,C) = k8_finseq_1(k1_numbers,k22_rfunct_3(A,B,k4_xboole_0(C,k2_setwiseo(A,D))),k12_finseq_1(k1_numbers,k2_seq_1(A,k1_numbers,B,D))) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d14_rfunct_3,t1_rfinseq,t69_rfunct_3,t2_rfinseq,t12_funct_1,t27_finseq_1,t25_finseq_1,t38_nat_1,t4_finseq_2,t5_finseq_2,t20_rfinseq,t14_rfinseq,t33_rfinseq,t36_rfinseq]), [file(rfunct_3,t73_rfunct_3),interesting(0.32)]). fof(t75_rfunct_3,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( ( v1_funct_1(B) & m2_relset_1(B,A,k1_numbers) ) => ! [C] : ( m1_subset_1(C,k1_numbers) => ! [D,E] : ( m1_subset_1(E,A) => ( ( v1_finset_1(k4_relset_1(A,k1_numbers,k2_partfun1(A,k1_numbers,B,D))) & r2_hidden(E,k4_relset_1(A,k1_numbers,k2_partfun1(A,k1_numbers,B,D))) ) => ( k2_seq_1(k5_numbers,k1_numbers,k22_rfunct_3(A,k21_rfunct_3(A,B,C),D),k3_finseq_1(k22_rfunct_3(A,k21_rfunct_3(A,B,C),D))) = k2_seq_1(A,k1_numbers,k21_rfunct_3(A,B,C),E) <=> k2_seq_1(k5_numbers,k1_numbers,k22_rfunct_3(A,B,D),k3_finseq_1(k22_rfunct_3(A,B,D))) = k2_seq_1(A,k1_numbers,B,E) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t68_funct_1,d12_rfunct_3,t68_funct_1,t70_rfunct_3,d3_finseq_1,d14_rfunct_3,t1_rfinseq,t68_funct_1,d3_xboole_0,d12_rfunct_3,d5_funct_1,t12_funct_1,t27_finseq_1,t25_finseq_1,t38_nat_1,t27_finseq_3,t68_funct_1,t11_finseq_2,t27_finseq_3,d5_funct_1,t26_partfun1,t68_funct_1,d3_xboole_0,t68_funct_1,d12_rfunct_3,d5_funct_1,t11_finseq_2,t27_finseq_3,d5_real_1,t32_rfinseq,d12_rfunct_3,d5_real_1,t32_rfinseq,t11_xreal_1,t1_xreal_1,d5_funct_1,t26_partfun1,d3_xboole_0,t68_funct_1,d12_rfunct_3,t68_funct_1,d5_funct_1,t11_finseq_2,t27_finseq_3,d5_funct_1,t68_funct_1,t11_finseq_2,t27_finseq_3,d5_real_1,t32_rfinseq,t11_xreal_1,d12_rfunct_3,d5_real_1,t32_rfinseq,t1_xreal_1]), [file(rfunct_3,t75_rfunct_3),interesting(0.28)]). fof(l90_rfunct_3,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( ( v1_funct_1(B) & m2_relset_1(B,A,k1_numbers) ) => ! [C,D,E] : ( v1_finset_1(E) => ( ( E = k4_relset_1(A,k1_numbers,k2_partfun1(A,k1_numbers,B,D)) & v1_finset_1(k4_relset_1(A,k1_numbers,k2_partfun1(A,k1_numbers,B,C))) & r1_tarski(D,C) & 0 = k4_card_1(E) & ! [F] : ( m1_subset_1(F,A) => ! [G] : ( m1_subset_1(G,A) => ( ( r2_hidden(F,k4_relset_1(A,k1_numbers,k2_partfun1(A,k1_numbers,B,D))) & r2_hidden(G,k4_relset_1(A,k1_numbers,k2_partfun1(A,k1_numbers,B,k4_xboole_0(C,D)))) ) => r1_xreal_0(k2_seq_1(A,k1_numbers,B,G),k2_seq_1(A,k1_numbers,B,F)) ) ) ) ) => k22_rfunct_3(A,B,C) = k8_finseq_1(k1_numbers,k22_rfunct_3(A,B,D),k22_rfunct_3(A,B,k4_xboole_0(C,D))) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t68_funct_1,t59_card_2,t66_rfunct_3,t71_rfunct_3,t50_xboole_1,t66_rfunct_3,t66_rfunct_3,t47_finseq_1]), [file(rfunct_3,l90_rfunct_3),interesting(0.20)]). fof(t77_rfunct_3,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( ( v1_funct_1(B) & m2_relset_1(B,A,k1_numbers) ) => ! [C] : ( ( v1_finset_1(k4_relset_1(A,k1_numbers,k2_partfun1(A,k1_numbers,B,C))) & ! [D] : ( m1_subset_1(D,A) => ( r2_hidden(D,k4_relset_1(A,k1_numbers,k2_partfun1(A,k1_numbers,B,C))) => r1_xreal_0(0,k2_seq_1(A,k1_numbers,B,D)) ) ) ) => k22_rfunct_3(A,k19_rfunct_3(A,B),C) = k22_rfunct_3(A,B,C) ) ) ) ), inference(mizar_proof,[status(thm)],[t68_funct_1,t49_rfunct_3,t47_rfunct_3,t67_rfunct_3,t67_rfunct_3]), [file(rfunct_3,t77_rfunct_3),interesting(0.19)]). fof(t78_rfunct_3,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( ( v1_funct_1(B) & m2_relset_1(B,A,k1_numbers) ) => ! [C,D] : ( m1_subset_1(D,k1_numbers) => ! [E] : ( v1_finset_1(E) => ( ( E = k4_relset_1(A,k1_numbers,k2_partfun1(A,k1_numbers,B,C)) & k5_relset_1(A,k1_numbers,k2_partfun1(A,k1_numbers,B,C)) = k2_setwiseo(k1_numbers,D) ) => k22_rfunct_3(A,B,C) = k4_finseqop(k1_numbers,k4_card_1(E),D) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d14_rfunct_3,t1_rfinseq,t70_rfunct_3,d3_finseq_1,t15_funcop_1,d2_finseq_2]), [file(rfunct_3,t78_rfunct_3),interesting(0.13)]). fof(t56_rfunct_3,theorem,( ! [A] : ( m1_subset_1(A,k1_numbers) => ! [B] : ( m1_subset_1(B,k1_numbers) => ! [C] : ( ( v1_funct_1(C) & m2_relset_1(C,k1_numbers,k1_numbers) ) => ( r2_rfunct_3(C,k1_rcomp_1(A,B)) <=> ( r1_tarski(k1_rcomp_1(A,B),k4_relset_1(k1_numbers,k1_numbers,C)) & ! [D] : ( m1_subset_1(D,k1_numbers) => ! [E] : ( m1_subset_1(E,k1_numbers) => ! [F] : ( m1_subset_1(F,k1_numbers) => ( ( r2_hidden(D,k1_rcomp_1(A,B)) & r2_hidden(E,k1_rcomp_1(A,B)) & r2_hidden(F,k1_rcomp_1(A,B)) ) => ( r1_xreal_0(E,D) | r1_xreal_0(F,E) | r1_xreal_0(k6_real_1(k5_real_1(k2_seq_1(k1_numbers,k1_numbers,C,D),k2_seq_1(k1_numbers,k1_numbers,C,E)),k5_real_1(D,E)),k6_real_1(k5_real_1(k2_seq_1(k1_numbers,k1_numbers,C,E),k2_seq_1(k1_numbers,k1_numbers,C,F)),k5_real_1(E,F))) ) ) ) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d13_rfunct_3,t105_real_2,t52_xreal_1,t2_xreal_1,t105_real_2,t63_xcmplx_1,t60_xcmplx_1,t75_xcmplx_1,t75_xcmplx_1,t63_xcmplx_1,t90_xcmplx_1,t127_real_2,t127_real_2,t174_real_2,d13_rfunct_3,t23_xreal_1,t26_xreal_1,d9_xcmplx_0,d9_xcmplx_0,t67_xreal_1,d7_xcmplx_0,d7_xcmplx_0,t187_real_2,t50_xreal_1,d1_rcomp_1,t66_xreal_1,t9_xreal_1,t26_xcmplx_1,d5_real_1,t52_xreal_1,t70_xreal_1,t10_xreal_1,t105_real_2,t70_xreal_1,t10_xreal_1,t105_real_2,t105_real_2,t185_real_2,t74_real_1,t90_xcmplx_1,t90_xcmplx_1,t21_xreal_1,t22_xreal_1,t70_xreal_1,t10_xreal_1,t105_real_2,t70_xreal_1,t10_xreal_1,t105_real_2,t105_real_2,t185_real_2,t74_real_1,t90_xcmplx_1,t90_xcmplx_1,t21_xreal_1,t22_xreal_1,d5_real_1,t55_rfunct_3]), [file(rfunct_3,t56_rfunct_3),interesting(0.12)]). fof(t82_rfunct_3,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( ( v1_funct_1(B) & m2_relset_1(B,A,k1_numbers) ) => ! [C] : ( ( v1_funct_1(C) & m2_relset_1(C,A,k1_numbers) ) => ! [D] : ( ( v1_finset_1(k4_relset_1(A,k1_numbers,k2_partfun1(A,k1_numbers,B,D))) & k4_relset_1(A,k1_numbers,k2_partfun1(A,k1_numbers,B,D)) = k4_relset_1(A,k1_numbers,k2_partfun1(A,k1_numbers,C,D)) ) => k24_rfunct_3(A,k7_seq_1(A,k1_numbers,B,C),D) = k5_real_1(k24_rfunct_3(A,B,D),k24_rfunct_3(A,C,D)) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t68_funct_1,d6_seq_1,t68_funct_1,t40_rfunct_1,t38_rfunct_1,t81_rfunct_3,t80_rfunct_3]), [file(rfunct_3,t82_rfunct_3),interesting(0.02)]). fof(t38_rfunct_1,theorem,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) & v1_seq_1(A) ) => k15_seq_1(A) = k12_seq_1(A,k1_real_1(1)) ) ), file(rfunct_1,t38_rfunct_1), [interesting(0.00)]). fof(d3_tarski,definition,( ! [A,B] : ( r1_tarski(A,B) <=> ! [C] : ( r2_hidden(C,A) => r2_hidden(C,B) ) ) ), file(tarski,d3_tarski), [interesting(0.00)]). fof(d13_funct_1,definition,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) ) => ! [B,C] : ( C = k10_relat_1(A,B) <=> ! [D] : ( r2_hidden(D,C) <=> ( r2_hidden(D,k1_relat_1(A)) & r2_hidden(k1_funct_1(A,D),B) ) ) ) ) ), file(funct_1,d13_funct_1), [interesting(0.00)]). fof(d6_seq_1,definition,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) & v1_seq_1(A) ) => ! [B] : ( v1_xreal_0(B) => ! [C] : ( ( v1_relat_1(C) & v1_funct_1(C) ) => ( C = k12_seq_1(A,B) <=> ( k1_relat_1(C) = k1_relat_1(A) & ! [D] : ( r2_hidden(D,k1_relat_1(C)) => k1_funct_1(C,D) = k3_xcmplx_0(B,k1_seq_1(A,D)) ) ) ) ) ) ) ), file(seq_1,d6_seq_1), [interesting(0.00)]). fof(d1_tarski,definition,( ! [A,B] : ( B = k1_tarski(A) <=> ! [C] : ( r2_hidden(C,B) <=> C = A ) ) ), file(tarski,d1_tarski), [interesting(0.00)]). fof(t88_xcmplx_1,theorem,( ! [A] : ( v1_xcmplx_0(A) => ! [B] : ( v1_xcmplx_0(B) => ( A != 0 => k3_xcmplx_0(k7_xcmplx_0(B,A),A) = B ) ) ) ), file(xcmplx_1,t88_xcmplx_1), [interesting(0.00)]). fof(d10_xboole_0,definition,( ! [A,B] : ( A = B <=> ( r1_tarski(A,B) & r1_tarski(B,A) ) ) ), file(xboole_0,d10_xboole_0), [interesting(0.00)]). fof(t90_xcmplx_1,theorem,( ! [A] : ( v1_xcmplx_0(A) => ! [B] : ( v1_xcmplx_0(B) => ( A != 0 => B = k7_xcmplx_0(k3_xcmplx_0(B,A),A) ) ) ) ), file(xcmplx_1,t90_xcmplx_1), [interesting(0.00)]). fof(t8_rfunct_3,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( ( v1_funct_1(B) & m2_relset_1(B,A,k1_numbers) ) => ! [C] : ( v1_xreal_0(C) => ! [D] : ( v1_xreal_0(D) => ( C != 0 => k11_relset_1(A,k1_numbers,B,k1_tarski(k7_xcmplx_0(D,C))) = k11_relset_1(A,k1_numbers,k13_seq_1(A,k1_numbers,B,C),k1_tarski(D)) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d3_tarski,d13_funct_1,d6_seq_1,d1_tarski,t88_xcmplx_1,d6_seq_1,d1_tarski,d13_funct_1,d10_xboole_0,d3_tarski,d13_funct_1,d6_seq_1,d1_tarski,d6_seq_1,t90_xcmplx_1,d1_tarski,d13_funct_1]), [file(rfunct_3,t8_rfunct_3),interesting(0.00)]). fof(d1_rfinseq,definition,( ! [A] : ( v1_relat_1(A) => ! [B] : ( v1_relat_1(B) => ( r1_rfinseq(A,B) <=> ! [C] : k1_card_1(k10_relat_1(A,k1_tarski(C))) = k1_card_1(k10_relat_1(B,k1_tarski(C))) ) ) ) ), file(rfinseq,d1_rfinseq), [interesting(0.00)]). fof(t5_rfinseq,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( ( v1_relat_1(B) & v1_funct_1(B) ) => ! [C] : ( ( v1_relat_1(C) & v1_funct_1(C) ) => ( ( r1_tarski(k2_relat_1(B),A) & r1_tarski(k2_relat_1(C),A) ) => ( r1_rfinseq(B,C) <=> ! [D] : ( m1_subset_1(D,A) => k1_card_1(k10_relat_1(B,k1_tarski(D))) = k1_card_1(k10_relat_1(C,k1_tarski(D))) ) ) ) ) ) ) ), file(rfinseq,t5_rfinseq), [interesting(0.00)]). fof(t13_rfunct_3,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( ~ v1_xboole_0(B) => ! [C] : ( ( v1_funct_1(C) & m2_relset_1(C,A,k1_numbers) ) => ! [D] : ( ( v1_funct_1(D) & m2_relset_1(D,B,k1_numbers) ) => ! [E] : ( m1_subset_1(E,k1_numbers) => ( E != 0 => ( r1_rfinseq(C,D) <=> r1_rfinseq(k13_seq_1(A,k1_numbers,C,E),k13_seq_1(B,k1_numbers,D,E)) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t8_rfunct_3,d1_rfinseq,t5_rfinseq,t90_xcmplx_1,t8_rfunct_3,d1_rfinseq,t5_rfinseq]), [file(rfunct_3,t13_rfunct_3),interesting(0.00)]). fof(d10_seq_1,definition,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) & v1_seq_1(A) ) => ! [B] : ( ( v1_relat_1(B) & v1_funct_1(B) ) => ( B = k20_seq_1(A) <=> ( k1_relat_1(B) = k1_relat_1(A) & ! [C] : ( r2_hidden(C,k1_relat_1(B)) => k1_funct_1(B,C) = k18_complex1(k1_seq_1(A,C)) ) ) ) ) ) ), file(seq_1,d10_seq_1), [interesting(0.00)]). fof(d1_absvalue,definition,( ! [A] : ( v1_xreal_0(A) => ( ( r1_xreal_0(0,A) => k16_complex1(A) = A ) & ( ~ r1_xreal_0(0,A) => k16_complex1(A) = k4_xcmplx_0(A) ) ) ) ), file(absvalue,d1_absvalue), [interesting(0.00)]). fof(d2_tarski,definition,( ! [A,B,C] : ( C = k2_tarski(A,B) <=> ! [D] : ( r2_hidden(D,C) <=> ( D = A | D = B ) ) ) ), file(tarski,d2_tarski), [interesting(0.00)]). fof(t138_complex1,theorem,( ! [A] : ( v1_xcmplx_0(A) => k17_complex1(k4_xcmplx_0(A)) = k17_complex1(A) ) ), file(complex1,t138_complex1), [interesting(0.00)]). fof(t4_rfinseq,theorem,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) ) => ! [B] : ( ( v1_relat_1(B) & v1_funct_1(B) ) => ( r1_rfinseq(A,B) <=> ! [C] : k1_card_1(k10_relat_1(A,C)) = k1_card_1(k10_relat_1(B,C)) ) ) ) ), file(rfinseq,t4_rfinseq), [interesting(0.00)]). fof(t7_absvalue,theorem,( ! [A] : ( v1_xreal_0(A) => ( A = 0 <=> k18_complex1(A) = 0 ) ) ), file(absvalue,t7_absvalue), [interesting(0.00)]). fof(t11_rfunct_3,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( ( v1_funct_1(B) & m2_relset_1(B,A,k1_numbers) ) => k11_relset_1(A,k1_numbers,k21_seq_1(A,k1_numbers,B),k2_setwiseo(k1_numbers,0)) = k11_relset_1(A,k1_numbers,B,k2_setwiseo(k1_numbers,0)) ) ) ), inference(mizar_proof,[status(thm)],[d10_seq_1,d3_tarski,d13_funct_1,d10_seq_1,d1_tarski,t7_absvalue,d1_tarski,d13_funct_1,d10_xboole_0,d3_tarski,d13_funct_1,d1_tarski,t7_absvalue,d10_seq_1,d1_tarski,d13_funct_1]), [file(rfunct_3,t11_rfunct_3),interesting(0.00)]). fof(t132_complex1,theorem,( ! [A] : ( v1_xcmplx_0(A) => r1_xreal_0(0,k17_complex1(A)) ) ), file(complex1,t132_complex1), [interesting(0.00)]). fof(t12_rfunct_3,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( ( v1_funct_1(B) & m2_relset_1(B,A,k1_numbers) ) => ! [C] : ( m1_subset_1(C,k1_numbers) => ( ~ r1_xreal_0(0,C) => k11_relset_1(A,k1_numbers,k21_seq_1(A,k1_numbers,B),k2_setwiseo(k1_numbers,C)) = k1_xboole_0 ) ) ) ) ), inference(mizar_proof,[status(thm)],[d3_tarski,d13_funct_1,d10_seq_1,d1_tarski,t132_complex1]), [file(rfunct_3,t12_rfunct_3),interesting(0.00)]). fof(d13_binop_1,definition,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( ( v1_funct_1(B) & v1_funct_2(B,k2_zfmisc_1(A,A),A) & m2_relset_1(B,k2_zfmisc_1(A,A),A) ) => ( v1_binop_1(B,A) <=> ! [C] : ( m1_subset_1(C,A) => ! [D] : ( m1_subset_1(D,A) => k2_binop_1(A,A,A,B,C,D) = k2_binop_1(A,A,A,B,D,C) ) ) ) ) ) ), file(binop_1,d13_binop_1), [interesting(0.00)]). fof(d4_rfunct_3,definition,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( ( v1_funct_1(B) & v1_funct_2(B,k2_zfmisc_1(k4_rfunct_3(A,k1_numbers),k4_rfunct_3(A,k1_numbers)),k4_rfunct_3(A,k1_numbers)) & m2_relset_1(B,k2_zfmisc_1(k4_rfunct_3(A,k1_numbers),k4_rfunct_3(A,k1_numbers)),k4_rfunct_3(A,k1_numbers)) ) => ( B = k14_rfunct_3(A) <=> ! [C] : ( m2_rfunct_3(C,A,k1_numbers,k4_rfunct_3(A,k1_numbers)) => ! [D] : ( m2_rfunct_3(D,A,k1_numbers,k4_rfunct_3(A,k1_numbers)) => k2_binop_1(k4_rfunct_3(A,k1_numbers),k4_rfunct_3(A,k1_numbers),k4_rfunct_3(A,k1_numbers),B,C,D) = k6_rfunct_3(A,k1_numbers,C,D) ) ) ) ) ) ), file(rfunct_3,d4_rfunct_3), [interesting(0.00)]). fof(d14_binop_1,definition,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( ( v1_funct_1(B) & v1_funct_2(B,k2_zfmisc_1(A,A),A) & m2_relset_1(B,k2_zfmisc_1(A,A),A) ) => ( v2_binop_1(B,A) <=> ! [C] : ( m1_subset_1(C,A) => ! [D] : ( m1_subset_1(D,A) => ! [E] : ( m1_subset_1(E,A) => k2_binop_1(A,A,A,B,C,k2_binop_1(A,A,A,B,D,E)) = k2_binop_1(A,A,A,B,k2_binop_1(A,A,A,B,C,D),E) ) ) ) ) ) ) ), file(binop_1,d14_binop_1), [interesting(0.00)]). fof(t19_rfunct_1,theorem,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) & v1_seq_1(A) ) => ! [B] : ( ( v1_relat_1(B) & v1_funct_1(B) & v1_seq_1(B) ) => ! [C] : ( ( v1_relat_1(C) & v1_funct_1(C) & v1_seq_1(C) ) => k3_seq_1(k3_seq_1(A,B),C) = k3_seq_1(A,k3_seq_1(B,C)) ) ) ) ), file(rfunct_1,t19_rfunct_1), [interesting(0.00)]). fof(d2_setwiseo,definition,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( ( v1_funct_1(B) & v1_funct_2(B,k2_zfmisc_1(A,A),A) & m2_relset_1(B,k2_zfmisc_1(A,A),A) ) => ( v1_setwiseo(B,A) <=> ? [C] : ( m1_subset_1(C,A) & r3_binop_1(A,C,B) ) ) ) ) ), file(setwiseo,d2_setwiseo), [interesting(0.00)]). fof(d4_subset_1,definition,( ! [A] : k2_subset_1(A) = A ), file(subset_1,d4_subset_1), [interesting(0.00)]). fof(t19_funcop_1,theorem,( ! [A,B] : ( k1_relat_1(k2_funcop_1(A,B)) = A & r1_tarski(k2_relat_1(k2_funcop_1(A,B)),k1_tarski(B)) ) ), file(funcop_1,t19_funcop_1), [interesting(0.00)]). fof(t28_xboole_1,theorem,( ! [A,B] : ( r1_tarski(A,B) => k3_xboole_0(A,B) = A ) ), file(xboole_1,t28_xboole_1), [interesting(0.00)]). fof(d3_seq_1,definition,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) & v1_seq_1(A) ) => ! [B] : ( ( v1_relat_1(B) & v1_funct_1(B) & v1_seq_1(B) ) => ! [C] : ( ( v1_relat_1(C) & v1_funct_1(C) ) => ( C = k3_seq_1(A,B) <=> ( k1_relat_1(C) = k3_xboole_0(k1_relat_1(A),k1_relat_1(B)) & ! [D] : ( r2_hidden(D,k1_relat_1(C)) => k1_funct_1(C,D) = k3_real_1(k1_seq_1(A,D),k1_seq_1(B,D)) ) ) ) ) ) ) ), file(seq_1,d3_seq_1), [interesting(0.00)]). fof(t13_funcop_1,theorem,( ! [A,B,C] : ( r2_hidden(B,A) => k1_funct_1(k2_funcop_1(A,C),B) = C ) ), file(funcop_1,t13_funcop_1), [interesting(0.00)]). fof(t34_partfun1,theorem,( ! [A,B,C] : ( ( v1_funct_1(C) & m2_relset_1(C,A,B) ) => ! [D] : ( ( v1_funct_1(D) & m2_relset_1(D,A,B) ) => ( ( k4_relset_1(A,B,C) = k4_relset_1(A,B,D) & ! [E] : ( m1_subset_1(E,A) => ( r2_hidden(E,k4_relset_1(A,B,C)) => k1_funct_1(C,E) = k1_funct_1(D,E) ) ) ) => C = D ) ) ) ), file(partfun1,t34_partfun1), [interesting(0.00)]). fof(t13_binop_1,theorem,( ! [A,B] : ( ( v1_funct_1(B) & v1_funct_2(B,k2_zfmisc_1(A,A),A) & m2_relset_1(B,k2_zfmisc_1(A,A),A) ) => ! [C] : ( m1_subset_1(C,A) => ( v1_binop_1(B,A) => ( r3_binop_1(A,C,B) <=> ! [D] : ( m1_subset_1(D,A) => k1_binop_1(B,D,C) = D ) ) ) ) ) ), file(binop_1,t13_binop_1), [interesting(0.00)]). fof(t6_finsop_1,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( m2_finseq_1(B,A) => ! [C] : ( m2_finseq_1(C,A) => ! [D] : ( ( v1_funct_1(D) & v1_funct_2(D,k2_zfmisc_1(A,A),A) & m2_relset_1(D,k2_zfmisc_1(A,A),A) ) => ( v2_binop_1(D,A) => ( ( ~ v1_setwiseo(D,A) & ~ ( r1_xreal_0(1,k3_finseq_1(B)) & r1_xreal_0(1,k3_finseq_1(C)) ) ) | k2_finsop_1(A,k8_finseq_1(A,B,C),D) = k2_binop_1(A,A,A,D,k2_finsop_1(A,B,D),k2_finsop_1(A,C,D)) ) ) ) ) ) ) ), file(finsop_1,t6_finsop_1), [interesting(0.00)]). fof(t24_rfunct_3,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( m2_finseq_1(B,k4_rfunct_3(A,k1_numbers)) => ! [C] : ( m2_finseq_1(C,k4_rfunct_3(A,k1_numbers)) => k15_rfunct_3(A,k8_finseq_1(k4_rfunct_3(A,k1_numbers),B,C)) = k6_rfunct_3(A,k1_numbers,k15_rfunct_3(A,B),k15_rfunct_3(A,C)) ) ) ) ), inference(mizar_proof,[status(thm)],[t16_rfunct_3,t17_rfunct_3,t20_rfunct_3,t6_finsop_1,d4_rfunct_3]), [file(rfunct_3,t24_rfunct_3),interesting(0.00)]). fof(t12_finsop_1,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( m1_subset_1(B,A) => ! [C] : ( ( v1_funct_1(C) & v1_funct_2(C,k2_zfmisc_1(A,A),A) & m2_relset_1(C,k2_zfmisc_1(A,A),A) ) => k2_finsop_1(A,k12_finseq_1(A,B),C) = B ) ) ) ), file(finsop_1,t12_finsop_1), [interesting(0.00)]). fof(t25_rfunct_3,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( m2_finseq_1(B,k4_rfunct_3(A,k1_numbers)) => ! [C] : ( m2_rfunct_3(C,A,k1_numbers,k4_rfunct_3(A,k1_numbers)) => k15_rfunct_3(A,k8_finseq_1(k4_rfunct_3(A,k1_numbers),k12_finseq_1(k4_rfunct_3(A,k1_numbers),C),B)) = k6_rfunct_3(A,k1_numbers,C,k15_rfunct_3(A,B)) ) ) ) ), inference(mizar_proof,[status(thm)],[t24_rfunct_3,t22_rfunct_3]), [file(rfunct_3,t25_rfunct_3),interesting(0.00)]). fof(t60_finseq_1,theorem,( ! [A,B,C] : ( k11_finseq_1(A,B,C) = k7_finseq_1(k9_finseq_1(A),k10_finseq_1(B,C)) & k11_finseq_1(A,B,C) = k7_finseq_1(k10_finseq_1(A,B),k9_finseq_1(C)) ) ), file(finseq_1,t60_finseq_1), [interesting(0.00)]). fof(t5_finsop_1,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( m1_subset_1(B,A) => ! [C] : ( m2_finseq_1(C,A) => ! [D] : ( ( v1_funct_1(D) & v1_funct_2(D,k2_zfmisc_1(A,A),A) & m2_relset_1(D,k2_zfmisc_1(A,A),A) ) => ( ( v1_setwiseo(D,A) | r1_xreal_0(1,k3_finseq_1(C)) ) => k2_finsop_1(A,k8_finseq_1(A,C,k12_finseq_1(A,B)),D) = k2_binop_1(A,A,A,D,k2_finsop_1(A,C,D),B) ) ) ) ) ) ), file(finsop_1,t5_finsop_1), [interesting(0.00)]). fof(t23_rfunct_3,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( m2_finseq_1(B,k4_rfunct_3(A,k1_numbers)) => ! [C] : ( m2_rfunct_3(C,A,k1_numbers,k4_rfunct_3(A,k1_numbers)) => k15_rfunct_3(A,k8_finseq_1(k4_rfunct_3(A,k1_numbers),B,k12_finseq_1(k4_rfunct_3(A,k1_numbers),C))) = k6_rfunct_3(A,k1_numbers,k15_rfunct_3(A,B),C) ) ) ) ), inference(mizar_proof,[status(thm)],[t16_rfunct_3,t17_rfunct_3,t20_rfunct_3,t5_finsop_1,d4_rfunct_3]), [file(rfunct_3,t23_rfunct_3),interesting(0.00)]). fof(d9_finseq_1,definition,( ! [A,B] : k10_finseq_1(A,B) = k7_finseq_1(k9_finseq_1(A),k9_finseq_1(B)) ), file(finseq_1,d9_finseq_1), [interesting(0.00)]). fof(t26_rfunct_3,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( m2_rfunct_3(B,A,k1_numbers,k4_rfunct_3(A,k1_numbers)) => ! [C] : ( m2_rfunct_3(C,A,k1_numbers,k4_rfunct_3(A,k1_numbers)) => k15_rfunct_3(A,k2_finseq_4(k4_rfunct_3(A,k1_numbers),B,C)) = k6_rfunct_3(A,k1_numbers,B,C) ) ) ) ), inference(mizar_proof,[status(thm)],[d9_finseq_1,t23_rfunct_3,t22_rfunct_3]), [file(rfunct_3,t26_rfunct_3),interesting(0.00)]). fof(t27_rfunct_3,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( m2_rfunct_3(B,A,k1_numbers,k4_rfunct_3(A,k1_numbers)) => ! [C] : ( m2_rfunct_3(C,A,k1_numbers,k4_rfunct_3(A,k1_numbers)) => ! [D] : ( m2_rfunct_3(D,A,k1_numbers,k4_rfunct_3(A,k1_numbers)) => k15_rfunct_3(A,k3_finseq_4(k4_rfunct_3(A,k1_numbers),B,C,D)) = k6_rfunct_3(A,k1_numbers,k6_rfunct_3(A,k1_numbers,B,C),D) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t60_finseq_1,t23_rfunct_3,t26_rfunct_3]), [file(rfunct_3,t27_rfunct_3),interesting(0.00)]). fof(t32_finseq_1,theorem,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) & v1_finseq_1(A) ) => ! [B] : ( A = k6_finseq_1(B) <=> k3_finseq_1(A) = 0 ) ) ), file(finseq_1,t32_finseq_1), [interesting(0.00)]). fof(t16_rfinseq,theorem,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) & v1_finseq_1(A) ) => ! [B] : ( ( v1_relat_1(B) & v1_funct_1(B) & v1_finseq_1(B) ) => ( r1_rfinseq(A,B) => ( k3_finseq_1(A) = k3_finseq_1(B) & k4_finseq_1(A) = k4_finseq_1(B) ) ) ) ) ), file(rfinseq,t16_rfinseq), [interesting(0.00)]). fof(t1_rfinseq,theorem,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) ) => ! [B] : ( ( v1_relat_1(B) & v1_funct_1(B) ) => ( r1_rfinseq(A,B) => k2_relat_1(A) = k2_relat_1(B) ) ) ) ), file(rfinseq,t1_rfinseq), [interesting(0.00)]). fof(t38_nat_1,theorem,( ! [A] : ( v4_ordinal2(A) => ! [B] : ( v4_ordinal2(B) => ( ~ r1_xreal_0(k2_xcmplx_0(B,1),A) <=> r1_xreal_0(A,B) ) ) ) ), file(nat_1,t38_nat_1), [interesting(0.00)]). fof(t27_finseq_3,theorem,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) & v1_finseq_1(A) ) => ! [B] : ( v4_ordinal2(B) => ( r2_hidden(B,k4_finseq_1(A)) <=> ( r1_xreal_0(1,B) & r1_xreal_0(B,k3_finseq_1(A)) ) ) ) ) ), file(finseq_3,t27_finseq_3), [interesting(0.00)]). fof(t13_finseq_2,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B,C] : ( m2_finseq_1(C,B) => ( r2_hidden(A,k4_finseq_1(C)) => r2_hidden(k1_funct_1(C,A),B) ) ) ) ), file(finseq_2,t13_finseq_2), [interesting(0.00)]). fof(d5_funct_1,definition,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) ) => ! [B] : ( B = k2_relat_1(A) <=> ! [C] : ( r2_hidden(C,B) <=> ? [D] : ( r2_hidden(D,k1_relat_1(A)) & C = k1_funct_1(A,D) ) ) ) ) ), file(funct_1,d5_funct_1), [interesting(0.00)]). fof(t11_finseq_2,theorem,( ! [A,B] : ( ( v1_relat_1(B) & v1_funct_1(B) & v1_finseq_1(B) ) => ~ ( r2_hidden(A,k2_relat_1(B)) & ! [C] : ( m2_subset_1(C,k1_numbers,k5_numbers) => ~ ( r2_hidden(C,k4_finseq_1(B)) & k1_funct_1(B,C) = A ) ) ) ) ), file(finseq_2,t11_finseq_2), [interesting(0.00)]). fof(t21_rfinseq,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( m2_finseq_1(B,A) => ! [C] : ( m2_subset_1(C,k1_numbers,k5_numbers) => k8_finseq_1(A,k16_finseq_1(A,B,C),k1_rfinseq(A,B,C)) = B ) ) ) ), file(rfinseq,t21_rfinseq), [interesting(0.00)]). fof(t4_finseq_2,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( m2_subset_1(B,k1_numbers,k5_numbers) => ( r1_xreal_0(A,B) => k2_square_1(0,k6_xcmplx_0(B,A)) = k6_xcmplx_0(B,A) ) ) ) ), file(finseq_2,t4_finseq_2), [interesting(0.00)]). fof(t5_finseq_2,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( m2_subset_1(B,k1_numbers,k5_numbers) => m2_subset_1(k2_square_1(0,k6_xcmplx_0(A,B)),k1_numbers,k5_numbers) ) ) ), file(finseq_2,t5_finseq_2), [interesting(0.00)]). fof(t80_finseq_1,theorem,( ! [A,B] : ( m2_finseq_1(B,A) => ! [C] : ( v4_ordinal2(C) => ( r1_xreal_0(C,k3_finseq_1(B)) => k3_finseq_1(k16_finseq_1(A,B,C)) = C ) ) ) ), file(finseq_1,t80_finseq_1), [interesting(0.00)]). fof(t3_finseq_1,theorem,( ! [A] : ( v4_ordinal2(A) => ! [B] : ( v4_ordinal2(B) => ( r2_hidden(A,k2_finseq_1(B)) <=> ( r1_xreal_0(1,A) & r1_xreal_0(A,B) ) ) ) ) ), file(finseq_1,t3_finseq_1), [interesting(0.00)]). fof(t19_rfinseq,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( m2_finseq_1(B,A) => ! [C] : ( m2_subset_1(C,k1_numbers,k5_numbers) => ! [D] : ( m2_subset_1(D,k1_numbers,k5_numbers) => ( ( r2_hidden(C,k4_finseq_1(B)) & r2_hidden(D,k2_finseq_1(C)) ) => ( k1_funct_1(k16_finseq_1(A,B,C),D) = k1_funct_1(B,D) & r2_hidden(D,k4_finseq_1(B)) ) ) ) ) ) ) ), file(rfinseq,t19_rfinseq), [interesting(0.00)]). fof(t20_rfinseq,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( m2_finseq_1(B,A) => ! [C] : ( m2_subset_1(C,k1_numbers,k5_numbers) => ! [D] : ( ( k3_finseq_1(B) = k1_nat_1(C,1) & D = k1_funct_1(B,k1_nat_1(C,1)) ) => B = k7_finseq_1(k16_finseq_1(A,B,C),k9_finseq_1(D)) ) ) ) ) ), file(rfinseq,t20_rfinseq), [interesting(0.00)]). fof(t29_nat_1,theorem,( ! [A] : ( v4_ordinal2(A) => ! [B] : ( v4_ordinal2(B) => r1_xreal_0(A,k2_xcmplx_0(A,B)) ) ) ), file(nat_1,t29_nat_1), [interesting(0.00)]). fof(t7_finseq_1,theorem,( ! [A] : ( v4_ordinal2(A) => ! [B] : ( v4_ordinal2(B) => ( r1_xreal_0(A,B) <=> r1_tarski(k2_finseq_1(A),k2_finseq_1(B)) ) ) ) ), file(finseq_1,t7_finseq_1), [interesting(0.00)]). fof(d15_finseq_1,definition,( ! [A,B] : ( m2_finseq_1(B,A) => ! [C] : ( v4_ordinal2(C) => k16_finseq_1(A,B,C) = k7_relat_1(B,k2_finseq_1(C)) ) ) ), file(finseq_1,d15_finseq_1), [interesting(0.00)]). fof(t100_relat_1,theorem,( ! [A,B,C] : ( v1_relat_1(C) => k7_relat_1(k7_relat_1(C,A),B) = k7_relat_1(C,k3_xboole_0(A,B)) ) ), file(relat_1,t100_relat_1), [interesting(0.00)]). fof(t63_finseq_3,theorem,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) & v1_finseq_1(A) ) => ! [B] : ( ( v1_relat_1(B) & v1_funct_1(B) & v1_finseq_1(B) ) => ! [C] : k4_card_1(k10_relat_1(k7_finseq_1(A,B),C)) = k1_nat_1(k4_card_1(k10_relat_1(A,C)),k4_card_1(k10_relat_1(B,C))) ) ) ), file(finseq_3,t63_finseq_3), [interesting(0.00)]). fof(s1_nat_1,theorem, ( ( p1_s1_nat_1(0) & ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ( p1_s1_nat_1(A) => p1_s1_nat_1(k1_nat_1(A,1)) ) ) ) => ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => p1_s1_nat_1(A) ) ), file(nat_1,s1_nat_1), [interesting(0.00)]). fof(d9_rfunct_3,definition,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( ~ v1_xboole_0(B) => ! [C] : ( m2_finseq_1(C,k4_rfunct_3(A,B)) => ! [D] : ( m1_subset_1(D,A) => ( r1_rfunct_3(A,B,C,D) <=> ! [E] : ( m2_rfunct_3(E,A,B,k4_rfunct_3(A,B)) => ! [F] : ( m2_subset_1(F,k1_numbers,k5_numbers) => ( ( r2_hidden(F,k4_finseq_1(C)) & k1_funct_1(C,F) = E ) => r2_hidden(D,k4_relset_1(A,B,E)) ) ) ) ) ) ) ) ) ), file(rfunct_3,d9_rfunct_3), [interesting(0.00)]). fof(d2_rfinseq,definition,( ! [A,B] : ( m2_finseq_1(B,A) => ! [C] : ( m2_subset_1(C,k1_numbers,k5_numbers) => ! [D] : ( m2_finseq_1(D,A) => ( ( r1_xreal_0(C,k3_finseq_1(B)) => ( D = k1_rfinseq(A,B,C) <=> ( k3_finseq_1(D) = k5_real_1(k3_finseq_1(B),C) & ! [E] : ( m2_subset_1(E,k1_numbers,k5_numbers) => ( r2_hidden(E,k4_finseq_1(D)) => k1_funct_1(D,E) = k1_funct_1(B,k1_nat_1(E,C)) ) ) ) ) ) & ( ~ r1_xreal_0(C,k3_finseq_1(B)) => ( D = k1_rfinseq(A,B,C) <=> D = k6_finseq_1(A) ) ) ) ) ) ) ), file(rfinseq,d2_rfinseq), [interesting(0.00)]). fof(t26_finseq_1,theorem,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) & v1_finseq_1(A) ) => ( A = k1_xboole_0 <=> k4_finseq_1(A) = k1_xboole_0 ) ) ), file(finseq_1,t26_finseq_1), [interesting(0.00)]). fof(d3_finseq_1,definition,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) & v1_finseq_1(A) ) => ! [B] : ( m2_subset_1(B,k1_numbers,k5_numbers) => ( B = k3_finseq_1(A) <=> k2_finseq_1(B) = k1_relat_1(A) ) ) ) ), file(finseq_1,d3_finseq_1), [interesting(0.00)]). fof(t2_xreal_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ! [C] : ( v1_xreal_0(C) => ( ( r1_xreal_0(A,B) & r1_xreal_0(B,C) ) => r1_xreal_0(A,C) ) ) ) ) ), file(xreal_1,t2_xreal_1), [interesting(0.00)]). fof(t21_xreal_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ! [C] : ( v1_xreal_0(C) => ( r1_xreal_0(k2_xcmplx_0(A,B),C) <=> r1_xreal_0(A,k6_xcmplx_0(C,B)) ) ) ) ) ), file(xreal_1,t21_xreal_1), [interesting(0.00)]). fof(d6_rfunct_3,definition,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( ( v1_relat_1(B) & v1_funct_1(B) & v1_finseq_1(B) ) => ! [C] : ( m2_finseq_1(C,k4_rfunct_3(A,k1_numbers)) => ( C = k16_rfunct_3(A,B) <=> ( k3_finseq_1(C) = k3_finseq_1(B) & ! [D] : ( m2_subset_1(D,k1_numbers,k5_numbers) => ( r2_hidden(D,k4_finseq_1(C)) => k1_funct_1(C,D) = k5_rfunct_1(k1_funct_1(B,D),A) ) ) ) ) ) ) ) ), file(rfunct_3,d6_rfunct_3), [interesting(0.00)]). fof(t77_rfunct_1,theorem,( ! [A,B] : ( ~ v1_xboole_0(B) => ! [C] : ( ( v1_funct_1(C) & m2_relset_1(C,B,k1_numbers) ) => ( C = k5_rfunct_1(A,B) <=> ( k4_relset_1(B,k1_numbers,C) = B & ! [D] : ( m1_subset_1(D,B) => ( ( r2_hidden(D,A) => k2_seq_1(B,k1_numbers,C,D) = 1 ) & ( ~ r2_hidden(D,A) => k2_seq_1(B,k1_numbers,C,D) = 0 ) ) ) ) ) ) ) ), file(rfunct_1,t77_rfunct_1), [interesting(0.00)]). fof(t35_square_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => r1_xreal_0(k1_square_1(A,B),A) ) ) ), file(square_1,t35_square_1), [interesting(0.00)]). fof(d7_rfunct_3,definition,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( m2_finseq_1(B,k4_rfunct_3(A,k1_numbers)) => ! [C] : ( m2_finseq_1(C,k1_numbers) => ! [D] : ( m2_finseq_1(D,k4_rfunct_3(A,k1_numbers)) => ( D = k17_rfunct_3(A,B,C) <=> ( k3_finseq_1(D) = k1_rfunct_3(k3_finseq_1(C),k3_finseq_1(B)) & ! [E] : ( m2_subset_1(E,k1_numbers,k5_numbers) => ( r2_hidden(E,k4_finseq_1(D)) => ! [F] : ( ( v1_funct_1(F) & m2_relset_1(F,A,k1_numbers) ) => ! [G] : ( m1_subset_1(G,k1_numbers) => ( ( G = k2_seq_1(k5_numbers,k1_numbers,C,E) & F = k1_funct_1(B,E) ) => k1_funct_1(D,E) = k13_seq_1(A,k1_numbers,F,G) ) ) ) ) ) ) ) ) ) ) ) ), file(rfunct_3,d7_rfunct_3), [interesting(0.00)]). fof(d8_binop_1,definition,( ! [A,B] : ( ( v1_funct_1(B) & v1_funct_2(B,k2_zfmisc_1(A,A),A) & m2_relset_1(B,k2_zfmisc_1(A,A),A) ) => ( ? [C] : ( m1_subset_1(C,A) & r3_binop_1(A,C,B) ) => ! [C] : ( m1_subset_1(C,A) => ( C = k3_binop_1(A,B) <=> r3_binop_1(A,C,B) ) ) ) ) ), file(binop_1,d8_binop_1), [interesting(0.00)]). fof(t11_finsop_1,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( ( v1_funct_1(B) & v1_funct_2(B,k2_zfmisc_1(A,A),A) & m2_relset_1(B,k2_zfmisc_1(A,A),A) ) => ( v1_setwiseo(B,A) => k2_finsop_1(A,k6_finseq_1(A),B) = k3_binop_1(A,B) ) ) ) ), file(finsop_1,t11_finsop_1), [interesting(0.00)]). fof(d8_rfunct_3,definition,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( m2_finseq_1(B,k4_rfunct_3(A,k1_numbers)) => ! [C] : ( m1_subset_1(C,A) => ! [D] : ( m2_finseq_1(D,k1_numbers) => ( D = k18_rfunct_3(A,B,C) <=> ( k3_finseq_1(D) = k3_finseq_1(B) & ! [E] : ( m2_subset_1(E,k1_numbers,k5_numbers) => ! [F] : ( m2_rfunct_3(F,A,k1_numbers,k4_rfunct_3(A,k1_numbers)) => ( ( r2_hidden(E,k4_finseq_1(D)) & k1_funct_1(B,E) = F ) => k2_seq_1(k5_numbers,k1_numbers,D,E) = k2_seq_1(A,k1_numbers,F,C) ) ) ) ) ) ) ) ) ) ), file(rfunct_3,d8_rfunct_3), [interesting(0.00)]). fof(t102_rvsum_1,theorem,( k15_rvsum_1(k6_finseq_1(k1_numbers)) = 0 ), file(rvsum_1,t102_rvsum_1), [interesting(0.00)]). fof(t57_finseq_1,theorem,( ! [A,B] : ( ( v1_relat_1(B) & v1_funct_1(B) & v1_finseq_1(B) ) => ( B = k9_finseq_1(A) <=> ( k3_finseq_1(B) = 1 & k1_funct_1(B,1) = A ) ) ) ), file(finseq_1,t57_finseq_1), [interesting(0.00)]). fof(t4_finseq_1,theorem, ( k2_finseq_1(0) = k1_xboole_0 & k2_finseq_1(1) = k1_tarski(1) & k2_finseq_1(2) = k2_tarski(1,2) ), file(finseq_1,t4_finseq_1), [interesting(0.00)]). fof(t10_finseq_2,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( ( v1_relat_1(B) & v1_funct_1(B) & v1_finseq_1(B) ) => ! [C] : ( ( v1_relat_1(C) & v1_funct_1(C) & v1_finseq_1(C) ) => ( ( k3_finseq_1(B) = A & k3_finseq_1(C) = A & ! [D] : ( m2_subset_1(D,k1_numbers,k5_numbers) => ( r2_hidden(D,k2_finseq_1(A)) => k1_funct_1(B,D) = k1_funct_1(C,D) ) ) ) => B = C ) ) ) ) ), file(finseq_2,t10_finseq_2), [interesting(0.00)]). fof(t103_rvsum_1,theorem,( ! [A] : ( m1_subset_1(A,k1_numbers) => k15_rvsum_1(k12_finseq_1(k1_numbers,A)) = A ) ), file(rvsum_1,t103_rvsum_1), [interesting(0.00)]). fof(t97_relat_1,theorem,( ! [A,B] : ( v1_relat_1(B) => ( r1_tarski(k1_relat_1(B),A) => k7_relat_1(B,A) = B ) ) ), file(relat_1,t97_relat_1), [interesting(0.00)]). fof(d3_xboole_0,definition,( ! [A,B,C] : ( C = k3_xboole_0(A,B) <=> ! [D] : ( r2_hidden(D,C) <=> ( r2_hidden(D,A) & r2_hidden(D,B) ) ) ) ), file(xboole_0,d3_xboole_0), [interesting(0.00)]). fof(d5_real_1,definition,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ( r1_xreal_0(A,B) <=> ~ ( r1_xreal_0(B,A) & B != A ) ) ) ) ), file(real_1,d5_real_1), [interesting(0.00)]). fof(t32_rfunct_3,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( m2_finseq_1(B,k4_rfunct_3(A,k1_numbers)) => ! [C] : ( m1_subset_1(C,A) => ! [D] : ( m2_subset_1(D,k1_numbers,k5_numbers) => k18_rfunct_3(A,k16_finseq_1(k4_rfunct_3(A,k1_numbers),B,D),C) = k16_finseq_1(k1_numbers,k18_rfunct_3(A,B,C),D) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d8_rfunct_3,l10_rfunct_3,l10_rfunct_3,t80_finseq_1,d3_finseq_1,t32_finseq_1,t38_nat_1,t27_finseq_3,t19_rfinseq,t13_finseq_2,d8_rfunct_3,t19_rfinseq,d8_rfunct_3,t10_finseq_2]), [file(rfunct_3,t32_rfunct_3),interesting(0.00)]). fof(t104_rvsum_1,theorem,( ! [A] : ( m1_subset_1(A,k1_numbers) => ! [B] : ( m2_finseq_1(B,k1_numbers) => k15_rvsum_1(k8_finseq_1(k1_numbers,B,k12_finseq_1(k1_numbers,A))) = k9_binop_2(k15_rvsum_1(B),A) ) ) ), file(rvsum_1,t104_rvsum_1), [interesting(0.00)]). fof(d10_rfunct_3,definition,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( ( v1_funct_1(B) & m2_relset_1(B,A,k1_numbers) ) => ! [C] : ( ( v1_funct_1(C) & m2_relset_1(C,A,k1_numbers) ) => ( C = k19_rfunct_3(A,B) <=> ( k4_relset_1(A,k1_numbers,C) = k4_relset_1(A,k1_numbers,B) & ! [D] : ( m1_subset_1(D,A) => ( r2_hidden(D,k4_relset_1(A,k1_numbers,C)) => k2_seq_1(A,k1_numbers,C,D) = k2_rfunct_3(k2_seq_1(A,k1_numbers,B,D)) ) ) ) ) ) ) ) ), file(rfunct_3,d10_rfunct_3), [interesting(0.00)]). fof(d11_rfunct_3,definition,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( ( v1_funct_1(B) & m2_relset_1(B,A,k1_numbers) ) => ! [C] : ( ( v1_funct_1(C) & m2_relset_1(C,A,k1_numbers) ) => ( C = k20_rfunct_3(A,B) <=> ( k4_relset_1(A,k1_numbers,C) = k4_relset_1(A,k1_numbers,B) & ! [D] : ( m1_subset_1(D,A) => ( r2_hidden(D,k4_relset_1(A,k1_numbers,C)) => k2_seq_1(A,k1_numbers,C,D) = k3_rfunct_3(k2_seq_1(A,k1_numbers,B,D)) ) ) ) ) ) ) ) ), file(rfunct_3,d11_rfunct_3), [interesting(0.00)]). fof(d4_seq_1,definition,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) & v1_seq_1(A) ) => ! [B] : ( ( v1_relat_1(B) & v1_funct_1(B) & v1_seq_1(B) ) => ! [C] : ( ( v1_relat_1(C) & v1_funct_1(C) ) => ( C = k4_seq_1(A,B) <=> ( k1_relat_1(C) = k3_xboole_0(k1_relat_1(A),k1_relat_1(B)) & ! [D] : ( r2_hidden(D,k1_relat_1(C)) => k1_funct_1(C,D) = k5_real_1(k1_seq_1(A,D),k1_seq_1(B,D)) ) ) ) ) ) ) ), file(seq_1,d4_seq_1), [interesting(0.00)]). fof(d2_square_1,definition,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ( ( r1_xreal_0(B,A) => k2_square_1(A,B) = A ) & ( ~ r1_xreal_0(B,A) => k2_square_1(A,B) = B ) ) ) ) ), file(square_1,d2_square_1), [interesting(0.00)]). fof(t26_xreal_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ( r1_xreal_0(A,B) <=> r1_xreal_0(k4_xcmplx_0(B),k4_xcmplx_0(A)) ) ) ) ), file(xreal_1,t26_xreal_1), [interesting(0.00)]). fof(t60_xreal_1,theorem,( ! [A] : ( v1_xreal_0(A) => ( ~ ( ~ r1_xreal_0(0,A) & r1_xreal_0(k4_xcmplx_0(A),0) ) & ~ ( ~ r1_xreal_0(k4_xcmplx_0(A),0) & r1_xreal_0(0,A) ) ) ) ), file(xreal_1,t60_xreal_1), [interesting(0.00)]). fof(t37_rfunct_3,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( ( v1_funct_1(B) & m2_relset_1(B,A,k1_numbers) ) => ( B = k7_seq_1(A,k1_numbers,k19_rfunct_3(A,B),k20_rfunct_3(A,B)) & k21_seq_1(A,k1_numbers,B) = k6_seq_1(A,k1_numbers,k19_rfunct_3(A,B),k20_rfunct_3(A,B)) & k13_seq_1(A,k1_numbers,k19_rfunct_3(A,B),2) = k6_seq_1(A,k1_numbers,B,k21_seq_1(A,k1_numbers,B)) ) ) ) ), inference(mizar_proof,[status(thm)],[d10_rfunct_3,d11_rfunct_3,d6_seq_1,d10_seq_1,d3_seq_1,d4_seq_1,d4_seq_1,d10_rfunct_3,d11_rfunct_3,t1_rfunct_3,t34_partfun1,d3_seq_1,d10_rfunct_3,d11_rfunct_3,t2_rfunct_3,d10_seq_1,t34_partfun1,d6_seq_1,d10_rfunct_3,t3_rfunct_3,d10_seq_1,d3_seq_1,t34_partfun1]), [file(rfunct_3,t37_rfunct_3),interesting(0.00)]). fof(t49_square_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ( k2_square_1(A,B) = A | k2_square_1(A,B) = B ) ) ) ), file(square_1,t49_square_1), [interesting(0.00)]). fof(t38_rfunct_3,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( ( v1_funct_1(B) & m2_relset_1(B,A,k1_numbers) ) => ! [C] : ( m1_subset_1(C,k1_numbers) => ( ~ r1_xreal_0(C,0) => k11_relset_1(A,k1_numbers,B,k2_setwiseo(k1_numbers,C)) = k11_relset_1(A,k1_numbers,k19_rfunct_3(A,B),k2_setwiseo(k1_numbers,C)) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d10_rfunct_3,d3_tarski,d13_funct_1,d1_tarski,d10_rfunct_3,d2_square_1,d1_tarski,d13_funct_1,d10_xboole_0,d3_tarski,d13_funct_1,d1_tarski,d10_rfunct_3,t49_square_1,d1_tarski,d13_funct_1]), [file(rfunct_3,t38_rfunct_3),interesting(0.00)]). fof(d1_limfunc1,definition,( ! [A] : ( v1_xreal_0(A) => k2_limfunc1(A) = a_1_0_limfunc1(A) ) ), file(limfunc1,d1_limfunc1), [interesting(0.00)]). fof(t39_rfunct_3,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( ( v1_funct_1(B) & m2_relset_1(B,A,k1_numbers) ) => k11_relset_1(A,k1_numbers,B,k2_limfunc1(0)) = k11_relset_1(A,k1_numbers,k19_rfunct_3(A,B),k2_setwiseo(k1_numbers,0)) ) ) ), inference(mizar_proof,[status(thm)],[d10_rfunct_3,d1_limfunc1,d3_tarski,d13_funct_1,d2_square_1,d10_rfunct_3,d1_tarski,d13_funct_1,d10_xboole_0,d3_tarski,d13_funct_1,d1_tarski,d10_rfunct_3,d2_square_1,d13_funct_1]), [file(rfunct_3,t39_rfunct_3),interesting(0.00)]). fof(t26_partfun1,theorem,( ! [A,B,C,D] : ( ( v1_funct_1(D) & m2_relset_1(D,A,B) ) => ~ ( r2_hidden(C,k2_relat_1(D)) & ! [E] : ( m1_subset_1(E,A) => ~ ( r2_hidden(E,k4_relset_1(A,B,D)) & C = k1_funct_1(D,E) ) ) ) ) ), file(partfun1,t26_partfun1), [interesting(0.00)]). fof(t46_square_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => r1_xreal_0(A,k2_square_1(A,B)) ) ) ), file(square_1,t46_square_1), [interesting(0.00)]). fof(d7_xboole_0,definition,( ! [A,B] : ( r1_xboole_0(A,B) <=> k3_xboole_0(A,B) = k1_xboole_0 ) ), file(xboole_0,d7_xboole_0), [interesting(0.00)]). fof(t173_relat_1,theorem,( ! [A,B] : ( v1_relat_1(B) => ( k10_relat_1(B,A) = k1_xboole_0 <=> r1_xboole_0(k2_relat_1(B),A) ) ) ), file(relat_1,t173_relat_1), [interesting(0.00)]). fof(t41_rfunct_3,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( ( v1_funct_1(B) & m2_relset_1(B,A,k1_numbers) ) => ! [C] : ( m1_subset_1(C,k1_numbers) => ( ~ r1_xreal_0(C,0) => k11_relset_1(A,k1_numbers,B,k2_setwiseo(k1_numbers,k1_real_1(C))) = k11_relset_1(A,k1_numbers,k20_rfunct_3(A,B),k2_setwiseo(k1_numbers,C)) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d11_rfunct_3,d3_tarski,d13_funct_1,d1_tarski,d11_rfunct_3,d2_square_1,d1_tarski,d13_funct_1,d10_xboole_0,d3_tarski,d13_funct_1,d1_tarski,d11_rfunct_3,t49_square_1,d1_tarski,d13_funct_1]), [file(rfunct_3,t41_rfunct_3),interesting(0.00)]). fof(d2_limfunc1,definition,( ! [A] : ( v1_xreal_0(A) => k3_limfunc1(A) = a_1_1_limfunc1(A) ) ), file(limfunc1,d2_limfunc1), [interesting(0.00)]). fof(t42_rfunct_3,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( ( v1_funct_1(B) & m2_relset_1(B,A,k1_numbers) ) => k11_relset_1(A,k1_numbers,B,k3_limfunc1(0)) = k11_relset_1(A,k1_numbers,k20_rfunct_3(A,B),k2_setwiseo(k1_numbers,0)) ) ) ), inference(mizar_proof,[status(thm)],[d11_rfunct_3,d2_limfunc1,d3_tarski,d13_funct_1,t26_xreal_1,d2_square_1,d11_rfunct_3,d1_tarski,d13_funct_1,d10_xboole_0,d3_tarski,d13_funct_1,d1_tarski,d11_rfunct_3,d2_square_1,t26_xreal_1,d13_funct_1]), [file(rfunct_3,t42_rfunct_3),interesting(0.00)]). fof(t19_limfunc1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => k5_subset_1(k1_numbers,k2_limfunc1(A),k3_limfunc1(B)) = k1_rcomp_1(B,A) ) ) ), file(limfunc1,t19_limfunc1), [interesting(0.00)]). fof(t14_rcomp_1,theorem,( ! [A] : ( v1_xreal_0(A) => k1_rcomp_1(A,A) = k1_seq_4(A) ) ), file(rcomp_1,t14_rcomp_1), [interesting(0.00)]). fof(t64_card_2,theorem,( ! [A] : ( v1_finset_1(A) => ! [B] : ( v1_finset_1(B) => k4_card_1(k2_xboole_0(A,B)) = k5_real_1(k1_nat_1(k4_card_1(A),k4_card_1(B)),k4_card_1(k3_xboole_0(A,B))) ) ) ), file(card_2,t64_card_2), [interesting(0.00)]). fof(t25_limfunc1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ( k4_xboole_0(k1_numbers,k2_rcomp_1(A,B)) = k4_subset_1(k1_numbers,k2_limfunc1(A),k3_limfunc1(B)) & k4_xboole_0(k1_numbers,k1_rcomp_1(A,B)) = k4_subset_1(k1_numbers,k12_prob_1(A),k4_limfunc1(B)) ) ) ) ), file(limfunc1,t25_limfunc1), [interesting(0.00)]). fof(t12_rcomp_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ( r1_xreal_0(A,B) => k2_rcomp_1(B,A) = k1_xboole_0 ) ) ) ), file(rcomp_1,t12_rcomp_1), [interesting(0.00)]). fof(t175_relat_1,theorem,( ! [A,B,C] : ( v1_relat_1(C) => k10_relat_1(C,k2_xboole_0(A,B)) = k2_xboole_0(k10_relat_1(C,A),k10_relat_1(C,B)) ) ), file(relat_1,t175_relat_1), [interesting(0.00)]). fof(t178_relat_1,theorem,( ! [A,B,C] : ( v1_relat_1(C) => ( r1_tarski(A,B) => r1_tarski(k10_relat_1(C,A),k10_relat_1(C,B)) ) ) ), file(relat_1,t178_relat_1), [interesting(0.00)]). fof(t167_relat_1,theorem,( ! [A,B] : ( v1_relat_1(B) => r1_tarski(k10_relat_1(B,A),k1_relat_1(B)) ) ), file(relat_1,t167_relat_1), [interesting(0.00)]). fof(t169_relat_1,theorem,( ! [A] : ( v1_relat_1(A) => k10_relat_1(A,k2_relat_1(A)) = k1_relat_1(A) ) ), file(relat_1,t169_relat_1), [interesting(0.00)]). fof(t9_rfinseq,theorem,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) & v1_finset_1(A) ) => ! [B] : ( ( v1_relat_1(B) & v1_funct_1(B) & v1_finset_1(B) ) => ( r1_rfinseq(A,B) <=> ! [C] : k4_card_1(k10_relat_1(A,C)) = k4_card_1(k10_relat_1(B,C)) ) ) ) ), file(rfinseq,t9_rfinseq), [interesting(0.00)]). fof(t11_rfinseq,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( ( v1_relat_1(B) & v1_funct_1(B) & v1_finset_1(B) ) => ! [C] : ( ( v1_relat_1(C) & v1_funct_1(C) & v1_finset_1(C) ) => ( ( r1_tarski(k2_relat_1(B),A) & r1_tarski(k2_relat_1(C),A) ) => ( r1_rfinseq(B,C) <=> ! [D] : ( m1_subset_1(D,A) => k4_card_1(k10_relat_1(B,k1_tarski(D))) = k4_card_1(k10_relat_1(C,k1_tarski(D))) ) ) ) ) ) ) ), file(rfinseq,t11_rfinseq), [interesting(0.00)]). fof(t137_funct_1,theorem,( ! [A,B,C] : ( ( v1_relat_1(C) & v1_funct_1(C) ) => k10_relat_1(C,k3_xboole_0(A,B)) = k3_xboole_0(k10_relat_1(C,A),k10_relat_1(C,B)) ) ), file(funct_1,t137_funct_1), [interesting(0.00)]). fof(t10_rfinseq,theorem,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) & v1_finset_1(A) ) => ! [B] : ( ( v1_relat_1(B) & v1_funct_1(B) & v1_finset_1(B) ) => ( r1_rfinseq(A,B) => k4_card_1(k1_relat_1(A)) = k4_card_1(k1_relat_1(B)) ) ) ) ), file(rfinseq,t10_rfinseq), [interesting(0.00)]). fof(t46_rfunct_3,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( ~ v1_xboole_0(B) => ! [C] : ( ( v1_funct_1(C) & v1_finset_1(C) & m2_relset_1(C,A,k1_numbers) ) => ! [D] : ( ( v1_funct_1(D) & v1_finset_1(D) & m2_relset_1(D,B,k1_numbers) ) => ( ( r1_rfinseq(k19_rfunct_3(A,C),k19_rfunct_3(B,D)) & r1_rfinseq(k20_rfunct_3(A,C),k20_rfunct_3(B,D)) ) => r1_rfinseq(C,D) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d10_rfunct_3,d11_rfunct_3,t19_limfunc1,t14_rcomp_1,t39_rfunct_3,t42_rfunct_3,t64_card_2,t25_limfunc1,t12_rcomp_1,t175_relat_1,t178_relat_1,t167_relat_1,t169_relat_1,d10_xboole_0,t175_relat_1,t178_relat_1,t167_relat_1,t169_relat_1,d10_xboole_0,t9_rfinseq,t38_rfunct_3,t11_rfinseq,t137_funct_1,t10_rfinseq,t60_xreal_1,t41_rfunct_3,t11_rfinseq,t11_rfinseq]), [file(rfunct_3,t46_rfunct_3),interesting(0.00)]). fof(t68_funct_1,theorem,( ! [A,B] : ( ( v1_relat_1(B) & v1_funct_1(B) ) => ! [C] : ( ( v1_relat_1(C) & v1_funct_1(C) ) => ( B = k7_relat_1(C,A) <=> ( k1_relat_1(B) = k3_xboole_0(k1_relat_1(C),A) & ! [D] : ( r2_hidden(D,k1_relat_1(B)) => k1_funct_1(B,D) = k1_funct_1(C,D) ) ) ) ) ) ), file(funct_1,t68_funct_1), [interesting(0.00)]). fof(d7_seq_1,definition,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) & v1_seq_1(A) ) => ! [B] : ( ( v1_relat_1(B) & v1_funct_1(B) ) => ( B = k15_seq_1(A) <=> ( k1_relat_1(B) = k1_relat_1(A) & ! [C] : ( r2_hidden(C,k1_relat_1(B)) => k1_funct_1(B,C) = k1_real_1(k1_seq_1(A,C)) ) ) ) ) ) ), file(seq_1,d7_seq_1), [interesting(0.00)]). fof(t50_rfunct_3,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( ( v1_funct_1(B) & m2_relset_1(B,A,k1_numbers) ) => ( ! [C] : ( m1_subset_1(C,A) => ( r2_hidden(C,k4_relset_1(A,k1_numbers,B)) => r1_xreal_0(k2_seq_1(A,k1_numbers,B,C),0) ) ) => k20_rfunct_3(A,B) = k16_seq_1(A,k1_numbers,B) ) ) ) ), inference(mizar_proof,[status(thm)],[d11_rfunct_3,d7_seq_1,t26_xreal_1,d11_rfunct_3,d2_square_1,d7_seq_1,t34_partfun1]), [file(rfunct_3,t50_rfunct_3),interesting(0.00)]). fof(d12_rfunct_3,definition,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( ( v1_funct_1(B) & m2_relset_1(B,A,k1_numbers) ) => ! [C] : ( m1_subset_1(C,k1_numbers) => ! [D] : ( ( v1_funct_1(D) & m2_relset_1(D,A,k1_numbers) ) => ( D = k21_rfunct_3(A,B,C) <=> ( k4_relset_1(A,k1_numbers,D) = k4_relset_1(A,k1_numbers,B) & ! [E] : ( m1_subset_1(E,A) => ( r2_hidden(E,k4_relset_1(A,k1_numbers,D)) => k2_seq_1(A,k1_numbers,D,E) = k5_real_1(k2_seq_1(A,k1_numbers,B,E),C) ) ) ) ) ) ) ) ) ), file(rfunct_3,d12_rfunct_3), [interesting(0.00)]). fof(t71_funct_1,theorem,( ! [A,B,C] : ( ( v1_relat_1(C) & v1_funct_1(C) ) => ( r2_hidden(B,k3_xboole_0(k1_relat_1(C),A)) => k1_funct_1(k7_relat_1(C,A),B) = k1_funct_1(C,B) ) ) ), file(funct_1,t71_funct_1), [interesting(0.00)]). fof(t53_rfunct_3,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( ( v1_funct_1(B) & m2_relset_1(B,A,k1_numbers) ) => ! [C] : ( m1_subset_1(C,k1_numbers) => ! [D] : ( m1_subset_1(D,k1_numbers) => k11_relset_1(A,k1_numbers,B,k2_setwiseo(k1_numbers,k3_real_1(D,C))) = k11_relset_1(A,k1_numbers,k21_rfunct_3(A,B,C),k2_setwiseo(k1_numbers,D)) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d3_tarski,d13_funct_1,d12_rfunct_3,d1_tarski,d12_rfunct_3,d1_tarski,d13_funct_1,d10_xboole_0,d3_tarski,d13_funct_1,d12_rfunct_3,d1_tarski,d12_rfunct_3,d1_tarski,d13_funct_1]), [file(rfunct_3,t53_rfunct_3),interesting(0.00)]). fof(d13_rfunct_3,definition,( ! [A] : ( ( v1_funct_1(A) & m2_relset_1(A,k1_numbers,k1_numbers) ) => ! [B] : ( r2_rfunct_3(A,B) <=> ( r1_tarski(B,k4_relset_1(k1_numbers,k1_numbers,A)) & ! [C] : ( m1_subset_1(C,k1_numbers) => ( ( r1_xreal_0(0,C) & r1_xreal_0(C,1) ) => ! [D] : ( m1_subset_1(D,k1_numbers) => ! [E] : ( m1_subset_1(E,k1_numbers) => ( ( r2_hidden(D,B) & r2_hidden(E,B) & r2_hidden(k3_real_1(k4_real_1(C,D),k4_real_1(k5_real_1(1,C),E)),B) ) => r1_xreal_0(k2_seq_1(k1_numbers,k1_numbers,A,k3_real_1(k4_real_1(C,D),k4_real_1(k5_real_1(1,C),E))),k3_real_1(k4_real_1(C,k2_seq_1(k1_numbers,k1_numbers,A,D)),k4_real_1(k5_real_1(1,C),k2_seq_1(k1_numbers,k1_numbers,A,E)))) ) ) ) ) ) ) ) ) ), file(rfunct_3,d13_rfunct_3), [interesting(0.00)]). fof(t105_real_2,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ! [C] : ( v1_xreal_0(C) => ( ~ ( ~ r1_xreal_0(k2_xcmplx_0(A,k4_xcmplx_0(B)),0) & ~ r1_xreal_0(0,k6_xcmplx_0(B,A)) & ~ r1_xreal_0(0,k2_xcmplx_0(B,k4_xcmplx_0(A))) & ~ r1_xreal_0(k6_xcmplx_0(A,C),k2_xcmplx_0(B,k4_xcmplx_0(C))) & ~ r1_xreal_0(k2_xcmplx_0(A,k4_xcmplx_0(C)),k6_xcmplx_0(B,C)) & ~ r1_xreal_0(k6_xcmplx_0(C,B),k6_xcmplx_0(C,A)) ) => r1_xreal_0(A,B) ) ) ) ) ), file(real_2,t105_real_2), [interesting(0.00)]). fof(t52_xreal_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ~ ( ~ r1_xreal_0(B,A) & r1_xreal_0(k6_xcmplx_0(B,A),0) ) ) ) ), file(xreal_1,t52_xreal_1), [interesting(0.00)]). fof(t63_xcmplx_1,theorem,( ! [A] : ( v1_xcmplx_0(A) => ! [B] : ( v1_xcmplx_0(B) => ! [C] : ( v1_xcmplx_0(C) => k2_xcmplx_0(k7_xcmplx_0(A,B),k7_xcmplx_0(C,B)) = k7_xcmplx_0(k2_xcmplx_0(A,C),B) ) ) ) ), file(xcmplx_1,t63_xcmplx_1), [interesting(0.00)]). fof(t60_xcmplx_1,theorem,( ! [A] : ( v1_xcmplx_0(A) => ( A != 0 => k7_xcmplx_0(A,A) = 1 ) ) ), file(xcmplx_1,t60_xcmplx_1), [interesting(0.00)]). fof(t75_xcmplx_1,theorem,( ! [A] : ( v1_xcmplx_0(A) => ! [B] : ( v1_xcmplx_0(B) => ! [C] : ( v1_xcmplx_0(C) => k3_xcmplx_0(A,k7_xcmplx_0(B,C)) = k7_xcmplx_0(k3_xcmplx_0(A,B),C) ) ) ) ), file(xcmplx_1,t75_xcmplx_1), [interesting(0.00)]). fof(t127_real_2,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ~ ( ( ( ~ r1_xreal_0(A,0) & ~ r1_xreal_0(B,0) ) | ( ~ r1_xreal_0(0,A) & ~ r1_xreal_0(0,B) ) ) & r1_xreal_0(k7_xcmplx_0(A,B),0) ) ) ) ), file(real_2,t127_real_2), [interesting(0.00)]). fof(t174_real_2,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ( ( r1_xreal_0(A,0) => ( r1_xreal_0(k2_xcmplx_0(A,B),B) & r1_xreal_0(B,k6_xcmplx_0(B,A)) ) ) & ( ( r1_xreal_0(k2_xcmplx_0(A,B),B) | r1_xreal_0(B,k6_xcmplx_0(B,A)) ) => r1_xreal_0(A,0) ) ) ) ) ), file(real_2,t174_real_2), [interesting(0.00)]). fof(t23_xreal_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ! [C] : ( v1_xreal_0(C) => ! [D] : ( v1_xreal_0(D) => ( r1_xreal_0(k2_xcmplx_0(A,B),k2_xcmplx_0(C,D)) <=> r1_xreal_0(k6_xcmplx_0(A,C),k6_xcmplx_0(D,B)) ) ) ) ) ) ), file(xreal_1,t23_xreal_1), [interesting(0.00)]). fof(d9_xcmplx_0,definition,( ! [A] : ( v1_xcmplx_0(A) => ! [B] : ( v1_xcmplx_0(B) => k7_xcmplx_0(A,B) = k3_xcmplx_0(A,k5_xcmplx_0(B)) ) ) ), file(xcmplx_0,d9_xcmplx_0), [interesting(0.00)]). fof(t67_xreal_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ! [C] : ( v1_xreal_0(C) => ( ( r1_xreal_0(A,B) & r1_xreal_0(C,0) ) => r1_xreal_0(k3_xcmplx_0(B,C),k3_xcmplx_0(A,C)) ) ) ) ) ), file(xreal_1,t67_xreal_1), [interesting(0.00)]). fof(d7_xcmplx_0,definition,( ! [A] : ( v1_xcmplx_0(A) => ! [B] : ( v1_xcmplx_0(B) => ( ( A != 0 => ( B = k5_xcmplx_0(A) <=> k3_xcmplx_0(A,B) = 1 ) ) & ( A = 0 => ( B = k5_xcmplx_0(A) <=> B = 0 ) ) ) ) ) ), file(xcmplx_0,d7_xcmplx_0), [interesting(0.00)]). fof(t187_real_2,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ! [C] : ( v1_xreal_0(C) => ! [D] : ( v1_xreal_0(D) => ( r1_xreal_0(k3_xcmplx_0(C,B),k3_xcmplx_0(D,A)) => ( ( ~ ( ~ r1_xreal_0(A,0) & ~ r1_xreal_0(B,0) ) & ~ ( ~ r1_xreal_0(0,A) & ~ r1_xreal_0(0,B) ) ) | r1_xreal_0(k7_xcmplx_0(C,A),k7_xcmplx_0(D,B)) ) ) ) ) ) ) ), file(real_2,t187_real_2), [interesting(0.00)]). fof(t50_xreal_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ( r1_xreal_0(A,B) => r1_xreal_0(0,k6_xcmplx_0(B,A)) ) ) ) ), file(xreal_1,t50_xreal_1), [interesting(0.00)]). fof(d1_rcomp_1,definition,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => k1_rcomp_1(A,B) = a_2_0_rcomp_1(A,B) ) ) ), file(rcomp_1,d1_rcomp_1), [interesting(0.00)]). fof(t66_xreal_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ! [C] : ( v1_xreal_0(C) => ( ( r1_xreal_0(A,B) & r1_xreal_0(0,C) ) => r1_xreal_0(k3_xcmplx_0(A,C),k3_xcmplx_0(B,C)) ) ) ) ) ), file(xreal_1,t66_xreal_1), [interesting(0.00)]). fof(t9_xreal_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ! [C] : ( v1_xreal_0(C) => ! [D] : ( v1_xreal_0(D) => ( ( r1_xreal_0(A,B) & r1_xreal_0(C,D) ) => r1_xreal_0(k2_xcmplx_0(A,C),k2_xcmplx_0(B,D)) ) ) ) ) ) ), file(xreal_1,t9_xreal_1), [interesting(0.00)]). fof(t26_xcmplx_1,theorem,( ! [A] : ( v1_xcmplx_0(A) => ! [B] : ( v1_xcmplx_0(B) => A = k6_xcmplx_0(k2_xcmplx_0(A,B),B) ) ) ), file(xcmplx_1,t26_xcmplx_1), [interesting(0.00)]). fof(t70_xreal_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ! [C] : ( v1_xreal_0(C) => ~ ( ~ r1_xreal_0(A,0) & ~ r1_xreal_0(C,B) & r1_xreal_0(k3_xcmplx_0(C,A),k3_xcmplx_0(B,A)) ) ) ) ) ), file(xreal_1,t70_xreal_1), [interesting(0.00)]). fof(t10_xreal_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ! [C] : ( v1_xreal_0(C) => ! [D] : ( v1_xreal_0(D) => ~ ( ~ r1_xreal_0(B,A) & r1_xreal_0(C,D) & r1_xreal_0(k2_xcmplx_0(B,D),k2_xcmplx_0(A,C)) ) ) ) ) ) ), file(xreal_1,t10_xreal_1), [interesting(0.00)]). fof(t185_real_2,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ! [C] : ( v1_xreal_0(C) => ! [D] : ( v1_xreal_0(D) => ~ ( ( ( ~ r1_xreal_0(A,0) & ~ r1_xreal_0(B,0) ) | ( ~ r1_xreal_0(0,A) & ~ r1_xreal_0(0,B) ) ) & ~ r1_xreal_0(k3_xcmplx_0(D,A),k3_xcmplx_0(C,B)) & r1_xreal_0(k7_xcmplx_0(D,B),k7_xcmplx_0(C,A)) ) ) ) ) ) ), file(real_2,t185_real_2), [interesting(0.00)]). fof(t74_real_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ! [C] : ( v1_xreal_0(C) => ( ~ r1_xreal_0(0,A) => ( ~ ( ~ r1_xreal_0(C,B) & r1_xreal_0(k7_xcmplx_0(B,A),k7_xcmplx_0(C,A)) ) & ~ ( ~ r1_xreal_0(k7_xcmplx_0(B,A),k7_xcmplx_0(C,A)) & r1_xreal_0(C,B) ) ) ) ) ) ) ), file(real_1,t74_real_1), [interesting(0.00)]). fof(t22_xreal_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ! [C] : ( v1_xreal_0(C) => ( r1_xreal_0(A,k2_xcmplx_0(B,C)) <=> r1_xreal_0(k6_xcmplx_0(A,B),C) ) ) ) ) ), file(xreal_1,t22_xreal_1), [interesting(0.00)]). fof(t55_rfunct_3,theorem,( ! [A] : ( m1_subset_1(A,k1_numbers) => ! [B] : ( m1_subset_1(B,k1_numbers) => ! [C] : ( ( v1_funct_1(C) & m2_relset_1(C,k1_numbers,k1_numbers) ) => ( r2_rfunct_3(C,k1_rcomp_1(A,B)) <=> ( r1_tarski(k1_rcomp_1(A,B),k4_relset_1(k1_numbers,k1_numbers,C)) & ! [D] : ( m1_subset_1(D,k1_numbers) => ( ( r1_xreal_0(0,D) & r1_xreal_0(D,1) ) => ! [E] : ( m1_subset_1(E,k1_numbers) => ! [F] : ( m1_subset_1(F,k1_numbers) => ( ( r2_hidden(E,k1_rcomp_1(A,B)) & r2_hidden(F,k1_rcomp_1(A,B)) ) => r1_xreal_0(k2_seq_1(k1_numbers,k1_numbers,C,k3_real_1(k4_real_1(D,E),k4_real_1(k5_real_1(1,D),F))),k3_real_1(k4_real_1(D,k2_seq_1(k1_numbers,k1_numbers,C,E)),k4_real_1(k5_real_1(1,D),k2_seq_1(k1_numbers,k1_numbers,C,F)))) ) ) ) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d1_rcomp_1,d13_rfunct_3,t50_xreal_1,t66_xreal_1,t66_xreal_1,t9_xreal_1,t9_xreal_1,d13_rfunct_3,d13_rfunct_3]), [file(rfunct_3,t55_rfunct_3),interesting(0.00)]). fof(t1_xboole_1,theorem,( ! [A,B,C] : ( ( r1_tarski(A,B) & r1_tarski(B,C) ) => r1_tarski(A,C) ) ), file(xboole_1,t1_xboole_1), [interesting(0.00)]). fof(t11_xreal_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ! [C] : ( v1_xreal_0(C) => ( r1_xreal_0(A,B) <=> r1_xreal_0(k6_xcmplx_0(A,C),k6_xcmplx_0(B,C)) ) ) ) ) ), file(xreal_1,t11_xreal_1), [interesting(0.00)]). fof(t73_real_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ! [C] : ( v1_xreal_0(C) => ( ~ r1_xreal_0(A,0) => ( ~ ( ~ r1_xreal_0(C,B) & r1_xreal_0(k7_xcmplx_0(C,A),k7_xcmplx_0(B,A)) ) & ~ ( ~ r1_xreal_0(k7_xcmplx_0(C,A),k7_xcmplx_0(B,A)) & r1_xreal_0(C,B) ) ) ) ) ) ) ), file(real_1,t73_real_1), [interesting(0.00)]). fof(t19_xboole_1,theorem,( ! [A,B,C] : ( ( r1_tarski(A,B) & r1_tarski(A,C) ) => r1_tarski(A,k3_xboole_0(B,C)) ) ), file(xboole_1,t19_xboole_1), [interesting(0.00)]). fof(t50_square_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ! [C] : ( v1_xreal_0(C) => ( ( r1_xreal_0(A,B) & r1_xreal_0(C,B) ) <=> r1_xreal_0(k2_square_1(A,C),B) ) ) ) ) ), file(square_1,t50_square_1), [interesting(0.00)]). fof(t129_xreal_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ( ( r1_xreal_0(0,A) & r1_xreal_0(0,B) ) => r1_xreal_0(0,k3_xcmplx_0(A,B)) ) ) ) ), file(xreal_1,t129_xreal_1), [interesting(0.00)]). fof(t133_xreal_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ( ( r1_xreal_0(0,A) & r1_xreal_0(B,0) ) => r1_xreal_0(k3_xcmplx_0(A,B),0) ) ) ) ), file(xreal_1,t133_xreal_1), [interesting(0.00)]). fof(t34_funct_1,theorem,( ! [A,B] : ( ( v1_relat_1(B) & v1_funct_1(B) ) => ( B = k6_relat_1(A) <=> ( k1_relat_1(B) = A & ! [C] : ( r2_hidden(C,A) => k1_funct_1(B,C) = C ) ) ) ) ), file(funct_1,t34_funct_1), [interesting(0.00)]). fof(t59_card_2,theorem,( ! [A] : ( k1_card_1(A) = 0 => A = k1_xboole_0 ) ), file(card_2,t59_card_2), [interesting(0.00)]). fof(d14_rfunct_3,definition,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( ( v1_funct_1(B) & m2_relset_1(B,A,k1_numbers) ) => ! [C] : ( v1_finset_1(k4_relset_1(A,k1_numbers,k2_partfun1(A,k1_numbers,B,C))) => ! [D] : ( ( v1_rfinseq(D) & m2_finseq_1(D,k1_numbers) ) => ( D = k22_rfunct_3(A,B,C) <=> r1_rfinseq(k2_partfun1(A,k1_numbers,B,C),D) ) ) ) ) ) ), file(rfunct_3,d14_rfunct_3), [interesting(0.00)]). fof(t66_rfunct_3,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( ( v1_funct_1(B) & m2_relset_1(B,A,k1_numbers) ) => ! [C] : ( v1_finset_1(k4_relset_1(A,k1_numbers,k2_partfun1(A,k1_numbers,B,C))) => k22_rfunct_3(A,B,k4_relset_1(A,k1_numbers,k2_partfun1(A,k1_numbers,B,C))) = k22_rfunct_3(A,B,C) ) ) ) ), inference(mizar_proof,[status(thm)],[d14_rfunct_3,t68_funct_1,t100_relat_1,t97_relat_1,d14_rfunct_3]), [file(rfunct_3,t66_rfunct_3),interesting(0.00)]). fof(t29_finset_1,theorem,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) ) => ( v1_finset_1(k1_relat_1(A)) <=> v1_finset_1(A) ) ) ), file(finset_1,t29_finset_1), [interesting(0.00)]). fof(t78_finseq_1,theorem, ( ! [A] : ( v4_ordinal2(A) => k4_card_1(k2_finseq_1(A)) = A ) & ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ( k4_card_1(A) = A & k4_card_1(k1_card_1(A)) = A ) ) ), file(finseq_1,t78_finseq_1), [interesting(0.00)]). fof(t78_card_1,theorem,( k4_card_1(k1_xboole_0) = 0 ), file(card_1,t78_card_1), [interesting(0.00)]). fof(t50_xboole_1,theorem,( ! [A,B,C] : k3_xboole_0(A,k4_xboole_0(B,C)) = k4_xboole_0(k3_xboole_0(A,B),k3_xboole_0(A,C)) ), file(xboole_1,t50_xboole_1), [interesting(0.00)]). fof(t47_finseq_1,theorem,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) & v1_finseq_1(A) ) => ( k7_finseq_1(A,k1_xboole_0) = A & k7_finseq_1(k1_xboole_0,A) = A ) ) ), file(finseq_1,t47_finseq_1), [interesting(0.00)]). fof(t36_xboole_1,theorem,( ! [A,B] : r1_tarski(k4_xboole_0(A,B),A) ), file(xboole_1,t36_xboole_1), [interesting(0.00)]). fof(t26_xboole_1,theorem,( ! [A,B,C] : ( r1_tarski(A,B) => r1_tarski(k3_xboole_0(A,C),k3_xboole_0(B,C)) ) ), file(xboole_1,t26_xboole_1), [interesting(0.00)]). fof(t13_finset_1,theorem,( ! [A,B] : ( ( r1_tarski(A,B) & v1_finset_1(B) ) => v1_finset_1(A) ) ), file(finset_1,t13_finset_1), [interesting(0.00)]). fof(t37_zfmisc_1,theorem,( ! [A,B] : ( r1_tarski(k1_tarski(A),B) <=> r2_hidden(A,B) ) ), file(zfmisc_1,t37_zfmisc_1), [interesting(0.00)]). fof(d4_xboole_0,definition,( ! [A,B,C] : ( C = k4_xboole_0(A,B) <=> ! [D] : ( r2_hidden(D,C) <=> ( r2_hidden(D,A) & ~ r2_hidden(D,B) ) ) ) ), file(xboole_0,d4_xboole_0), [interesting(0.00)]). fof(t63_card_2,theorem,( ! [A] : ( v1_finset_1(A) => ! [B] : ( v1_finset_1(B) => ( r1_tarski(B,A) => k4_card_1(k4_xboole_0(A,B)) = k5_real_1(k4_card_1(A),k4_card_1(B)) ) ) ) ), file(card_2,t63_card_2), [interesting(0.00)]). fof(t79_card_1,theorem,( ! [A] : k4_card_1(k1_tarski(A)) = 1 ), file(card_1,t79_card_1), [interesting(0.00)]). fof(t52_xboole_1,theorem,( ! [A,B,C] : k4_xboole_0(A,k4_xboole_0(B,C)) = k2_xboole_0(k4_xboole_0(A,B),k3_xboole_0(A,C)) ), file(xboole_1,t52_xboole_1), [interesting(0.00)]). fof(t23_xboole_1,theorem,( ! [A,B,C] : k3_xboole_0(A,k2_xboole_0(B,C)) = k2_xboole_0(k3_xboole_0(A,B),k3_xboole_0(A,C)) ), file(xboole_1,t23_xboole_1), [interesting(0.00)]). fof(t32_rfinseq,theorem,( ! [A] : ( m2_finseq_1(A,k1_numbers) => ( v1_rfinseq(A) <=> ! [B] : ( m2_subset_1(B,k1_numbers,k5_numbers) => ! [C] : ( m2_subset_1(C,k1_numbers,k5_numbers) => ( ( r2_hidden(B,k4_finseq_1(A)) & r2_hidden(C,k4_finseq_1(A)) ) => ( r1_xreal_0(C,B) | r1_xreal_0(k2_seq_1(k5_numbers,k1_numbers,A,C),k2_seq_1(k5_numbers,k1_numbers,A,B)) ) ) ) ) ) ) ), file(rfinseq,t32_rfinseq), [interesting(0.00)]). fof(d2_xboole_0,definition,( ! [A,B,C] : ( C = k2_xboole_0(A,B) <=> ! [D] : ( r2_hidden(D,C) <=> ( r2_hidden(D,A) | r2_hidden(D,B) ) ) ) ), file(xboole_0,d2_xboole_0), [interesting(0.00)]). fof(t41_xboole_1,theorem,( ! [A,B,C] : k4_xboole_0(k4_xboole_0(A,B),C) = k4_xboole_0(A,k2_xboole_0(B,C)) ), file(xboole_1,t41_xboole_1), [interesting(0.00)]). fof(t39_xboole_1,theorem,( ! [A,B] : k2_xboole_0(A,k4_xboole_0(B,A)) = k2_xboole_0(A,B) ), file(xboole_1,t39_xboole_1), [interesting(0.00)]). fof(t12_xboole_1,theorem,( ! [A,B] : ( r1_tarski(A,B) => k2_xboole_0(A,B) = B ) ), file(xboole_1,t12_xboole_1), [interesting(0.00)]). fof(t14_finset_1,theorem,( ! [A,B] : ( ( v1_finset_1(A) & v1_finset_1(B) ) => v1_finset_1(k2_xboole_0(A,B)) ) ), file(finset_1,t14_finset_1), [interesting(0.00)]). fof(t16_finset_1,theorem,( ! [A,B] : ( v1_finset_1(A) => v1_finset_1(k4_xboole_0(A,B)) ) ), file(finset_1,t16_finset_1), [interesting(0.00)]). fof(t79_xboole_1,theorem,( ! [A,B] : r1_xboole_0(k4_xboole_0(A,B),B) ), file(xboole_1,t79_xboole_1), [interesting(0.00)]). fof(t139_funct_1,theorem,( ! [A,B,C] : ( v1_relat_1(C) => k10_relat_1(k7_relat_1(C,A),B) = k3_xboole_0(A,k10_relat_1(C,B)) ) ), file(funct_1,t139_funct_1), [interesting(0.00)]). fof(t16_xboole_1,theorem,( ! [A,B,C] : k3_xboole_0(k3_xboole_0(A,B),C) = k3_xboole_0(A,k3_xboole_0(B,C)) ), file(xboole_1,t16_xboole_1), [interesting(0.00)]). fof(t91_relat_1,theorem,( ! [A,B] : ( v1_relat_1(B) => ( r1_tarski(A,k1_relat_1(B)) => k1_relat_1(k7_relat_1(B,A)) = A ) ) ), file(relat_1,t91_relat_1), [interesting(0.00)]). fof(t55_finseq_1,theorem,( ! [A,B] : ( ( v1_relat_1(B) & v1_funct_1(B) & v1_finseq_1(B) ) => ( B = k9_finseq_1(A) <=> ( k4_finseq_1(B) = k2_finseq_1(1) & k2_relat_1(B) = k1_tarski(A) ) ) ) ), file(finseq_1,t55_finseq_1), [interesting(0.00)]). fof(t68_rfunct_3,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( m1_subset_1(B,A) => ! [C,D] : ( ( v1_funct_1(D) & m2_relset_1(D,A,k1_numbers) ) => ( ( v1_finset_1(C) & r2_hidden(B,k4_relset_1(A,k1_numbers,k2_partfun1(A,k1_numbers,D,C))) ) => r1_rfinseq(k8_finseq_1(k1_numbers,k22_rfunct_3(A,D,k4_xboole_0(C,k2_setwiseo(A,B))),k12_finseq_1(k1_numbers,k2_seq_1(A,k1_numbers,D,B))),k2_partfun1(A,k1_numbers,D,C)) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d14_rfunct_3,t68_funct_1,d3_xboole_0,t37_zfmisc_1,d1_rfinseq,t79_xboole_1,t139_funct_1,t139_funct_1,t16_xboole_1,t16_xboole_1,d7_xboole_0,t139_funct_1,t139_funct_1,t23_xboole_1,t39_xboole_1,t12_xboole_1,t139_funct_1,t91_relat_1,t4_finseq_1,t55_finseq_1,t167_relat_1,d3_tarski,d1_tarski,t68_funct_1,d1_tarski,d13_funct_1,d10_xboole_0,t79_card_1,t167_relat_1,d3_tarski,d1_tarski,t57_finseq_1,d1_tarski,d13_funct_1,d10_xboole_0,t79_card_1,d13_funct_1,d1_tarski,t68_funct_1,d13_funct_1,d1_tarski,t57_finseq_1,t64_card_2,t78_card_1,t63_finseq_3,d1_rfinseq]), [file(rfunct_3,t68_rfunct_3),interesting(0.00)]). fof(t15_rfinseq,theorem,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) & v1_finseq_1(A) ) => ! [B] : ( ( v1_relat_1(B) & v1_funct_1(B) & v1_finseq_1(B) ) => r1_rfinseq(k7_finseq_1(A,B),k7_finseq_1(B,A)) ) ) ), file(rfinseq,t15_rfinseq), [interesting(0.00)]). fof(t2_rfinseq,theorem,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) ) => ! [B] : ( ( v1_relat_1(B) & v1_funct_1(B) ) => ! [C] : ( ( v1_relat_1(C) & v1_funct_1(C) ) => ( ( r1_rfinseq(A,B) & r1_rfinseq(A,C) ) => r1_rfinseq(B,C) ) ) ) ) ), file(rfinseq,t2_rfinseq), [interesting(0.00)]). fof(d4_rfinseq,definition,( ! [A] : ( m2_finseq_1(A,k1_numbers) => ( v1_rfinseq(A) <=> ! [B] : ( m2_subset_1(B,k1_numbers,k5_numbers) => ( ( r2_hidden(B,k4_finseq_1(A)) & r2_hidden(k1_nat_1(B,1),k4_finseq_1(A)) ) => r1_xreal_0(k2_seq_1(k5_numbers,k1_numbers,A,k1_nat_1(B,1)),k2_seq_1(k5_numbers,k1_numbers,A,B)) ) ) ) ) ), file(rfinseq,d4_rfinseq), [interesting(0.00)]). fof(t35_finseq_1,theorem,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) & v1_finseq_1(A) ) => ! [B] : ( ( v1_relat_1(B) & v1_funct_1(B) & v1_finseq_1(B) ) => k3_finseq_1(k7_finseq_1(A,B)) = k1_nat_1(k3_finseq_1(A),k3_finseq_1(B)) ) ) ), file(finseq_1,t35_finseq_1), [interesting(0.00)]). fof(t37_finseq_1,theorem,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) & v1_finseq_1(A) ) => ! [B] : ( ( v1_relat_1(B) & v1_funct_1(B) & v1_finseq_1(B) ) => ! [C] : ( v4_ordinal2(C) => ( r1_xreal_0(C,k3_finseq_1(k7_finseq_1(A,B))) => ( r1_xreal_0(C,k3_finseq_1(A)) | k1_funct_1(k7_finseq_1(A,B),C) = k1_funct_1(B,k6_xcmplx_0(C,k3_finseq_1(A))) ) ) ) ) ) ), file(finseq_1,t37_finseq_1), [interesting(0.00)]). fof(t58_finseq_1,theorem,( ! [A,B] : ( ( v1_relat_1(B) & v1_funct_1(B) & v1_finseq_1(B) ) => k1_funct_1(k7_finseq_1(k9_finseq_1(A),B),1) = A ) ), file(finseq_1,t58_finseq_1), [interesting(0.00)]). fof(t36_rfinseq,theorem,( ! [A] : ( ( v1_rfinseq(A) & m2_finseq_1(A,k1_numbers) ) => ! [B] : ( ( v1_rfinseq(B) & m2_finseq_1(B,k1_numbers) ) => ( r1_rfinseq(A,B) => A = B ) ) ) ), file(rfinseq,t36_rfinseq), [interesting(0.00)]). fof(t45_finseq_1,theorem,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) & v1_finseq_1(A) ) => ! [B] : ( ( v1_relat_1(B) & v1_funct_1(B) & v1_finseq_1(B) ) => ! [C] : ( ( v1_relat_1(C) & v1_funct_1(C) & v1_finseq_1(C) ) => k7_finseq_1(k7_finseq_1(A,B),C) = k7_finseq_1(A,k7_finseq_1(B,C)) ) ) ) ), file(finseq_1,t45_finseq_1), [interesting(0.00)]). fof(t14_rfinseq,theorem,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) & v1_finseq_1(A) ) => ! [B] : ( ( v1_relat_1(B) & v1_funct_1(B) & v1_finseq_1(B) ) => ! [C] : ( ( v1_relat_1(C) & v1_funct_1(C) & v1_finseq_1(C) ) => ( r1_rfinseq(A,B) <=> r1_rfinseq(k7_finseq_1(A,C),k7_finseq_1(B,C)) ) ) ) ) ), file(rfinseq,t14_rfinseq), [interesting(0.00)]). fof(t33_rfinseq,theorem,( ! [A] : ( ( v1_rfinseq(A) & m2_finseq_1(A,k1_numbers) ) => ! [B] : ( m2_subset_1(B,k1_numbers,k5_numbers) => ( v1_rfinseq(k16_finseq_1(k1_numbers,A,B)) & m2_finseq_1(k16_finseq_1(k1_numbers,A,B),k1_numbers) ) ) ) ), file(rfinseq,t33_rfinseq), [interesting(0.00)]). fof(l91_rfunct_3,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ( ! [B] : ( ~ v1_xboole_0(B) => ! [C] : ( ( v1_funct_1(C) & m2_relset_1(C,B,k1_numbers) ) => ! [D,E,F] : ( v1_finset_1(F) => ( ( F = k4_relset_1(B,k1_numbers,k2_partfun1(B,k1_numbers,C,E)) & v1_finset_1(k4_relset_1(B,k1_numbers,k2_partfun1(B,k1_numbers,C,D))) & r1_tarski(E,D) & A = k4_card_1(F) & ! [G] : ( m1_subset_1(G,B) => ! [H] : ( m1_subset_1(H,B) => ( ( r2_hidden(G,k4_relset_1(B,k1_numbers,k2_partfun1(B,k1_numbers,C,E))) & r2_hidden(H,k4_relset_1(B,k1_numbers,k2_partfun1(B,k1_numbers,C,k4_xboole_0(D,E)))) ) => r1_xreal_0(k2_seq_1(B,k1_numbers,C,H),k2_seq_1(B,k1_numbers,C,G)) ) ) ) ) => k22_rfunct_3(B,C,D) = k8_finseq_1(k1_numbers,k22_rfunct_3(B,C,E),k22_rfunct_3(B,C,k4_xboole_0(D,E))) ) ) ) ) => ! [B] : ( ~ v1_xboole_0(B) => ! [C] : ( ( v1_funct_1(C) & m2_relset_1(C,B,k1_numbers) ) => ! [D,E,F] : ( v1_finset_1(F) => ( ( F = k4_relset_1(B,k1_numbers,k2_partfun1(B,k1_numbers,C,E)) & v1_finset_1(k4_relset_1(B,k1_numbers,k2_partfun1(B,k1_numbers,C,D))) & r1_tarski(E,D) & k1_nat_1(A,1) = k4_card_1(F) & ! [G] : ( m1_subset_1(G,B) => ! [H] : ( m1_subset_1(H,B) => ( ( r2_hidden(G,k4_relset_1(B,k1_numbers,k2_partfun1(B,k1_numbers,C,E))) & r2_hidden(H,k4_relset_1(B,k1_numbers,k2_partfun1(B,k1_numbers,C,k4_xboole_0(D,E)))) ) => r1_xreal_0(k2_seq_1(B,k1_numbers,C,H),k2_seq_1(B,k1_numbers,C,G)) ) ) ) ) => k22_rfunct_3(B,C,D) = k8_finseq_1(k1_numbers,k22_rfunct_3(B,C,E),k22_rfunct_3(B,C,k4_xboole_0(D,E))) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t36_xboole_1,t68_funct_1,t26_xboole_1,t13_finset_1,d14_rfunct_3,t1_rfinseq,t38_nat_1,t70_rfunct_3,t27_finseq_3,d5_funct_1,t26_partfun1,t68_funct_1,t68_funct_1,d3_xboole_0,t37_zfmisc_1,d3_tarski,d3_xboole_0,d4_xboole_0,d3_xboole_0,d4_xboole_0,d10_xboole_0,d3_tarski,d4_xboole_0,d3_xboole_0,d4_xboole_0,d3_xboole_0,t63_card_2,t79_card_1,t36_xboole_1,t1_xboole_1,t37_zfmisc_1,t52_xboole_1,t28_xboole_1,t23_xboole_1,t28_xboole_1,d4_xboole_0,d1_tarski,d5_funct_1,t68_funct_1,t11_finseq_2,t27_finseq_3,t68_funct_1,d5_real_1,t32_rfinseq,d2_xboole_0,t41_xboole_1,t39_xboole_1,t12_xboole_1,t14_finset_1,d1_tarski,d2_xboole_0,d3_xboole_0,t69_rfunct_3,t15_rfinseq,t2_rfinseq,d14_rfunct_3,t2_rfinseq,d4_rfinseq,t57_finseq_1,t27_finseq_3,t4_finseq_2,t5_finseq_2,t35_finseq_1,t11_xreal_1,t38_nat_1,t21_xreal_1,t2_xreal_1,t27_finseq_3,t37_finseq_1,d5_funct_1,t26_partfun1,t68_funct_1,t58_finseq_1,d5_real_1,t37_finseq_1,t38_nat_1,t21_xreal_1,t27_finseq_3,d4_rfinseq,t36_rfinseq,t45_finseq_1,t69_rfunct_3,t2_rfinseq,t20_rfinseq,t14_rfinseq,t33_rfinseq,t36_rfinseq]), [file(rfunct_3,l91_rfunct_3),interesting(0.00)]). fof(t104_relat_1,theorem,( ! [A,B,C] : ( v1_relat_1(C) => ( r1_tarski(A,B) => r1_tarski(k7_relat_1(C,A),k7_relat_1(C,B)) ) ) ), file(relat_1,t104_relat_1), [interesting(0.00)]). fof(t25_relat_1,theorem,( ! [A] : ( v1_relat_1(A) => ! [B] : ( v1_relat_1(B) => ( r1_tarski(A,B) => ( r1_tarski(k1_relat_1(A),k1_relat_1(B)) & r1_tarski(k2_relat_1(A),k2_relat_1(B)) ) ) ) ) ), file(relat_1,t25_relat_1), [interesting(0.00)]). fof(t101_relat_1,theorem,( ! [A,B] : ( v1_relat_1(B) => k7_relat_1(k7_relat_1(B,A),A) = k7_relat_1(B,A) ) ), file(relat_1,t101_relat_1), [interesting(0.00)]). fof(t15_funcop_1,theorem,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) ) => ! [B] : ( k2_relat_1(A) = k1_tarski(B) => A = k2_funcop_1(k1_relat_1(A),B) ) ) ), file(funcop_1,t15_funcop_1), [interesting(0.00)]). fof(d2_finseq_2,definition,( ! [A] : ( v4_ordinal2(A) => ! [B] : k2_finseq_2(A,B) = k2_funcop_1(k2_finseq_1(A),B) ) ), file(finseq_2,d2_finseq_2), [interesting(0.00)]). fof(t40_rfunct_1,theorem,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) & v1_seq_1(A) ) => ! [B] : ( ( v1_relat_1(B) & v1_funct_1(B) & v1_seq_1(B) ) => k4_seq_1(A,B) = k3_seq_1(A,k15_seq_1(B)) ) ) ), file(rfunct_1,t40_rfunct_1), [interesting(0.00)]). fof(t65_relat_1,theorem,( ! [A] : ( v1_relat_1(A) => ( k1_relat_1(A) = k1_xboole_0 <=> k2_relat_1(A) = k1_xboole_0 ) ) ), file(relat_1,t65_relat_1), [interesting(0.00)]). fof(t27_finseq_1,theorem,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) & v1_finseq_1(A) ) => ( A = k1_xboole_0 <=> k2_relat_1(A) = k1_xboole_0 ) ) ), file(finseq_1,t27_finseq_1), [interesting(0.00)]). fof(t60_rfunct_1,theorem,( ! [A,B] : ( ( v1_relat_1(B) & v1_funct_1(B) & v1_seq_1(B) ) => ! [C] : ( ( v1_relat_1(C) & v1_funct_1(C) & v1_seq_1(C) ) => ( k7_relat_1(k3_seq_1(B,C),A) = k3_seq_1(k7_relat_1(B,A),k7_relat_1(C,A)) & k7_relat_1(k3_seq_1(B,C),A) = k3_seq_1(k7_relat_1(B,A),C) & k7_relat_1(k3_seq_1(B,C),A) = k3_seq_1(B,k7_relat_1(C,A)) ) ) ) ), file(rfunct_1,t60_rfunct_1), [interesting(0.00)]). fof(t47_card_1,theorem,( k1_card_1(k1_xboole_0) = k1_xboole_0 ), file(card_1,t47_card_1), [interesting(0.00)]). fof(t22_rfinseq,theorem,( ! [A] : ( m2_finseq_1(A,k1_numbers) => ! [B] : ( m2_finseq_1(B,k1_numbers) => ( r1_rfinseq(A,B) => k15_rvsum_1(A) = k15_rvsum_1(B) ) ) ) ), file(rfinseq,t22_rfinseq), [interesting(0.00)]). fof(t18_rfinseq,theorem,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) ) => ! [B] : ( v1_finset_1(B) => ? [C] : ( v1_relat_1(C) & v1_funct_1(C) & v1_finseq_1(C) & r1_rfinseq(k7_relat_1(A,B),C) ) ) ) ), file(rfinseq,t18_rfinseq), [interesting(0.00)]). fof(t76_funct_1,theorem,( ! [A,B] : ( ( v1_relat_1(B) & v1_funct_1(B) ) => ( r1_tarski(k1_relat_1(k7_relat_1(B,A)),k1_relat_1(B)) & r1_tarski(k2_relat_1(k7_relat_1(B,A)),k2_relat_1(B)) ) ) ), file(funct_1,t76_funct_1), [interesting(0.00)]). fof(d4_finseq_1,definition,( ! [A,B] : ( ( v1_relat_1(B) & v1_funct_1(B) & v1_finseq_1(B) ) => ( m1_finseq_1(B,A) <=> r1_tarski(k2_relat_1(B),A) ) ) ), file(finseq_1,d4_finseq_1), [interesting(0.00)]). fof(t65_rfunct_1,theorem,( ! [A,B] : ( ( v1_relat_1(B) & v1_funct_1(B) & v1_seq_1(B) ) => ! [C] : ( v1_xreal_0(C) => k7_relat_1(k12_seq_1(B,C),A) = k12_seq_1(k7_relat_1(B,A),C) ) ) ), file(rfunct_1,t65_rfunct_1), [interesting(0.00)]). fof(d7_rvsum_1,definition,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( m2_finseq_1(B,k1_numbers) => k9_rvsum_1(A,B) = k5_finseqop(k1_numbers,k1_numbers,B,k2_rvsum_1(A)) ) ) ), file(rvsum_1,d7_rvsum_1), [interesting(0.00)]). fof(t37_finseq_2,theorem,( ! [A,B] : ( ~ v1_xboole_0(B) => ! [C] : ( ( v1_relat_1(C) & v1_funct_1(C) & v1_finseq_1(C) ) => ! [D] : ( m2_finseq_1(D,A) => ! [E] : ( ( v1_funct_1(E) & v1_funct_2(E,A,B) & m2_relset_1(E,A,B) ) => ( C = k1_partfun1(k5_numbers,A,A,B,D,E) => k3_finseq_1(C) = k3_finseq_1(D) ) ) ) ) ) ), file(finseq_2,t37_finseq_2), [interesting(0.00)]). fof(t31_finseq_3,theorem,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) & v1_finseq_1(A) ) => ! [B] : ( ( v1_relat_1(B) & v1_funct_1(B) & v1_finseq_1(B) ) => ( k3_finseq_1(A) = k3_finseq_1(B) <=> k4_finseq_1(A) = k4_finseq_1(B) ) ) ) ), file(finseq_3,t31_finseq_3), [interesting(0.00)]). fof(t66_rvsum_1,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( m1_subset_1(B,k1_numbers) => ! [C] : ( m2_finseq_1(C,k1_numbers) => k2_seq_1(k5_numbers,k1_numbers,k9_rvsum_1(B,C),A) = k11_binop_2(B,k2_seq_1(k5_numbers,k1_numbers,C,A)) ) ) ) ), file(rvsum_1,t66_rvsum_1), [interesting(0.00)]). fof(t38_rfinseq,theorem,( ! [A] : ( m2_finseq_1(A,k1_numbers) => k3_funct_2(k5_numbers,k1_numbers,k9_rvsum_1(0,A),k1_tarski(0)) = k4_finseq_1(A) ) ), file(rfinseq,t38_rfinseq), [interesting(0.00)]). fof(t9_rfunct_3,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( ( v1_funct_1(B) & m2_relset_1(B,A,k1_numbers) ) => k11_relset_1(A,k1_numbers,k13_seq_1(A,k1_numbers,B,0),k2_setwiseo(k1_numbers,0)) = k4_relset_1(A,k1_numbers,B) ) ) ), inference(mizar_proof,[status(thm)],[d3_tarski,d13_funct_1,d6_seq_1,d10_xboole_0,d3_tarski,d6_seq_1,d6_seq_1,d1_tarski,d13_funct_1]), [file(rfunct_3,t9_rfunct_3),interesting(0.00)]). fof(t37_rfinseq,theorem,( ! [A] : ( m2_finseq_1(A,k1_numbers) => ! [B] : ( m1_subset_1(B,k1_numbers) => ! [C] : ( m1_subset_1(C,k1_numbers) => ( B != 0 => k3_funct_2(k5_numbers,k1_numbers,A,k1_tarski(k6_real_1(C,B))) = k3_funct_2(k5_numbers,k1_numbers,k9_rvsum_1(B,A),k1_tarski(C)) ) ) ) ) ), file(rfinseq,t37_rfinseq), [interesting(0.00)]). fof(t117_rvsum_1,theorem,( ! [A] : ( m1_subset_1(A,k1_numbers) => ! [B] : ( m2_finseq_1(B,k1_numbers) => k15_rvsum_1(k9_rvsum_1(A,B)) = k11_binop_2(A,k15_rvsum_1(B)) ) ) ), file(rvsum_1,t117_rvsum_1), [interesting(0.00)]). fof(t49_rvsum_1,theorem,( ! [A] : ( m2_finseq_1(A,k1_numbers) => ( k7_rvsum_1(k6_finseq_1(k1_numbers),A) = k6_finseq_1(k1_numbers) & k7_rvsum_1(A,k6_finseq_1(k1_numbers)) = k6_finseq_1(k1_numbers) ) ) ), file(rvsum_1,t49_rvsum_1), [interesting(0.00)]). fof(t12_funct_1,theorem,( ! [A,B] : ( ( v1_relat_1(B) & v1_funct_1(B) ) => ( r2_hidden(A,k1_relat_1(B)) => r2_hidden(k1_funct_1(B,A),k2_relat_1(B)) ) ) ), file(funct_1,t12_funct_1), [interesting(0.00)]). fof(t25_finseq_1,theorem,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) & v1_finseq_1(A) ) => ( k3_finseq_1(A) = 0 <=> A = k1_xboole_0 ) ) ), file(finseq_1,t25_finseq_1), [interesting(0.00)]). fof(t1_xreal_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ( ( r1_xreal_0(A,B) & r1_xreal_0(B,A) ) => A = B ) ) ) ), file(xreal_1,t1_xreal_1), [interesting(0.00)]). fof(t46_finseq_1,theorem,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) & v1_finseq_1(A) ) => ! [B] : ( ( v1_relat_1(B) & v1_funct_1(B) & v1_finseq_1(B) ) => ! [C] : ( ( v1_relat_1(C) & v1_funct_1(C) & v1_finseq_1(C) ) => ( ( k7_finseq_1(A,B) = k7_finseq_1(C,B) | k7_finseq_1(B,A) = k7_finseq_1(B,C) ) => A = C ) ) ) ) ), file(finseq_1,t46_finseq_1), [interesting(0.00)]). fof(t50_rvsum_1,theorem,( ! [A] : ( m1_subset_1(A,k1_numbers) => ! [B] : ( m1_subset_1(B,k1_numbers) => k7_rvsum_1(k12_finseq_1(k1_numbers,A),k12_finseq_1(k1_numbers,B)) = k12_finseq_1(k1_numbers,k10_binop_2(A,B)) ) ) ), file(rvsum_1,t50_rvsum_1), [interesting(0.00)]). fof(t69_finseq_2,theorem,( ! [A] : ( v4_ordinal2(A) => ! [B] : k3_finseq_1(k2_finseq_2(A,B)) = A ) ), file(finseq_2,t69_finseq_2), [interesting(0.00)]). fof(d6_rvsum_1,definition,( ! [A] : ( m2_finseq_1(A,k1_numbers) => ! [B] : ( m2_finseq_1(B,k1_numbers) => k7_rvsum_1(A,B) = k1_finseqop(k1_numbers,k1_numbers,k1_numbers,k34_binop_2,A,B) ) ) ), file(rvsum_1,d6_rvsum_1), [interesting(0.00)]). fof(t86_finseq_2,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( ~ v1_xboole_0(B) => ! [C] : ( ~ v1_xboole_0(C) => ! [D] : ( ( v1_relat_1(D) & v1_funct_1(D) & v1_finseq_1(D) ) => ! [E] : ( ( v1_funct_1(E) & v1_funct_2(E,k2_zfmisc_1(A,B),C) & m2_relset_1(E,k2_zfmisc_1(A,B),C) ) => ! [F] : ( m2_finseq_1(F,A) => ! [G] : ( m2_finseq_1(G,B) => ( ( k3_finseq_1(F) = k3_finseq_1(G) & D = k3_funcop_1(E,F,G) ) => ( k3_finseq_1(D) = k3_finseq_1(F) & k3_finseq_1(D) = k3_finseq_1(G) ) ) ) ) ) ) ) ) ) ), file(finseq_2,t86_finseq_2), [interesting(0.00)]). fof(t6_finseq_1,theorem,( ! [A] : ( v4_ordinal2(A) => r2_hidden(k2_xcmplx_0(A,1),k2_finseq_1(k2_xcmplx_0(A,1))) ) ), file(finseq_1,t6_finseq_1), [interesting(0.00)]). fof(t70_finseq_2,theorem,( ! [A] : ( v4_ordinal2(A) => ! [B,C] : ( r2_hidden(B,k2_finseq_1(A)) => k1_funct_1(k2_finseq_2(A,C),B) = C ) ) ), file(finseq_2,t70_finseq_2), [interesting(0.00)]). fof(t47_rvsum_1,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( m2_finseq_1(B,k1_numbers) => ! [C] : ( m2_finseq_1(C,k1_numbers) => ( r2_hidden(A,k4_finseq_1(k7_rvsum_1(B,C))) => k2_seq_1(k5_numbers,k1_numbers,k7_rvsum_1(B,C),A) = k10_binop_2(k2_seq_1(k5_numbers,k1_numbers,B,A),k2_seq_1(k5_numbers,k1_numbers,C,A)) ) ) ) ) ), file(rvsum_1,t47_rvsum_1), [interesting(0.00)]). fof(d7_finseq_1,definition,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) & v1_finseq_1(A) ) => ! [B] : ( ( v1_relat_1(B) & v1_funct_1(B) & v1_finseq_1(B) ) => ! [C] : ( ( v1_relat_1(C) & v1_funct_1(C) & v1_finseq_1(C) ) => ( C = k7_finseq_1(A,B) <=> ( k4_finseq_1(C) = k2_finseq_1(k1_nat_1(k3_finseq_1(A),k3_finseq_1(B))) & ! [D] : ( m2_subset_1(D,k1_numbers,k5_numbers) => ( r2_hidden(D,k4_finseq_1(A)) => k1_funct_1(C,D) = k1_funct_1(A,D) ) ) & ! [D] : ( m2_subset_1(D,k1_numbers,k5_numbers) => ( r2_hidden(D,k4_finseq_1(B)) => k1_funct_1(C,k1_nat_1(k3_finseq_1(A),D)) = k1_funct_1(B,D) ) ) ) ) ) ) ) ), file(finseq_1,d7_finseq_1), [interesting(0.00)]). fof(t110_finseq_2,theorem,( ! [A,B] : ( m2_finseq_1(B,A) => m1_subset_1(B,k4_finseq_2(k3_finseq_1(B),A)) ) ), file(finseq_2,t110_finseq_2), [interesting(0.00)]). fof(t120_rvsum_1,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( m2_finseq_2(B,k1_numbers,k4_finseq_2(A,k1_numbers)) => ! [C] : ( m2_finseq_2(C,k1_numbers,k4_finseq_2(A,k1_numbers)) => k15_rvsum_1(k8_rvsum_1(A,B,C)) = k10_binop_2(k15_rvsum_1(B),k15_rvsum_1(C)) ) ) ) ), file(rvsum_1,t120_rvsum_1), [interesting(0.00)]). fof(t110_rvsum_1,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( m1_subset_1(B,k1_numbers) => k15_rvsum_1(k4_finseqop(k1_numbers,A,B)) = k11_binop_2(A,B) ) ) ), file(rvsum_1,t110_rvsum_1), [interesting(0.00)]). fof(t56_finseq_1,theorem,( ! [A,B] : ( ( v1_relat_1(B) & v1_funct_1(B) & v1_finseq_1(B) ) => ( B = k9_finseq_1(A) <=> ( k3_finseq_1(B) = 1 & k2_relat_1(B) = k1_tarski(A) ) ) ) ), file(finseq_1,t56_finseq_1), [interesting(0.00)]). fof(t72_rfunct_3,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( ( v1_funct_1(B) & m2_relset_1(B,A,k1_numbers) ) => ! [C] : ( m1_subset_1(C,A) => ( r2_hidden(C,k4_relset_1(A,k1_numbers,B)) => k22_rfunct_3(A,B,k2_setwiseo(A,C)) = k12_finseq_1(k1_numbers,k2_seq_1(A,k1_numbers,B,C)) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t37_zfmisc_1,t28_xboole_1,t68_funct_1,t70_rfunct_3,t79_card_1,d14_rfunct_3,t1_rfinseq,d3_tarski,t26_partfun1,d1_tarski,t68_funct_1,d1_tarski,d10_xboole_0,d3_tarski,d1_tarski,t68_funct_1,d5_funct_1,t56_finseq_1]), [file(rfunct_3,t72_rfunct_3),interesting(0.00)]). fof(t7_xboole_1,theorem,( ! [A,B] : r1_tarski(A,k2_xboole_0(A,B)) ), file(xboole_1,t7_xboole_1), [interesting(0.00)]). fof(t13_xboole_1,theorem,( ! [A,B,C,D] : ( ( r1_tarski(A,B) & r1_tarski(C,D) ) => r1_tarski(k2_xboole_0(A,C),k2_xboole_0(B,D)) ) ), file(xboole_1,t13_xboole_1), [interesting(0.00)]). fof(t27_xboole_1,theorem,( ! [A,B,C,D] : ( ( r1_tarski(A,B) & r1_tarski(C,D) ) => r1_tarski(k3_xboole_0(A,C),k3_xboole_0(B,D)) ) ), file(xboole_1,t27_xboole_1), [interesting(0.00)]). fof(t3_xboole_1,theorem,( ! [A] : ( r1_tarski(A,k1_xboole_0) => A = k1_xboole_0 ) ), file(xboole_1,t3_xboole_1), [interesting(0.00)]). fof(t65_zfmisc_1,theorem,( ! [A,B] : ( k4_xboole_0(A,k1_tarski(B)) = A <=> ~ r2_hidden(B,A) ) ), file(zfmisc_1,t65_zfmisc_1), [interesting(0.00)]). fof(t42_xboole_1,theorem,( ! [A,B,C] : k4_xboole_0(k2_xboole_0(A,B),C) = k2_xboole_0(k4_xboole_0(A,C),k4_xboole_0(B,C)) ), file(xboole_1,t42_xboole_1), [interesting(0.00)]). fof(t105_rvsum_1,theorem,( ! [A] : ( m2_finseq_1(A,k1_numbers) => ! [B] : ( m2_finseq_1(B,k1_numbers) => k15_rvsum_1(k8_finseq_1(k1_numbers,A,B)) = k9_binop_2(k15_rvsum_1(A),k15_rvsum_1(B)) ) ) ), file(rvsum_1,t105_rvsum_1), [interesting(0.00)]).