fof(t23_analoaf,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_rlvect_1(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & v7_rlvect_1(A) & l2_rlvect_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ~ ( r1_analoaf(A,B,C,B,D) & ~ r1_analoaf(A,B,C,C,D) & ~ r1_analoaf(A,B,D,D,C) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t16_analoaf,t4_analoaf,t6_analoaf,t48_rlvect_1,t49_rlvect_1,t11_analoaf,t4_analoaf,t6_analoaf,t48_rlvect_1,t49_rlvect_1,t11_analoaf,t50_rlvect_1,t21_rlvect_1,d1_analoaf,l3_analoaf,d1_analoaf,t21_analoaf,d1_analoaf]), [file(analoaf,t23_analoaf),interesting(1.00)]). fof(t19_analoaf,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_rlvect_1(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & v7_rlvect_1(A) & l2_rlvect_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ( r1_analoaf(A,B,C,C,B) => B = C ) ) ) ) ), inference(mizar_proof,[status(thm)],[t16_analoaf,t10_analoaf,t16_rlvect_1,d9_rlvect_1,t24_rlvect_1,l2_analoaf,d10_rlvect_1,t30_rlvect_1]), [file(analoaf,t19_analoaf),interesting(0.94)]). fof(l2_analoaf,theorem,( ! [A] : ( m1_subset_1(A,k1_numbers) => ! [B] : ( m1_subset_1(B,k1_numbers) => ~ ( ~ r1_xreal_0(A,0) & ~ r1_xreal_0(B,0) & r1_xreal_0(k3_real_1(A,B),0) ) ) ) ), inference(mizar_proof,[status(thm)],[t36_xreal_1]), [file(analoaf,l2_analoaf),interesting(0.84)]). fof(t22_analoaf,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_rlvect_1(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & v7_rlvect_1(A) & l2_rlvect_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ( r1_analoaf(A,B,C,C,D) => r1_analoaf(A,B,C,B,D) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t16_analoaf,t4_analoaf,d9_rlvect_1,d9_rlvect_1,l2_analoaf,d1_analoaf,d1_analoaf,t17_analoaf]), [file(analoaf,t22_analoaf),interesting(0.79)]). fof(l3_analoaf,theorem,( ! [A] : ( m1_subset_1(A,k1_numbers) => ! [B] : ( m1_subset_1(B,k1_numbers) => ~ ( A != B & r1_xreal_0(k5_real_1(A,B),0) & r1_xreal_0(k5_real_1(B,A),0) ) ) ) ), inference(mizar_proof,[status(thm)],[t57_xreal_1]), [file(analoaf,l3_analoaf),interesting(0.79)]). fof(t38_analoaf,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_rlvect_1(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & v7_rlvect_1(A) & l2_rlvect_1(A) ) => ( ? [B] : ( m1_subset_1(B,u1_struct_0(A)) & ? [C] : ( m1_subset_1(C,u1_struct_0(A)) & ! [D] : ( m1_subset_1(D,k1_numbers) => ! [E] : ( m1_subset_1(E,k1_numbers) => ( k4_rlvect_1(A,k3_rlvect_1(A,B,D),k3_rlvect_1(A,C,E)) = k1_rlvect_1(A) => ( D = 0 & E = 0 ) ) ) ) ) ) => ( ~ v3_struct_0(k2_analoaf(A)) & ~ v3_realset2(k2_analoaf(A)) & v2_analoaf(k2_analoaf(A)) & l1_analoaf(k2_analoaf(A)) ) ) ) ), inference(mizar_proof,[status(thm)],[t35_analoaf,d5_analoaf,d7_realset2]), [file(analoaf,t38_analoaf),interesting(0.78)]). fof(t27_analoaf,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_rlvect_1(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & v7_rlvect_1(A) & l2_rlvect_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ! [E] : ( m1_subset_1(E,u1_struct_0(A)) => ~ ( B != C & r1_analoaf(A,C,B,B,D) & ! [F] : ( m1_subset_1(F,u1_struct_0(A)) => ~ ( r1_analoaf(A,E,B,B,F) & r1_analoaf(A,E,C,D,F) ) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d1_analoaf,t16_analoaf,d9_rlvect_1,t78_rlsub_2,t124_xreal_1,t131_xreal_1,d1_analoaf,t78_rlsub_2,d9_rlvect_1,t4_analoaf,t6_analoaf,t4_analoaf,t6_analoaf,t48_rlvect_1,t13_analoaf,t48_rlvect_1,d1_analoaf]), [file(analoaf,t27_analoaf),interesting(0.77)]). fof(t26_analoaf,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_rlvect_1(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & v7_rlvect_1(A) & l2_rlvect_1(A) ) => ( ~ ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => B = C ) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ? [E] : ( m1_subset_1(E,u1_struct_0(A)) & r1_analoaf(A,B,C,D,E) & r1_analoaf(A,B,D,C,E) & C != E ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d1_analoaf,d1_analoaf,t25_analoaf,d6_rlvect_1,t22_rlvect_1,t35_rlvect_1]), [file(analoaf,t26_analoaf),interesting(0.66)]). fof(t17_analoaf,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_rlvect_1(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & v7_rlvect_1(A) & l2_rlvect_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => r1_analoaf(A,B,C,B,C) ) ) ) ), inference(mizar_proof,[status(thm)],[d1_analoaf]), [file(analoaf,t17_analoaf),interesting(0.65)]). fof(t9_analoaf,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_rlvect_1(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & v7_rlvect_1(A) & l2_rlvect_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ! [E] : ( m1_subset_1(E,u1_struct_0(A)) => ( k4_rlvect_1(A,B,C) = k4_rlvect_1(A,D,E) => k6_rlvect_1(A,B,E) = k6_rlvect_1(A,D,C) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t10_rlvect_1,t28_rlvect_1,d6_rlvect_1,d6_rlvect_1,t78_rlsub_2]), [file(analoaf,t9_analoaf),interesting(0.57)]). fof(t25_analoaf,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_rlvect_1(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & v7_rlvect_1(A) & l2_rlvect_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ! [E] : ( m1_subset_1(E,u1_struct_0(A)) => ( B = k6_rlvect_1(A,k4_rlvect_1(A,C,D),E) => ( r1_analoaf(A,E,C,D,B) & r1_analoaf(A,E,D,C,B) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t78_rlsub_2,t9_analoaf,t24_analoaf]), [file(analoaf,t25_analoaf),interesting(0.51)]). fof(t31_analoaf,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_rlvect_1(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & v7_rlvect_1(A) & l2_rlvect_1(A) ) => ( ? [B] : ( m1_subset_1(B,u1_struct_0(A)) & ? [C] : ( m1_subset_1(C,u1_struct_0(A)) & ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ? [E] : ( m1_subset_1(E,k1_numbers) & ? [F] : ( m1_subset_1(F,k1_numbers) & k4_rlvect_1(A,k3_rlvect_1(A,B,E),k3_rlvect_1(A,C,F)) = D ) ) ) ) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ! [E] : ( m1_subset_1(E,u1_struct_0(A)) => ~ ( ~ r1_analoaf(A,B,C,D,E) & ~ r1_analoaf(A,B,C,E,D) & ! [F] : ( m1_subset_1(F,u1_struct_0(A)) => ~ ( ( r1_analoaf(A,B,C,B,F) | r1_analoaf(A,B,C,F,B) ) & ( r1_analoaf(A,D,E,D,F) | r1_analoaf(A,D,E,F,D) ) ) ) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t23_rlvect_1,t23_rlvect_1,t10_rlvect_1,t35_rlvect_1,d1_analoaf,t6_xcmplx_1,t23_rlvect_1,t23_rlvect_1,t10_rlvect_1,t35_rlvect_1,d1_analoaf,t23_rlvect_1,t10_rlvect_1,t23_rlvect_1,t10_rlvect_1,d9_rlvect_1,d7_xcmplx_0,d9_rlvect_1,d9_rlvect_1,d7_xcmplx_0,d9_rlvect_1,t203_xcmplx_1,l33_analoaf,t23_rlvect_1,t23_rlvect_1,t10_rlvect_1,t35_rlvect_1,d1_analoaf,t6_xcmplx_1,t6_xcmplx_1,t23_rlvect_1,t10_rlvect_1,t23_rlvect_1,t10_rlvect_1,d9_rlvect_1,d7_xcmplx_0,d9_rlvect_1,d9_rlvect_1,d7_xcmplx_0,d9_rlvect_1,t203_xcmplx_1,l33_analoaf,d9_rlvect_1,d9_rlvect_1,d9_rlvect_1,d9_rlvect_1,d9_rlvect_1,d9_rlvect_1,l33_analoaf,t6_xcmplx_1,t6_xcmplx_1,t23_rlvect_1,t23_rlvect_1,t10_rlvect_1,t35_rlvect_1,d1_analoaf,t48_rlvect_1,d9_rlvect_1,d9_rlvect_1,d7_xcmplx_0,d6_rlvect_1,t28_rlvect_1,t10_rlvect_1,t48_rlvect_1,d9_rlvect_1,d9_rlvect_1,d7_xcmplx_0,d6_rlvect_1,t48_rlvect_1,d9_rlvect_1,d9_rlvect_1,d9_rlvect_1,d9_rlvect_1,d9_rlvect_1,d9_rlvect_1,d6_rlvect_1,d6_rlvect_1,d6_rlvect_1,d9_rlvect_1,d9_rlvect_1,d9_rlvect_1,d9_rlvect_1,d9_rlvect_1,t23_rlvect_1,t24_rlvect_1,t35_rlvect_1,d1_analoaf,l33_analoaf,t23_rlvect_1,t24_rlvect_1,t35_rlvect_1,d1_analoaf,l33_analoaf,l33_analoaf]), [file(analoaf,t31_analoaf),interesting(0.46)]). fof(t12_analoaf,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_rlvect_1(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & v7_rlvect_1(A) & l2_rlvect_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,k1_numbers) => ( k3_rlvect_1(A,B,D) = C => ( D = 0 | B = k3_rlvect_1(A,C,k2_real_1(D)) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d9_rlvect_1,d7_xcmplx_0,d9_rlvect_1]), [file(analoaf,t12_analoaf),interesting(0.42)]). fof(l33_analoaf,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_rlvect_1(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & v7_rlvect_1(A) & l2_rlvect_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ! [E] : ( m1_subset_1(E,u1_struct_0(A)) => ! [F] : ( m1_subset_1(F,k1_numbers) => ! [G] : ( m1_subset_1(G,k1_numbers) => ~ ( k3_rlvect_1(A,k6_rlvect_1(A,B,C),F) = k3_rlvect_1(A,k6_rlvect_1(A,D,E),G) & ~ ( F = 0 & G = 0 ) & ~ r1_analoaf(A,C,B,D,E) & ~ r1_analoaf(A,C,B,E,D) ) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t23_rlvect_1,t24_rlvect_1,t35_rlvect_1,d1_analoaf,t23_rlvect_1,t24_rlvect_1,t35_rlvect_1,d1_analoaf,t60_xreal_1,t38_rlvect_1,t39_rlvect_1,t39_rlvect_1,t38_rlvect_1,d1_analoaf,t60_xreal_1,t38_rlvect_1,t39_rlvect_1,t39_rlvect_1,t81_vectsp_1,d1_analoaf,t60_xreal_1,t30_rlvect_1,t39_rlvect_1,t81_vectsp_1,t39_rlvect_1,t38_rlvect_1,d1_analoaf,d1_analoaf]), [file(analoaf,l33_analoaf),interesting(0.36)]). fof(t11_analoaf,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_rlvect_1(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & v7_rlvect_1(A) & l2_rlvect_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,k1_numbers) => ! [E] : ( m1_subset_1(E,k1_numbers) => k3_rlvect_1(A,k6_rlvect_1(A,B,C),k5_real_1(D,E)) = k3_rlvect_1(A,k6_rlvect_1(A,C,B),k5_real_1(E,D)) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t81_vectsp_1,t40_rlvect_1]), [file(analoaf,t11_analoaf),interesting(0.32)]). fof(t36_analoaf,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_rlvect_1(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & v7_rlvect_1(A) & l2_rlvect_1(A) ) => ( ? [B] : ( m1_subset_1(B,u1_struct_0(A)) & ? [C] : ( m1_subset_1(C,u1_struct_0(A)) & ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ? [E] : ( m1_subset_1(E,k1_numbers) & ? [F] : ( m1_subset_1(F,k1_numbers) & k4_rlvect_1(A,k3_rlvect_1(A,B,E),k3_rlvect_1(A,C,F)) = D ) ) ) ) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(k2_analoaf(A))) => ! [C] : ( m1_subset_1(C,u1_struct_0(k2_analoaf(A))) => ! [D] : ( m1_subset_1(D,u1_struct_0(k2_analoaf(A))) => ! [E] : ( m1_subset_1(E,u1_struct_0(k2_analoaf(A))) => ~ ( ~ r2_analoaf(k2_analoaf(A),B,C,D,E) & ~ r2_analoaf(k2_analoaf(A),B,C,E,D) & ! [F] : ( m1_subset_1(F,u1_struct_0(k2_analoaf(A))) => ~ ( ( r2_analoaf(k2_analoaf(A),B,C,B,F) | r2_analoaf(k2_analoaf(A),B,C,F,B) ) & ( r2_analoaf(k2_analoaf(A),D,E,D,F) | r2_analoaf(k2_analoaf(A),D,E,F,D) ) ) ) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d2_analoaf,t33_analoaf,t31_analoaf,t33_analoaf,d2_analoaf]), [file(analoaf,t36_analoaf),interesting(0.29)]). fof(t10_analoaf,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_rlvect_1(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & v7_rlvect_1(A) & l2_rlvect_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,k1_numbers) => k3_rlvect_1(A,k6_rlvect_1(A,B,C),D) = k5_rlvect_1(A,k3_rlvect_1(A,k6_rlvect_1(A,C,B),D)) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t81_vectsp_1,t39_rlvect_1,t28_rlvect_1,d10_rlvect_1]), [file(analoaf,t10_analoaf),interesting(0.29)]). fof(t29_analoaf,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_rlvect_1(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & v7_rlvect_1(A) & l2_rlvect_1(A) ) => ~ ( ? [B] : ( m1_subset_1(B,u1_struct_0(A)) & ? [C] : ( m1_subset_1(C,u1_struct_0(A)) & ! [D] : ( m1_subset_1(D,k1_numbers) => ! [E] : ( m1_subset_1(E,k1_numbers) => ( k4_rlvect_1(A,k3_rlvect_1(A,B,D),k3_rlvect_1(A,C,E)) = k1_rlvect_1(A) => ( D = 0 & E = 0 ) ) ) ) ) ) & ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ! [E] : ( m1_subset_1(E,u1_struct_0(A)) => ~ ( ~ r1_analoaf(A,B,C,D,E) & ~ r1_analoaf(A,B,C,E,D) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t28_analoaf,t26_rlvect_1,t27_rlvect_1,t39_rlvect_1,t16_rlvect_1,d1_analoaf,t26_rlvect_1,t28_rlvect_1,t39_rlvect_1,t38_rlvect_1,d1_analoaf]), [file(analoaf,t29_analoaf),interesting(0.29)]). fof(t51_analoaf,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_rlvect_1(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & v7_rlvect_1(A) & l2_rlvect_1(A) ) => ( ? [B] : ( m1_subset_1(B,u1_struct_0(A)) & ? [C] : ( m1_subset_1(C,u1_struct_0(A)) & ! [D] : ( m1_subset_1(D,k1_numbers) => ! [E] : ( m1_subset_1(E,k1_numbers) => ( k4_rlvect_1(A,k3_rlvect_1(A,B,D),k3_rlvect_1(A,C,E)) = k1_rlvect_1(A) => ( D = 0 & E = 0 ) ) ) ) & ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ? [E] : ( m1_subset_1(E,k1_numbers) & ? [F] : ( m1_subset_1(F,k1_numbers) & D = k4_rlvect_1(A,k3_rlvect_1(A,B,E),k3_rlvect_1(A,C,F)) ) ) ) ) ) => ( ~ v3_struct_0(k2_analoaf(A)) & ~ v3_realset2(k2_analoaf(A)) & v2_analoaf(k2_analoaf(A)) & v3_analoaf(k2_analoaf(A)) & l1_analoaf(k2_analoaf(A)) ) ) ) ), inference(mizar_proof,[status(thm)],[t36_analoaf,d6_analoaf,t38_analoaf]), [file(analoaf,t51_analoaf),interesting(0.29)]). fof(t28_analoaf,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_rlvect_1(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & v7_rlvect_1(A) & l2_rlvect_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ( ! [D] : ( m1_subset_1(D,k1_numbers) => ! [E] : ( m1_subset_1(E,k1_numbers) => ( k4_rlvect_1(A,k3_rlvect_1(A,B,D),k3_rlvect_1(A,C,E)) = k1_rlvect_1(A) => ( D = 0 & E = 0 ) ) ) ) => ( B != C & B != k1_rlvect_1(A) & C != k1_rlvect_1(A) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t28_rlvect_1,d9_rlvect_1,t29_rlvect_1,t23_rlvect_1,t10_rlvect_1,t23_rlvect_1,t23_rlvect_1,t10_rlvect_1,t23_rlvect_1]), [file(analoaf,t28_analoaf),interesting(0.28)]). fof(t13_analoaf,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_rlvect_1(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & v7_rlvect_1(A) & l2_rlvect_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,k1_numbers) => ( ( k3_rlvect_1(A,B,D) = C => ( D = 0 | B = k3_rlvect_1(A,C,k2_real_1(D)) ) ) & ( B = k3_rlvect_1(A,C,k2_real_1(D)) => ( D = 0 | k3_rlvect_1(A,B,D) = C ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t203_xcmplx_1,t12_analoaf,t12_analoaf]), [file(analoaf,t13_analoaf),interesting(0.23)]). fof(t33_analoaf,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_rlvect_1(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & v7_rlvect_1(A) & l2_rlvect_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ! [E] : ( m1_subset_1(E,u1_struct_0(A)) => ( r2_hidden(k1_domain_1(k2_zfmisc_1(u1_struct_0(A),u1_struct_0(A)),k2_zfmisc_1(u1_struct_0(A),u1_struct_0(A)),k1_domain_1(u1_struct_0(A),u1_struct_0(A),B,C),k1_domain_1(u1_struct_0(A),u1_struct_0(A),D,E)),k1_analoaf(A)) <=> r1_analoaf(A,B,C,D,E) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d3_analoaf,t33_zfmisc_1,d3_analoaf]), [file(analoaf,t33_analoaf),interesting(0.22)]). fof(t35_analoaf,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_rlvect_1(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & v7_rlvect_1(A) & l2_rlvect_1(A) ) => ( ? [B] : ( m1_subset_1(B,u1_struct_0(A)) & ? [C] : ( m1_subset_1(C,u1_struct_0(A)) & ! [D] : ( m1_subset_1(D,k1_numbers) => ! [E] : ( m1_subset_1(E,k1_numbers) => ( k4_rlvect_1(A,k3_rlvect_1(A,B,D),k3_rlvect_1(A,C,E)) = k1_rlvect_1(A) => ( D = 0 & E = 0 ) ) ) ) ) ) => ( ~ ! [B] : ( m1_subset_1(B,u1_struct_0(k2_analoaf(A))) => ! [C] : ( m1_subset_1(C,u1_struct_0(k2_analoaf(A))) => B = C ) ) & ! [B] : ( m1_subset_1(B,u1_struct_0(k2_analoaf(A))) => ! [C] : ( m1_subset_1(C,u1_struct_0(k2_analoaf(A))) => ! [D] : ( m1_subset_1(D,u1_struct_0(k2_analoaf(A))) => ! [E] : ( m1_subset_1(E,u1_struct_0(k2_analoaf(A))) => ! [F] : ( m1_subset_1(F,u1_struct_0(k2_analoaf(A))) => ! [G] : ( m1_subset_1(G,u1_struct_0(k2_analoaf(A))) => ! [H] : ( m1_subset_1(H,u1_struct_0(k2_analoaf(A))) => ! [I] : ( m1_subset_1(I,u1_struct_0(k2_analoaf(A))) => ( r2_analoaf(k2_analoaf(A),B,C,D,D) & ( r2_analoaf(k2_analoaf(A),B,C,C,B) => B = C ) & ( ( r2_analoaf(k2_analoaf(A),B,C,F,G) & r2_analoaf(k2_analoaf(A),B,C,H,I) ) => ( B = C | r2_analoaf(k2_analoaf(A),F,G,H,I) ) ) & ( r2_analoaf(k2_analoaf(A),B,C,D,E) => r2_analoaf(k2_analoaf(A),C,B,E,D) ) & ( r2_analoaf(k2_analoaf(A),B,C,C,D) => r2_analoaf(k2_analoaf(A),B,C,B,D) ) & ~ ( r2_analoaf(k2_analoaf(A),B,C,B,D) & ~ r2_analoaf(k2_analoaf(A),B,C,C,D) & ~ r2_analoaf(k2_analoaf(A),B,D,D,C) ) ) ) ) ) ) ) ) ) ) & ? [B] : ( m1_subset_1(B,u1_struct_0(k2_analoaf(A))) & ? [C] : ( m1_subset_1(C,u1_struct_0(k2_analoaf(A))) & ? [D] : ( m1_subset_1(D,u1_struct_0(k2_analoaf(A))) & ? [E] : ( m1_subset_1(E,u1_struct_0(k2_analoaf(A))) & ~ r2_analoaf(k2_analoaf(A),B,C,D,E) & ~ r2_analoaf(k2_analoaf(A),B,C,E,D) ) ) ) ) & ! [B] : ( m1_subset_1(B,u1_struct_0(k2_analoaf(A))) => ! [C] : ( m1_subset_1(C,u1_struct_0(k2_analoaf(A))) => ! [D] : ( m1_subset_1(D,u1_struct_0(k2_analoaf(A))) => ? [E] : ( m1_subset_1(E,u1_struct_0(k2_analoaf(A))) & r2_analoaf(k2_analoaf(A),B,C,D,E) & r2_analoaf(k2_analoaf(A),B,D,C,E) & C != E ) ) ) ) & ! [B] : ( m1_subset_1(B,u1_struct_0(k2_analoaf(A))) => ! [C] : ( m1_subset_1(C,u1_struct_0(k2_analoaf(A))) => ! [D] : ( m1_subset_1(D,u1_struct_0(k2_analoaf(A))) => ! [E] : ( m1_subset_1(E,u1_struct_0(k2_analoaf(A))) => ~ ( B != D & r2_analoaf(k2_analoaf(A),D,B,B,E) & ! [F] : ( m1_subset_1(F,u1_struct_0(k2_analoaf(A))) => ~ ( r2_analoaf(k2_analoaf(A),C,B,B,F) & r2_analoaf(k2_analoaf(A),C,D,E,F) ) ) ) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t28_analoaf,d1_analoaf,t33_analoaf,d2_analoaf,d2_analoaf,t33_analoaf,t19_analoaf,d2_analoaf,t33_analoaf,t20_analoaf,t33_analoaf,d2_analoaf,d2_analoaf,t33_analoaf,t21_analoaf,t33_analoaf,d2_analoaf,d2_analoaf,t33_analoaf,t22_analoaf,t33_analoaf,d2_analoaf,d2_analoaf,t33_analoaf,t23_analoaf,t33_analoaf,d2_analoaf,t29_analoaf,t33_analoaf,d2_analoaf,t26_analoaf,t33_analoaf,d2_analoaf,d2_analoaf,t33_analoaf,t27_analoaf,t33_analoaf,d2_analoaf]), [file(analoaf,t35_analoaf),interesting(0.04)]). fof(t14_analoaf,theorem,( $true ), file(analoaf,t14_analoaf), [interesting(0.00)]). fof(t15_analoaf,theorem,( $true ), file(analoaf,t15_analoaf), [interesting(0.00)]). fof(d1_analoaf,definition,( ! [A] : ( ( ~ v3_struct_0(A) & v3_rlvect_1(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & v7_rlvect_1(A) & l2_rlvect_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ! [E] : ( m1_subset_1(E,u1_struct_0(A)) => ( r1_analoaf(A,B,C,D,E) <=> ~ ( B != C & D != E & ! [F] : ( m1_subset_1(F,k1_numbers) => ! [G] : ( m1_subset_1(G,k1_numbers) => ~ ( ~ r1_xreal_0(F,0) & ~ r1_xreal_0(G,0) & k3_rlvect_1(A,k6_rlvect_1(A,C,B),F) = k3_rlvect_1(A,k6_rlvect_1(A,E,D),G) ) ) ) ) ) ) ) ) ) ) ), file(analoaf,d1_analoaf), [interesting(0.00)]). fof(t18_analoaf,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_rlvect_1(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & v7_rlvect_1(A) & l2_rlvect_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ( r1_analoaf(A,B,C,D,D) & r1_analoaf(A,B,B,C,D) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d1_analoaf]), [file(analoaf,t18_analoaf),interesting(0.00)]). fof(t1_analoaf,theorem,( $true ), file(analoaf,t1_analoaf), [interesting(0.00)]). fof(t2_analoaf,theorem,( $true ), file(analoaf,t2_analoaf), [interesting(0.00)]). fof(t30_analoaf,theorem,( $true ), file(analoaf,t30_analoaf), [interesting(0.00)]). fof(t32_analoaf,theorem,( $true ), file(analoaf,t32_analoaf), [interesting(0.00)]). fof(t34_analoaf,theorem,( $true ), file(analoaf,t34_analoaf), [interesting(0.00)]). fof(d5_analoaf,definition,( ! [A] : ( ( ~ v3_struct_0(A) & l1_analoaf(A) ) => ( v2_analoaf(A) <=> ( ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ! [E] : ( m1_subset_1(E,u1_struct_0(A)) => ! [F] : ( m1_subset_1(F,u1_struct_0(A)) => ! [G] : ( m1_subset_1(G,u1_struct_0(A)) => ! [H] : ( m1_subset_1(H,u1_struct_0(A)) => ! [I] : ( m1_subset_1(I,u1_struct_0(A)) => ( r2_analoaf(A,B,C,D,D) & ( r2_analoaf(A,B,C,C,B) => B = C ) & ( ( r2_analoaf(A,B,C,F,G) & r2_analoaf(A,B,C,H,I) ) => ( B = C | r2_analoaf(A,F,G,H,I) ) ) & ( r2_analoaf(A,B,C,D,E) => r2_analoaf(A,C,B,E,D) ) & ( r2_analoaf(A,B,C,C,D) => r2_analoaf(A,B,C,B,D) ) & ~ ( r2_analoaf(A,B,C,B,D) & ~ r2_analoaf(A,B,C,C,D) & ~ r2_analoaf(A,B,D,D,C) ) ) ) ) ) ) ) ) ) ) & ? [B] : ( m1_subset_1(B,u1_struct_0(A)) & ? [C] : ( m1_subset_1(C,u1_struct_0(A)) & ? [D] : ( m1_subset_1(D,u1_struct_0(A)) & ? [E] : ( m1_subset_1(E,u1_struct_0(A)) & ~ r2_analoaf(A,B,C,D,E) & ~ r2_analoaf(A,B,C,E,D) ) ) ) ) & ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ? [E] : ( m1_subset_1(E,u1_struct_0(A)) & r2_analoaf(A,B,C,D,E) & r2_analoaf(A,B,D,C,E) & C != E ) ) ) ) & ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ! [E] : ( m1_subset_1(E,u1_struct_0(A)) => ~ ( B != D & r2_analoaf(A,D,B,B,E) & ! [F] : ( m1_subset_1(F,u1_struct_0(A)) => ~ ( r2_analoaf(A,C,B,B,F) & r2_analoaf(A,C,D,E,F) ) ) ) ) ) ) ) ) ) ) ), file(analoaf,d5_analoaf), [interesting(0.00)]). fof(d7_realset2,definition,( ! [A] : ( l1_struct_0(A) => ( v3_realset2(A) <=> ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => B = C ) ) ) ) ), file(realset2,d7_realset2), [interesting(0.00)]). fof(t37_analoaf,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & l1_analoaf(A) ) => ( ( ~ ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => B = C ) ) & ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ! [E] : ( m1_subset_1(E,u1_struct_0(A)) => ! [F] : ( m1_subset_1(F,u1_struct_0(A)) => ! [G] : ( m1_subset_1(G,u1_struct_0(A)) => ! [H] : ( m1_subset_1(H,u1_struct_0(A)) => ! [I] : ( m1_subset_1(I,u1_struct_0(A)) => ( r2_analoaf(A,B,C,D,D) & ( r2_analoaf(A,B,C,C,B) => B = C ) & ( ( r2_analoaf(A,B,C,F,G) & r2_analoaf(A,B,C,H,I) ) => ( B = C | r2_analoaf(A,F,G,H,I) ) ) & ( r2_analoaf(A,B,C,D,E) => r2_analoaf(A,C,B,E,D) ) & ( r2_analoaf(A,B,C,C,D) => r2_analoaf(A,B,C,B,D) ) & ~ ( r2_analoaf(A,B,C,B,D) & ~ r2_analoaf(A,B,C,C,D) & ~ r2_analoaf(A,B,D,D,C) ) ) ) ) ) ) ) ) ) ) & ? [B] : ( m1_subset_1(B,u1_struct_0(A)) & ? [C] : ( m1_subset_1(C,u1_struct_0(A)) & ? [D] : ( m1_subset_1(D,u1_struct_0(A)) & ? [E] : ( m1_subset_1(E,u1_struct_0(A)) & ~ r2_analoaf(A,B,C,D,E) & ~ r2_analoaf(A,B,C,E,D) ) ) ) ) & ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ? [E] : ( m1_subset_1(E,u1_struct_0(A)) & r2_analoaf(A,B,C,D,E) & r2_analoaf(A,B,D,C,E) & C != E ) ) ) ) & ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ! [E] : ( m1_subset_1(E,u1_struct_0(A)) => ~ ( B != D & r2_analoaf(A,D,B,B,E) & ! [F] : ( m1_subset_1(F,u1_struct_0(A)) => ~ ( r2_analoaf(A,C,B,B,F) & r2_analoaf(A,C,D,E,F) ) ) ) ) ) ) ) ) <=> ( ~ v3_struct_0(A) & ~ v3_realset2(A) & v2_analoaf(A) & l1_analoaf(A) ) ) ) ), inference(mizar_proof,[status(thm)],[d5_analoaf,d7_realset2]), [file(analoaf,t37_analoaf),interesting(0.00)]). fof(t39_analoaf,theorem,( $true ), file(analoaf,t39_analoaf), [interesting(0.00)]). fof(t3_analoaf,theorem,( $true ), file(analoaf,t3_analoaf), [interesting(0.00)]). fof(t40_analoaf,theorem,( $true ), file(analoaf,t40_analoaf), [interesting(0.00)]). fof(t41_analoaf,theorem,( $true ), file(analoaf,t41_analoaf), [interesting(0.00)]). fof(t42_analoaf,theorem,( $true ), file(analoaf,t42_analoaf), [interesting(0.00)]). fof(t43_analoaf,theorem,( $true ), file(analoaf,t43_analoaf), [interesting(0.00)]). fof(t44_analoaf,theorem,( $true ), file(analoaf,t44_analoaf), [interesting(0.00)]). fof(t45_analoaf,theorem,( $true ), file(analoaf,t45_analoaf), [interesting(0.00)]). fof(t46_analoaf,theorem,( $true ), file(analoaf,t46_analoaf), [interesting(0.00)]). fof(t47_analoaf,theorem,( $true ), file(analoaf,t47_analoaf), [interesting(0.00)]). fof(t48_analoaf,theorem,( $true ), file(analoaf,t48_analoaf), [interesting(0.00)]). fof(t49_analoaf,theorem,( $true ), file(analoaf,t49_analoaf), [interesting(0.00)]). fof(d6_analoaf,definition,( ! [A] : ( ( ~ v3_struct_0(A) & ~ v3_realset2(A) & v2_analoaf(A) & l1_analoaf(A) ) => ( v3_analoaf(A) <=> ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ! [E] : ( m1_subset_1(E,u1_struct_0(A)) => ~ ( ~ r2_analoaf(A,B,C,D,E) & ~ r2_analoaf(A,B,C,E,D) & ! [F] : ( m1_subset_1(F,u1_struct_0(A)) => ~ ( ( r2_analoaf(A,B,C,B,F) | r2_analoaf(A,B,C,F,B) ) & ( r2_analoaf(A,D,E,D,F) | r2_analoaf(A,D,E,F,D) ) ) ) ) ) ) ) ) ) ) ), file(analoaf,d6_analoaf), [interesting(0.00)]). fof(t50_analoaf,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & l1_analoaf(A) ) => ( ( ~ ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => B = C ) ) & ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ! [E] : ( m1_subset_1(E,u1_struct_0(A)) => ! [F] : ( m1_subset_1(F,u1_struct_0(A)) => ! [G] : ( m1_subset_1(G,u1_struct_0(A)) => ! [H] : ( m1_subset_1(H,u1_struct_0(A)) => ! [I] : ( m1_subset_1(I,u1_struct_0(A)) => ( r2_analoaf(A,B,C,D,D) & ( r2_analoaf(A,B,C,C,B) => B = C ) & ( ( r2_analoaf(A,B,C,F,G) & r2_analoaf(A,B,C,H,I) ) => ( B = C | r2_analoaf(A,F,G,H,I) ) ) & ( r2_analoaf(A,B,C,D,E) => r2_analoaf(A,C,B,E,D) ) & ( r2_analoaf(A,B,C,C,D) => r2_analoaf(A,B,C,B,D) ) & ~ ( r2_analoaf(A,B,C,B,D) & ~ r2_analoaf(A,B,C,C,D) & ~ r2_analoaf(A,B,D,D,C) ) ) ) ) ) ) ) ) ) ) & ? [B] : ( m1_subset_1(B,u1_struct_0(A)) & ? [C] : ( m1_subset_1(C,u1_struct_0(A)) & ? [D] : ( m1_subset_1(D,u1_struct_0(A)) & ? [E] : ( m1_subset_1(E,u1_struct_0(A)) & ~ r2_analoaf(A,B,C,D,E) & ~ r2_analoaf(A,B,C,E,D) ) ) ) ) & ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ? [E] : ( m1_subset_1(E,u1_struct_0(A)) & r2_analoaf(A,B,C,D,E) & r2_analoaf(A,B,D,C,E) & C != E ) ) ) ) & ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ! [E] : ( m1_subset_1(E,u1_struct_0(A)) => ~ ( B != D & r2_analoaf(A,D,B,B,E) & ! [F] : ( m1_subset_1(F,u1_struct_0(A)) => ~ ( r2_analoaf(A,C,B,B,F) & r2_analoaf(A,C,D,E,F) ) ) ) ) ) ) ) & ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ! [E] : ( m1_subset_1(E,u1_struct_0(A)) => ~ ( ~ r2_analoaf(A,B,C,D,E) & ~ r2_analoaf(A,B,C,E,D) & ! [F] : ( m1_subset_1(F,u1_struct_0(A)) => ~ ( ( r2_analoaf(A,B,C,B,F) | r2_analoaf(A,B,C,F,B) ) & ( r2_analoaf(A,D,E,D,F) | r2_analoaf(A,D,E,F,D) ) ) ) ) ) ) ) ) ) <=> ( ~ v3_struct_0(A) & ~ v3_realset2(A) & v2_analoaf(A) & v3_analoaf(A) & l1_analoaf(A) ) ) ) ), inference(mizar_proof,[status(thm)],[d5_analoaf,d6_analoaf,d7_realset2]), [file(analoaf,t50_analoaf),interesting(0.00)]). fof(d2_analoaf,definition,( ! [A] : ( ( ~ v3_struct_0(A) & l1_analoaf(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ! [E] : ( m1_subset_1(E,u1_struct_0(A)) => ( r2_analoaf(A,B,C,D,E) <=> r2_hidden(k1_domain_1(k2_zfmisc_1(u1_struct_0(A),u1_struct_0(A)),k2_zfmisc_1(u1_struct_0(A),u1_struct_0(A)),k1_domain_1(u1_struct_0(A),u1_struct_0(A),B,C),k1_domain_1(u1_struct_0(A),u1_struct_0(A),D,E)),u1_analoaf(A)) ) ) ) ) ) ) ), file(analoaf,d2_analoaf), [interesting(0.00)]). fof(d3_analoaf,definition,( ! [A] : ( ( ~ v3_struct_0(A) & v3_rlvect_1(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & v7_rlvect_1(A) & l2_rlvect_1(A) ) => ! [B] : ( m2_relset_1(B,k2_zfmisc_1(u1_struct_0(A),u1_struct_0(A)),k2_zfmisc_1(u1_struct_0(A),u1_struct_0(A))) => ( B = k1_analoaf(A) <=> ! [C,D] : ( r2_hidden(k4_tarski(C,D),B) <=> ? [E] : ( m1_subset_1(E,u1_struct_0(A)) & ? [F] : ( m1_subset_1(F,u1_struct_0(A)) & ? [G] : ( m1_subset_1(G,u1_struct_0(A)) & ? [H] : ( m1_subset_1(H,u1_struct_0(A)) & C = k1_domain_1(u1_struct_0(A),u1_struct_0(A),E,F) & D = k1_domain_1(u1_struct_0(A),u1_struct_0(A),G,H) & r1_analoaf(A,E,F,G,H) ) ) ) ) ) ) ) ) ), file(analoaf,d3_analoaf), [interesting(0.00)]). fof(t33_zfmisc_1,theorem,( ! [A,B,C,D] : ( k4_tarski(A,B) = k4_tarski(C,D) => ( A = C & B = D ) ) ), file(zfmisc_1,t33_zfmisc_1), [interesting(0.00)]). fof(t23_rlvect_1,theorem,( ! [A] : ( m1_subset_1(A,k1_numbers) => ! [B] : ( ( ~ v3_struct_0(B) & v3_rlvect_1(B) & v4_rlvect_1(B) & v5_rlvect_1(B) & v6_rlvect_1(B) & v7_rlvect_1(B) & l2_rlvect_1(B) ) => ! [C] : ( m1_subset_1(C,u1_struct_0(B)) => ( ( A = 0 | C = k1_rlvect_1(B) ) => k3_rlvect_1(B,C,A) = k1_rlvect_1(B) ) ) ) ) ), file(rlvect_1,t23_rlvect_1), [interesting(0.00)]). fof(t10_rlvect_1,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & l1_rlvect_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ( k2_rlvect_1(A,B,k1_rlvect_1(A)) = B & k2_rlvect_1(A,k1_rlvect_1(A),B) = B ) ) ) ), file(rlvect_1,t10_rlvect_1), [interesting(0.00)]). fof(t35_rlvect_1,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & l1_rlvect_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ( k6_rlvect_1(A,B,C) = k1_rlvect_1(A) => B = C ) ) ) ) ), file(rlvect_1,t35_rlvect_1), [interesting(0.00)]). fof(t6_xcmplx_1,theorem,( ! [A] : ( v1_xcmplx_0(A) => ! [B] : ( v1_xcmplx_0(B) => ~ ( k3_xcmplx_0(A,B) = 0 & A != 0 & B != 0 ) ) ) ), file(xcmplx_1,t6_xcmplx_1), [interesting(0.00)]). fof(d9_rlvect_1,definition,( ! [A] : ( ( ~ v3_struct_0(A) & l2_rlvect_1(A) ) => ( v7_rlvect_1(A) <=> ( ! [B] : ( m1_subset_1(B,k1_numbers) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => k3_rlvect_1(A,k2_rlvect_1(A,C,D),B) = k2_rlvect_1(A,k3_rlvect_1(A,C,B),k3_rlvect_1(A,D,B)) ) ) ) & ! [B] : ( m1_subset_1(B,k1_numbers) => ! [C] : ( m1_subset_1(C,k1_numbers) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => k3_rlvect_1(A,D,k3_real_1(B,C)) = k2_rlvect_1(A,k3_rlvect_1(A,D,B),k3_rlvect_1(A,D,C)) ) ) ) & ! [B] : ( m1_subset_1(B,k1_numbers) => ! [C] : ( m1_subset_1(C,k1_numbers) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => k3_rlvect_1(A,D,k4_real_1(B,C)) = k3_rlvect_1(A,k3_rlvect_1(A,D,C),B) ) ) ) & ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => k3_rlvect_1(A,B,1) = B ) ) ) ) ), file(rlvect_1,d9_rlvect_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(t203_xcmplx_1,theorem,( k5_xcmplx_0(0) = 0 ), file(xcmplx_1,t203_xcmplx_1), [interesting(0.00)]). fof(t24_rlvect_1,theorem,( ! [A] : ( m1_subset_1(A,k1_numbers) => ! [B] : ( ( ~ v3_struct_0(B) & v3_rlvect_1(B) & v4_rlvect_1(B) & v5_rlvect_1(B) & v6_rlvect_1(B) & v7_rlvect_1(B) & l2_rlvect_1(B) ) => ! [C] : ( m1_subset_1(C,u1_struct_0(B)) => ~ ( k3_rlvect_1(B,C,A) = k1_rlvect_1(B) & A != 0 & C != k1_rlvect_1(B) ) ) ) ) ), file(rlvect_1,t24_rlvect_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(t38_rlvect_1,theorem,( ! [A] : ( m1_subset_1(A,k1_numbers) => ! [B] : ( ( ~ v3_struct_0(B) & v3_rlvect_1(B) & v4_rlvect_1(B) & v5_rlvect_1(B) & v6_rlvect_1(B) & v7_rlvect_1(B) & l2_rlvect_1(B) ) => ! [C] : ( m1_subset_1(C,u1_struct_0(B)) => k3_rlvect_1(B,k5_rlvect_1(B,C),A) = k3_rlvect_1(B,C,k1_real_1(A)) ) ) ) ), file(rlvect_1,t38_rlvect_1), [interesting(0.00)]). fof(t39_rlvect_1,theorem,( ! [A] : ( m1_subset_1(A,k1_numbers) => ! [B] : ( ( ~ v3_struct_0(B) & v3_rlvect_1(B) & v4_rlvect_1(B) & v5_rlvect_1(B) & v6_rlvect_1(B) & v7_rlvect_1(B) & l2_rlvect_1(B) ) => ! [C] : ( m1_subset_1(C,u1_struct_0(B)) => k3_rlvect_1(B,k5_rlvect_1(B,C),A) = k5_rlvect_1(B,k3_rlvect_1(B,C,A)) ) ) ) ), file(rlvect_1,t39_rlvect_1), [interesting(0.00)]). fof(t81_vectsp_1,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & l1_rlvect_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => k5_rlvect_1(A,k6_rlvect_1(A,B,C)) = k6_rlvect_1(A,C,B) ) ) ) ), file(vectsp_1,t81_vectsp_1), [interesting(0.00)]). fof(t30_rlvect_1,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & l1_rlvect_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => k5_rlvect_1(A,k5_rlvect_1(A,B)) = B ) ) ), file(rlvect_1,t30_rlvect_1), [interesting(0.00)]). fof(t48_rlvect_1,theorem,( ! [A] : ( m1_subset_1(A,k1_numbers) => ! [B] : ( ( ~ v3_struct_0(B) & v3_rlvect_1(B) & v4_rlvect_1(B) & v5_rlvect_1(B) & v6_rlvect_1(B) & v7_rlvect_1(B) & l2_rlvect_1(B) ) => ! [C] : ( m1_subset_1(C,u1_struct_0(B)) => ! [D] : ( m1_subset_1(D,u1_struct_0(B)) => k3_rlvect_1(B,k6_rlvect_1(B,C,D),A) = k6_rlvect_1(B,k3_rlvect_1(B,C,A),k3_rlvect_1(B,D,A)) ) ) ) ) ), file(rlvect_1,t48_rlvect_1), [interesting(0.00)]). fof(d6_rlvect_1,definition,( ! [A] : ( ( ~ v3_struct_0(A) & l1_rlvect_1(A) ) => ( v4_rlvect_1(A) <=> ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => k2_rlvect_1(A,k2_rlvect_1(A,B,C),D) = k2_rlvect_1(A,B,k2_rlvect_1(A,C,D)) ) ) ) ) ) ), file(rlvect_1,d6_rlvect_1), [interesting(0.00)]). fof(t28_rlvect_1,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & l1_rlvect_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => k6_rlvect_1(A,B,B) = k1_rlvect_1(A) ) ) ), file(rlvect_1,t28_rlvect_1), [interesting(0.00)]). fof(t29_rlvect_1,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_rlvect_1(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & v7_rlvect_1(A) & l2_rlvect_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => k5_rlvect_1(A,B) = k3_rlvect_1(A,B,k1_real_1(1)) ) ) ), file(rlvect_1,t29_rlvect_1), [interesting(0.00)]). fof(t16_analoaf,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_rlvect_1(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & v7_rlvect_1(A) & l2_rlvect_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ! [E] : ( m1_subset_1(E,u1_struct_0(A)) => ~ ( r1_analoaf(A,B,C,D,E) & B != C & D != E & ! [F] : ( m1_subset_1(F,k1_numbers) => ! [G] : ( m1_subset_1(G,k1_numbers) => ~ ( k3_rlvect_1(A,k6_rlvect_1(A,C,B),F) = k3_rlvect_1(A,k6_rlvect_1(A,E,D),G) & ~ r1_xreal_0(F,0) & ~ r1_xreal_0(G,0) ) ) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d1_analoaf]), [file(analoaf,t16_analoaf),interesting(0.00)]). fof(d10_rlvect_1,definition,( ! [A] : ( ( ~ v3_struct_0(A) & l1_rlvect_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ( ( v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) ) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ( C = k5_rlvect_1(A,B) <=> k2_rlvect_1(A,B,C) = k1_rlvect_1(A) ) ) ) ) ) ), file(rlvect_1,d10_rlvect_1), [interesting(0.00)]). fof(t16_rlvect_1,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & l1_rlvect_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ( k2_rlvect_1(A,B,k5_rlvect_1(A,B)) = k1_rlvect_1(A) & k2_rlvect_1(A,k5_rlvect_1(A,B),B) = k1_rlvect_1(A) ) ) ) ), file(rlvect_1,t16_rlvect_1), [interesting(0.00)]). fof(t36_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(k2_xcmplx_0(A,B),0) ) ) ) ), file(xreal_1,t36_xreal_1), [interesting(0.00)]). fof(t124_xreal_1,theorem,( ! [A] : ( v1_xreal_0(A) => ( ~ ( ~ r1_xreal_0(A,0) & r1_xreal_0(k5_xcmplx_0(A),0) ) & ~ ( ~ r1_xreal_0(k5_xcmplx_0(A),0) & r1_xreal_0(A,0) ) ) ) ), file(xreal_1,t124_xreal_1), [interesting(0.00)]). fof(t131_xreal_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ~ ( ~ r1_xreal_0(A,0) & ~ r1_xreal_0(B,0) & r1_xreal_0(k3_xcmplx_0(A,B),0) ) ) ) ), file(xreal_1,t131_xreal_1), [interesting(0.00)]). fof(t20_analoaf,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_rlvect_1(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & v7_rlvect_1(A) & l2_rlvect_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ! [E] : ( m1_subset_1(E,u1_struct_0(A)) => ! [F] : ( m1_subset_1(F,u1_struct_0(A)) => ! [G] : ( m1_subset_1(G,u1_struct_0(A)) => ( ( r1_analoaf(A,B,C,D,E) & r1_analoaf(A,B,C,F,G) ) => ( B = C | r1_analoaf(A,D,E,F,G) ) ) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t16_analoaf,t16_analoaf,t13_analoaf,d9_rlvect_1,t13_analoaf,d9_rlvect_1,t124_xreal_1,t131_xreal_1,d1_analoaf,d1_analoaf]), [file(analoaf,t20_analoaf),interesting(0.00)]). fof(t21_analoaf,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_rlvect_1(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & v7_rlvect_1(A) & l2_rlvect_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ! [E] : ( m1_subset_1(E,u1_struct_0(A)) => ( r1_analoaf(A,B,C,D,E) => ( r1_analoaf(A,C,B,E,D) & r1_analoaf(A,D,E,B,C) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t16_analoaf,t10_analoaf,t10_analoaf,d1_analoaf,d1_analoaf]), [file(analoaf,t21_analoaf),interesting(0.00)]). fof(t43_rlvect_1,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_rlvect_1(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & l1_rlvect_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => k6_rlvect_1(A,B,k6_rlvect_1(A,C,D)) = k4_rlvect_1(A,k6_rlvect_1(A,B,C),D) ) ) ) ) ), file(rlvect_1,t43_rlvect_1), [interesting(0.00)]). fof(t4_analoaf,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_rlvect_1(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & v7_rlvect_1(A) & l2_rlvect_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => k4_rlvect_1(A,k6_rlvect_1(A,B,C),k6_rlvect_1(A,C,D)) = k6_rlvect_1(A,B,D) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t43_rlvect_1,t43_rlvect_1,t28_rlvect_1,t10_rlvect_1]), [file(analoaf,t4_analoaf),interesting(0.00)]). fof(t6_analoaf,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_rlvect_1(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & v7_rlvect_1(A) & l2_rlvect_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => k6_rlvect_1(A,B,k6_rlvect_1(A,C,D)) = k4_rlvect_1(A,B,k6_rlvect_1(A,D,C)) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t81_vectsp_1]), [file(analoaf,t6_analoaf),interesting(0.00)]). fof(t49_rlvect_1,theorem,( ! [A] : ( m1_subset_1(A,k1_numbers) => ! [B] : ( m1_subset_1(B,k1_numbers) => ! [C] : ( ( ~ v3_struct_0(C) & v3_rlvect_1(C) & v4_rlvect_1(C) & v5_rlvect_1(C) & v6_rlvect_1(C) & v7_rlvect_1(C) & l2_rlvect_1(C) ) => ! [D] : ( m1_subset_1(D,u1_struct_0(C)) => k3_rlvect_1(C,D,k5_real_1(A,B)) = k6_rlvect_1(C,k3_rlvect_1(C,D,A),k3_rlvect_1(C,D,B)) ) ) ) ) ), file(rlvect_1,t49_rlvect_1), [interesting(0.00)]). fof(t40_rlvect_1,theorem,( ! [A] : ( m1_subset_1(A,k1_numbers) => ! [B] : ( ( ~ v3_struct_0(B) & v3_rlvect_1(B) & v4_rlvect_1(B) & v5_rlvect_1(B) & v6_rlvect_1(B) & v7_rlvect_1(B) & l2_rlvect_1(B) ) => ! [C] : ( m1_subset_1(C,u1_struct_0(B)) => k3_rlvect_1(B,k5_rlvect_1(B,C),k1_real_1(A)) = k3_rlvect_1(B,C,A) ) ) ) ), file(rlvect_1,t40_rlvect_1), [interesting(0.00)]). fof(t50_rlvect_1,theorem,( ! [A] : ( m1_subset_1(A,k1_numbers) => ! [B] : ( ( ~ v3_struct_0(B) & v3_rlvect_1(B) & v4_rlvect_1(B) & v5_rlvect_1(B) & v6_rlvect_1(B) & v7_rlvect_1(B) & l2_rlvect_1(B) ) => ! [C] : ( m1_subset_1(C,u1_struct_0(B)) => ! [D] : ( m1_subset_1(D,u1_struct_0(B)) => ( k3_rlvect_1(B,C,A) = k3_rlvect_1(B,D,A) => ( A = 0 | C = D ) ) ) ) ) ) ), file(rlvect_1,t50_rlvect_1), [interesting(0.00)]). fof(t21_rlvect_1,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & l1_rlvect_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ! [E] : ( m1_subset_1(E,u1_struct_0(A)) => ( ( k2_rlvect_1(A,B,D) = k2_rlvect_1(A,B,E) | k2_rlvect_1(A,D,B) = k2_rlvect_1(A,E,B) ) => D = E ) ) ) ) ) ) ), file(rlvect_1,t21_rlvect_1), [interesting(0.00)]). fof(t57_xreal_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ~ ( A != B & r1_xreal_0(k6_xcmplx_0(A,B),0) & r1_xreal_0(k6_xcmplx_0(B,A),0) ) ) ) ), file(xreal_1,t57_xreal_1), [interesting(0.00)]). fof(t26_rlvect_1,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & l1_rlvect_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => k6_rlvect_1(A,B,k1_rlvect_1(A)) = B ) ) ), file(rlvect_1,t26_rlvect_1), [interesting(0.00)]). fof(t27_rlvect_1,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & l1_rlvect_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => k6_rlvect_1(A,k1_rlvect_1(A),B) = k5_rlvect_1(A,B) ) ) ), file(rlvect_1,t27_rlvect_1), [interesting(0.00)]). fof(t78_rlsub_2,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & l1_rlvect_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ( B = k2_rlvect_1(A,C,D) <=> C = k6_rlvect_1(A,B,D) ) ) ) ) ) ), file(rlsub_2,t78_rlsub_2), [interesting(0.00)]). fof(t24_analoaf,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_rlvect_1(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & v7_rlvect_1(A) & l2_rlvect_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ! [E] : ( m1_subset_1(E,u1_struct_0(A)) => ( k6_rlvect_1(A,B,C) = k6_rlvect_1(A,D,E) => r1_analoaf(A,C,B,E,D) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d1_analoaf]), [file(analoaf,t24_analoaf),interesting(0.00)]). fof(t22_rlvect_1,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & l1_rlvect_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ( ( k2_rlvect_1(A,B,C) = B | k2_rlvect_1(A,C,B) = B ) => C = k1_rlvect_1(A) ) ) ) ) ), file(rlvect_1,t22_rlvect_1), [interesting(0.00)]). fof(t5_analoaf,theorem,( $true ), file(analoaf,t5_analoaf), [interesting(0.00)]). fof(t7_analoaf,theorem,( $true ), file(analoaf,t7_analoaf), [interesting(0.00)]). fof(t8_analoaf,theorem,( $true ), file(analoaf,t8_analoaf), [interesting(0.00)]).