fof(t11_bilinear,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & l2_struct_0(A) ) => ! [B] : ( ( ~ v3_struct_0(B) & l4_vectsp_1(B,A) ) => ! [C] : ( ( ~ v3_struct_0(C) & l4_vectsp_1(C,A) ) => ! [D] : ( m1_subset_1(D,u1_struct_0(B)) => k9_bilinear(A,B,C,k1_bilinear(A,B,C),D) = k7_hahnban1(A,C) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t9_bilinear,t1_bilinear,t22_hahnban1,t113_funct_2]), [file(bilinear,t11_bilinear),interesting(1.00)]). fof(t12_bilinear,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & l2_struct_0(A) ) => ! [B] : ( ( ~ v3_struct_0(B) & l4_vectsp_1(B,A) ) => ! [C] : ( ( ~ v3_struct_0(C) & l4_vectsp_1(C,A) ) => ! [D] : ( m1_subset_1(D,u1_struct_0(C)) => k10_bilinear(A,B,C,k1_bilinear(A,B,C),D) = k7_hahnban1(A,B) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t10_bilinear,t1_bilinear,t22_hahnban1,t113_funct_2]), [file(bilinear,t12_bilinear),interesting(1.00)]). fof(t2_bilinear,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v5_rlvect_1(A) & l1_rlvect_1(A) ) => ! [B] : ( ( ~ v3_struct_0(B) & l4_vectsp_1(B,A) ) => ! [C] : ( ( ~ v3_struct_0(C) & l4_vectsp_1(C,A) ) => ! [D] : ( ( v1_funct_1(D) & v1_funct_2(D,k2_zfmisc_1(u1_struct_0(B),u1_struct_0(C)),u1_struct_0(A)) & m2_relset_1(D,k2_zfmisc_1(u1_struct_0(B),u1_struct_0(C)),u1_struct_0(A)) ) => k2_bilinear(A,B,C,D,k1_bilinear(A,B,C)) = D ) ) ) ) ), inference(mizar_proof,[status(thm)],[d3_bilinear,t1_bilinear,d7_rlvect_1,t120_funct_2]), [file(bilinear,t2_bilinear),interesting(0.95)]). fof(t6_bilinear,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v5_vectsp_1(A) & l3_vectsp_1(A) ) => ! [B] : ( ( ~ v3_struct_0(B) & l4_vectsp_1(B,A) ) => ! [C] : ( ( ~ v3_struct_0(C) & l4_vectsp_1(C,A) ) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ! [E] : ( m1_subset_1(E,u1_struct_0(A)) => ! [F] : ( ( v1_funct_1(F) & v1_funct_2(F,k2_zfmisc_1(u1_struct_0(B),u1_struct_0(C)),u1_struct_0(A)) & m2_relset_1(F,k2_zfmisc_1(u1_struct_0(B),u1_struct_0(C)),u1_struct_0(A)) ) => k3_bilinear(A,B,C,F,k2_rlvect_1(A,D,E)) = k2_bilinear(A,B,C,k3_bilinear(A,B,C,F,D),k3_bilinear(A,B,C,F,E)) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d4_bilinear,d12_vectsp_1,d4_bilinear,d4_bilinear,d3_bilinear,t120_funct_2]), [file(bilinear,t6_bilinear),interesting(0.92)]). fof(t17_bilinear,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & l1_rlvect_1(A) ) => ! [B] : ( ( ~ v3_struct_0(B) & l4_vectsp_1(B,A) ) => ! [C] : ( ( ~ v3_struct_0(C) & l4_vectsp_1(C,A) ) => ! [D] : ( ( v1_funct_1(D) & v1_funct_2(D,k2_zfmisc_1(u1_struct_0(B),u1_struct_0(C)),u1_struct_0(A)) & m2_relset_1(D,k2_zfmisc_1(u1_struct_0(B),u1_struct_0(C)),u1_struct_0(A)) ) => ! [E] : ( m1_subset_1(E,u1_struct_0(C)) => k10_bilinear(A,B,C,k4_bilinear(A,B,C,D),E) = k4_hahnban1(A,B,k10_bilinear(A,B,C,D,E)) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t10_bilinear,d5_bilinear,t10_bilinear,d7_hahnban1,t113_funct_2]), [file(bilinear,t17_bilinear),interesting(0.90)]). fof(t18_bilinear,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & l1_rlvect_1(A) ) => ! [B] : ( ( ~ v3_struct_0(B) & l4_vectsp_1(B,A) ) => ! [C] : ( ( ~ v3_struct_0(C) & l4_vectsp_1(C,A) ) => ! [D] : ( ( v1_funct_1(D) & v1_funct_2(D,k2_zfmisc_1(u1_struct_0(B),u1_struct_0(C)),u1_struct_0(A)) & m2_relset_1(D,k2_zfmisc_1(u1_struct_0(B),u1_struct_0(C)),u1_struct_0(A)) ) => ! [E] : ( m1_subset_1(E,u1_struct_0(B)) => k9_bilinear(A,B,C,k4_bilinear(A,B,C,D),E) = k4_hahnban1(A,C,k9_bilinear(A,B,C,D,E)) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t9_bilinear,d5_bilinear,t9_bilinear,d7_hahnban1,t113_funct_2]), [file(bilinear,t18_bilinear),interesting(0.90)]). fof(t15_bilinear,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & l3_vectsp_1(A) ) => ! [B] : ( ( ~ v3_struct_0(B) & l4_vectsp_1(B,A) ) => ! [C] : ( ( ~ v3_struct_0(C) & l4_vectsp_1(C,A) ) => ! [D] : ( ( v1_funct_1(D) & v1_funct_2(D,k2_zfmisc_1(u1_struct_0(B),u1_struct_0(C)),u1_struct_0(A)) & m2_relset_1(D,k2_zfmisc_1(u1_struct_0(B),u1_struct_0(C)),u1_struct_0(A)) ) => ! [E] : ( m1_subset_1(E,u1_struct_0(A)) => ! [F] : ( m1_subset_1(F,u1_struct_0(C)) => k10_bilinear(A,B,C,k3_bilinear(A,B,C,D,E),F) = k6_hahnban1(A,B,E,k10_bilinear(A,B,C,D,F)) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t10_bilinear,d4_bilinear,t10_bilinear,d9_hahnban1,t113_funct_2]), [file(bilinear,t15_bilinear),interesting(0.88)]). fof(t16_bilinear,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & l3_vectsp_1(A) ) => ! [B] : ( ( ~ v3_struct_0(B) & l4_vectsp_1(B,A) ) => ! [C] : ( ( ~ v3_struct_0(C) & l4_vectsp_1(C,A) ) => ! [D] : ( ( v1_funct_1(D) & v1_funct_2(D,k2_zfmisc_1(u1_struct_0(B),u1_struct_0(C)),u1_struct_0(A)) & m2_relset_1(D,k2_zfmisc_1(u1_struct_0(B),u1_struct_0(C)),u1_struct_0(A)) ) => ! [E] : ( m1_subset_1(E,u1_struct_0(A)) => ! [F] : ( m1_subset_1(F,u1_struct_0(B)) => k9_bilinear(A,B,C,k3_bilinear(A,B,C,D,E),F) = k6_hahnban1(A,C,E,k9_bilinear(A,B,C,D,F)) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t9_bilinear,d4_bilinear,t9_bilinear,d9_hahnban1,t113_funct_2]), [file(bilinear,t16_bilinear),interesting(0.88)]). fof(t4_bilinear,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & l1_rlvect_1(A) ) => ! [B] : ( ( ~ v3_struct_0(B) & l4_vectsp_1(B,A) ) => ! [C] : ( ( ~ v3_struct_0(C) & l4_vectsp_1(C,A) ) => ! [D] : ( ( v1_funct_1(D) & v1_funct_2(D,k2_zfmisc_1(u1_struct_0(B),u1_struct_0(C)),u1_struct_0(A)) & m2_relset_1(D,k2_zfmisc_1(u1_struct_0(B),u1_struct_0(C)),u1_struct_0(A)) ) => k7_bilinear(A,B,C,D,D) = k1_bilinear(A,B,C) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d8_bilinear,t28_rlvect_1,t1_bilinear,t120_funct_2]), [file(bilinear,t4_bilinear),interesting(0.87)]). fof(t60_bilinear,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & v4_vectsp_1(A) & l3_vectsp_1(A) ) => ! [B] : ( ( ~ v3_struct_0(B) & l4_vectsp_1(B,A) ) => ! [C] : ( ( v1_funct_1(C) & v1_funct_2(C,k2_zfmisc_1(u1_struct_0(B),u1_struct_0(B)),u1_struct_0(A)) & v1_bilinear(C,A,B,B) & v2_bilinear(C,A,B,B) & v3_bilinear(C,A,B,B) & v4_bilinear(C,A,B,B) & v8_bilinear(C,A,B) & m2_relset_1(C,k2_zfmisc_1(u1_struct_0(B),u1_struct_0(B)),u1_struct_0(A)) ) => k12_bilinear(A,B,B,C) = k13_bilinear(A,B,B,C) ) ) ) ), inference(mizar_proof,[status(thm)],[d3_tarski,t59_bilinear,t25_rlvect_1,d10_xboole_0,d3_tarski,t59_bilinear,t25_rlvect_1]), [file(bilinear,t60_bilinear),interesting(0.86)]). fof(t43_bilinear,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & v4_vectsp_1(A) & l3_vectsp_1(A) ) => ! [B] : ( ( ~ v3_struct_0(B) & l4_vectsp_1(B,A) ) => ! [C] : ( ( ~ v3_struct_0(C) & l4_vectsp_1(C,A) ) => ! [D] : ( ( v1_funct_1(D) & v1_funct_2(D,k2_zfmisc_1(u1_struct_0(B),u1_struct_0(C)),u1_struct_0(A)) & v2_bilinear(D,A,B,C) & v4_bilinear(D,A,B,C) & m2_relset_1(D,k2_zfmisc_1(u1_struct_0(B),u1_struct_0(C)),u1_struct_0(A)) ) => v1_vectsp_4(k12_bilinear(A,B,C,D),A,B) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t27_bilinear,d7_rlvect_1,d1_vectsp_4,t32_bilinear,t36_vectsp_1]), [file(bilinear,t43_bilinear),interesting(0.81)]). fof(t44_bilinear,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & v4_vectsp_1(A) & l3_vectsp_1(A) ) => ! [B] : ( ( ~ v3_struct_0(B) & l4_vectsp_1(B,A) ) => ! [C] : ( ( ~ v3_struct_0(C) & l4_vectsp_1(C,A) ) => ! [D] : ( ( v1_funct_1(D) & v1_funct_2(D,k2_zfmisc_1(u1_struct_0(B),u1_struct_0(C)),u1_struct_0(A)) & v1_bilinear(D,A,B,C) & v3_bilinear(D,A,B,C) & m2_relset_1(D,k2_zfmisc_1(u1_struct_0(B),u1_struct_0(C)),u1_struct_0(A)) ) => v1_vectsp_4(k13_bilinear(A,B,C,D),A,C) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t28_bilinear,d7_rlvect_1,d1_vectsp_4,t33_bilinear,t36_vectsp_1]), [file(bilinear,t44_bilinear),interesting(0.81)]). fof(t5_bilinear,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v4_vectsp_1(A) & l3_vectsp_1(A) ) => ! [B] : ( ( ~ v3_struct_0(B) & l4_vectsp_1(B,A) ) => ! [C] : ( ( ~ v3_struct_0(C) & l4_vectsp_1(C,A) ) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ! [E] : ( ( v1_funct_1(E) & v1_funct_2(E,k2_zfmisc_1(u1_struct_0(B),u1_struct_0(C)),u1_struct_0(A)) & m2_relset_1(E,k2_zfmisc_1(u1_struct_0(B),u1_struct_0(C)),u1_struct_0(A)) ) => ! [F] : ( ( v1_funct_1(F) & v1_funct_2(F,k2_zfmisc_1(u1_struct_0(B),u1_struct_0(C)),u1_struct_0(A)) & m2_relset_1(F,k2_zfmisc_1(u1_struct_0(B),u1_struct_0(C)),u1_struct_0(A)) ) => k3_bilinear(A,B,C,k2_bilinear(A,B,C,E,F),D) = k2_bilinear(A,B,C,k3_bilinear(A,B,C,E,D),k3_bilinear(A,B,C,F,D)) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d4_bilinear,d3_bilinear,d11_vectsp_1,d4_bilinear,d4_bilinear,d3_bilinear,t120_funct_2]), [file(bilinear,t5_bilinear),interesting(0.81)]). fof(t49_bilinear,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_rlvect_1(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & v4_group_1(A) & v7_vectsp_1(A) & v8_vectsp_1(A) & l3_vectsp_1(A) ) => ! [B] : ( ( ~ v3_struct_0(B) & v3_rlvect_1(B) & v4_rlvect_1(B) & v5_rlvect_1(B) & v6_rlvect_1(B) & v12_vectsp_1(B,A) & l4_vectsp_1(B,A) ) => ! [C] : ( ( ~ v3_struct_0(C) & v3_rlvect_1(C) & v4_rlvect_1(C) & v5_rlvect_1(C) & v6_rlvect_1(C) & v12_vectsp_1(C,A) & l4_vectsp_1(C,A) ) => ! [D] : ( ( v1_funct_1(D) & v1_funct_2(D,k2_zfmisc_1(u1_struct_0(B),u1_struct_0(C)),u1_struct_0(A)) & v1_bilinear(D,A,B,C) & v2_bilinear(D,A,B,C) & v3_bilinear(D,A,B,C) & v4_bilinear(D,A,B,C) & m2_relset_1(D,k2_zfmisc_1(u1_struct_0(B),u1_struct_0(C)),u1_struct_0(A)) ) => ( k19_bilinear(A,B,C,D) = k18_bilinear(A,k6_vectsp10(A,B,k15_bilinear(A,B,C,D)),C,k17_bilinear(A,B,C,D)) & k19_bilinear(A,B,C,D) = k17_bilinear(A,B,k6_vectsp10(A,C,k16_bilinear(A,B,C,D)),k18_bilinear(A,B,C,D)) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d1_funct_2,d1_funct_2,d1_funct_2,t47_bilinear,t48_bilinear,t9_domain_1,t23_vectsp10,t23_vectsp10,t47_bilinear,d23_bilinear,d21_bilinear,d22_bilinear,t9_funct_1,t9_domain_1,t23_vectsp10,t23_vectsp10,t48_bilinear,d23_bilinear,d22_bilinear,d21_bilinear,t9_funct_1]), [file(bilinear,t49_bilinear),interesting(0.72)]). fof(t52_bilinear,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & v4_group_1(A) & v7_group_1(A) & v7_vectsp_1(A) & v8_vectsp_1(A) & v9_vectsp_1(A) & l3_vectsp_1(A) ) => ! [B] : ( ( ~ v3_struct_0(B) & l4_vectsp_1(B,A) ) => ! [C] : ( ( ~ v3_struct_0(C) & l4_vectsp_1(C,A) ) => ! [D] : ( ( v1_funct_1(D) & v1_funct_2(D,u1_struct_0(B),u1_struct_0(A)) & m2_relset_1(D,u1_struct_0(B),u1_struct_0(A)) ) => ! [E] : ( ( v1_funct_1(E) & v1_funct_2(E,u1_struct_0(C),u1_struct_0(A)) & m2_relset_1(E,u1_struct_0(C),u1_struct_0(A)) ) => ( E != k7_hahnban1(A,C) => k12_bilinear(A,B,C,k11_bilinear(A,B,C,D,E)) = k8_vectsp10(A,B,D) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d9_vectsp10,d3_tarski,d11_bilinear,t44_vectsp_1,t22_hahnban1,t113_funct_2,d10_xboole_0,t51_bilinear]), [file(bilinear,t52_bilinear),interesting(0.72)]). fof(t54_bilinear,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & v4_group_1(A) & v7_group_1(A) & v7_vectsp_1(A) & v8_vectsp_1(A) & v9_vectsp_1(A) & l3_vectsp_1(A) ) => ! [B] : ( ( ~ v3_struct_0(B) & l4_vectsp_1(B,A) ) => ! [C] : ( ( ~ v3_struct_0(C) & l4_vectsp_1(C,A) ) => ! [D] : ( ( v1_funct_1(D) & v1_funct_2(D,u1_struct_0(B),u1_struct_0(A)) & m2_relset_1(D,u1_struct_0(B),u1_struct_0(A)) ) => ! [E] : ( ( v1_funct_1(E) & v1_funct_2(E,u1_struct_0(C),u1_struct_0(A)) & m2_relset_1(E,u1_struct_0(C),u1_struct_0(A)) ) => ( D != k7_hahnban1(A,B) => k13_bilinear(A,B,C,k11_bilinear(A,B,C,D,E)) = k8_vectsp10(A,C,E) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d9_vectsp10,d3_tarski,d11_bilinear,t44_vectsp_1,t22_hahnban1,t113_funct_2,d10_xboole_0,t53_bilinear]), [file(bilinear,t54_bilinear),interesting(0.72)]). fof(t45_bilinear,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_rlvect_1(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & v4_group_1(A) & v7_vectsp_1(A) & v8_vectsp_1(A) & l3_vectsp_1(A) ) => ! [B] : ( ( ~ v3_struct_0(B) & v3_rlvect_1(B) & v4_rlvect_1(B) & v5_rlvect_1(B) & v6_rlvect_1(B) & v12_vectsp_1(B,A) & l4_vectsp_1(B,A) ) => ! [C] : ( ( ~ v3_struct_0(C) & l4_vectsp_1(C,A) ) => ! [D] : ( ( v1_funct_1(D) & v1_funct_2(D,k2_zfmisc_1(u1_struct_0(B),u1_struct_0(C)),u1_struct_0(A)) & v2_bilinear(D,A,B,C) & v4_bilinear(D,A,B,C) & m2_relset_1(D,k2_zfmisc_1(u1_struct_0(B),u1_struct_0(C)),u1_struct_0(A)) ) => k13_bilinear(A,B,C,D) = k13_bilinear(A,k6_vectsp10(A,B,k15_bilinear(A,B,C,D)),C,k17_bilinear(A,B,C,D)) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d3_tarski,t23_vectsp10,d21_bilinear,d10_xboole_0,d3_tarski,t24_vectsp10,d21_bilinear]), [file(bilinear,t45_bilinear),interesting(0.67)]). fof(t46_bilinear,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_rlvect_1(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & v4_group_1(A) & v7_vectsp_1(A) & v8_vectsp_1(A) & l3_vectsp_1(A) ) => ! [B] : ( ( ~ v3_struct_0(B) & l4_vectsp_1(B,A) ) => ! [C] : ( ( ~ v3_struct_0(C) & v3_rlvect_1(C) & v4_rlvect_1(C) & v5_rlvect_1(C) & v6_rlvect_1(C) & v12_vectsp_1(C,A) & l4_vectsp_1(C,A) ) => ! [D] : ( ( v1_funct_1(D) & v1_funct_2(D,k2_zfmisc_1(u1_struct_0(B),u1_struct_0(C)),u1_struct_0(A)) & v1_bilinear(D,A,B,C) & v3_bilinear(D,A,B,C) & m2_relset_1(D,k2_zfmisc_1(u1_struct_0(B),u1_struct_0(C)),u1_struct_0(A)) ) => k12_bilinear(A,B,C,D) = k12_bilinear(A,B,k6_vectsp10(A,C,k16_bilinear(A,B,C,D)),k18_bilinear(A,B,C,D)) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d3_tarski,t23_vectsp10,d22_bilinear,d10_xboole_0,d3_tarski,t24_vectsp10,d22_bilinear]), [file(bilinear,t46_bilinear),interesting(0.67)]). fof(t47_bilinear,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_rlvect_1(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & v4_group_1(A) & v7_vectsp_1(A) & v8_vectsp_1(A) & l3_vectsp_1(A) ) => ! [B] : ( ( ~ v3_struct_0(B) & v3_rlvect_1(B) & v4_rlvect_1(B) & v5_rlvect_1(B) & v6_rlvect_1(B) & v12_vectsp_1(B,A) & l4_vectsp_1(B,A) ) => ! [C] : ( ( ~ v3_struct_0(C) & v3_rlvect_1(C) & v4_rlvect_1(C) & v5_rlvect_1(C) & v6_rlvect_1(C) & v12_vectsp_1(C,A) & l4_vectsp_1(C,A) ) => ! [D] : ( ( v1_funct_1(D) & v1_funct_2(D,k2_zfmisc_1(u1_struct_0(B),u1_struct_0(C)),u1_struct_0(A)) & v1_bilinear(D,A,B,C) & v2_bilinear(D,A,B,C) & v3_bilinear(D,A,B,C) & v4_bilinear(D,A,B,C) & m2_relset_1(D,k2_zfmisc_1(u1_struct_0(B),u1_struct_0(C)),u1_struct_0(A)) ) => k16_bilinear(A,B,C,D) = k16_bilinear(A,k6_vectsp10(A,B,k15_bilinear(A,B,C,D)),C,k17_bilinear(A,B,C,D)) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d20_bilinear,t45_bilinear,d20_bilinear,t37_vectsp_4]), [file(bilinear,t47_bilinear),interesting(0.60)]). fof(t48_bilinear,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_rlvect_1(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & v4_group_1(A) & v7_vectsp_1(A) & v8_vectsp_1(A) & l3_vectsp_1(A) ) => ! [B] : ( ( ~ v3_struct_0(B) & v3_rlvect_1(B) & v4_rlvect_1(B) & v5_rlvect_1(B) & v6_rlvect_1(B) & v12_vectsp_1(B,A) & l4_vectsp_1(B,A) ) => ! [C] : ( ( ~ v3_struct_0(C) & v3_rlvect_1(C) & v4_rlvect_1(C) & v5_rlvect_1(C) & v6_rlvect_1(C) & v12_vectsp_1(C,A) & l4_vectsp_1(C,A) ) => ! [D] : ( ( v1_funct_1(D) & v1_funct_2(D,k2_zfmisc_1(u1_struct_0(B),u1_struct_0(C)),u1_struct_0(A)) & v1_bilinear(D,A,B,C) & v2_bilinear(D,A,B,C) & v3_bilinear(D,A,B,C) & v4_bilinear(D,A,B,C) & m2_relset_1(D,k2_zfmisc_1(u1_struct_0(B),u1_struct_0(C)),u1_struct_0(A)) ) => k15_bilinear(A,B,C,D) = k15_bilinear(A,B,k6_vectsp10(A,C,k16_bilinear(A,B,C,D)),k18_bilinear(A,B,C,D)) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d19_bilinear,t46_bilinear,d19_bilinear,t37_vectsp_4]), [file(bilinear,t48_bilinear),interesting(0.60)]). fof(t21_bilinear,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & v4_vectsp_1(A) & l3_vectsp_1(A) ) => ! [B] : ( ( ~ v3_struct_0(B) & l4_vectsp_1(B,A) ) => ! [C] : ( ( ~ v3_struct_0(C) & l4_vectsp_1(C,A) ) => ! [D] : ( ( v1_funct_1(D) & v1_funct_2(D,u1_struct_0(B),u1_struct_0(A)) & m2_relset_1(D,u1_struct_0(B),u1_struct_0(A)) ) => ! [E] : ( m1_subset_1(E,u1_struct_0(B)) => ! [F] : ( m1_subset_1(F,u1_struct_0(C)) => k8_funct_2(k2_zfmisc_1(u1_struct_0(B),u1_struct_0(C)),u1_struct_0(A),k11_bilinear(A,B,C,D,k7_hahnban1(A,C)),k1_domain_1(u1_struct_0(B),u1_struct_0(C),E,F)) = k1_rlvect_1(A) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t12_pre_topc,d11_bilinear,t13_funcop_1,t36_vectsp_1]), [file(bilinear,t21_bilinear),interesting(0.54)]). fof(t22_bilinear,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & v5_vectsp_1(A) & l3_vectsp_1(A) ) => ! [B] : ( ( ~ v3_struct_0(B) & l4_vectsp_1(B,A) ) => ! [C] : ( ( ~ v3_struct_0(C) & l4_vectsp_1(C,A) ) => ! [D] : ( ( v1_funct_1(D) & v1_funct_2(D,u1_struct_0(C),u1_struct_0(A)) & m2_relset_1(D,u1_struct_0(C),u1_struct_0(A)) ) => ! [E] : ( m1_subset_1(E,u1_struct_0(B)) => ! [F] : ( m1_subset_1(F,u1_struct_0(C)) => k8_funct_2(k2_zfmisc_1(u1_struct_0(B),u1_struct_0(C)),u1_struct_0(A),k11_bilinear(A,B,C,k7_hahnban1(A,B),D),k1_domain_1(u1_struct_0(B),u1_struct_0(C),E,F)) = k1_rlvect_1(A) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t12_pre_topc,d11_bilinear,t13_funcop_1,t39_vectsp_1]), [file(bilinear,t22_bilinear),interesting(0.54)]). fof(t55_bilinear,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_rlvect_1(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & v4_group_1(A) & v7_group_1(A) & v7_vectsp_1(A) & v8_vectsp_1(A) & v9_vectsp_1(A) & l3_vectsp_1(A) ) => ! [B] : ( ( ~ v3_struct_0(B) & v3_rlvect_1(B) & v4_rlvect_1(B) & v5_rlvect_1(B) & v6_rlvect_1(B) & v12_vectsp_1(B,A) & l4_vectsp_1(B,A) ) => ! [C] : ( ( ~ v3_struct_0(C) & l4_vectsp_1(C,A) ) => ! [D] : ( ( v1_funct_1(D) & v1_funct_2(D,u1_struct_0(B),u1_struct_0(A)) & v1_hahnban1(D,A,B) & v2_hahnban1(D,A,B) & m2_relset_1(D,u1_struct_0(B),u1_struct_0(A)) ) => ! [E] : ( ( v1_funct_1(E) & v1_funct_2(E,u1_struct_0(C),u1_struct_0(A)) & m2_relset_1(E,u1_struct_0(C),u1_struct_0(A)) ) => ( E != k7_hahnban1(A,C) => ( k15_bilinear(A,B,C,k11_bilinear(A,B,C,D,E)) = k9_vectsp10(A,B,D) & k17_bilinear(A,B,C,k11_bilinear(A,B,C,D,E)) = k11_bilinear(A,k6_vectsp10(A,B,k9_vectsp10(A,B,D)),C,k11_vectsp10(A,B,D),E) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d19_bilinear,t52_bilinear,d11_vectsp10,d1_funct_2,d1_funct_2,t9_domain_1,t23_vectsp10,d11_bilinear,t36_vectsp10,d11_bilinear,d21_bilinear,t9_funct_1]), [file(bilinear,t55_bilinear),interesting(0.52)]). fof(t56_bilinear,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_rlvect_1(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & v4_group_1(A) & v7_group_1(A) & v7_vectsp_1(A) & v8_vectsp_1(A) & v9_vectsp_1(A) & l3_vectsp_1(A) ) => ! [B] : ( ( ~ v3_struct_0(B) & l4_vectsp_1(B,A) ) => ! [C] : ( ( ~ v3_struct_0(C) & v3_rlvect_1(C) & v4_rlvect_1(C) & v5_rlvect_1(C) & v6_rlvect_1(C) & v12_vectsp_1(C,A) & l4_vectsp_1(C,A) ) => ! [D] : ( ( v1_funct_1(D) & v1_funct_2(D,u1_struct_0(B),u1_struct_0(A)) & m2_relset_1(D,u1_struct_0(B),u1_struct_0(A)) ) => ! [E] : ( ( v1_funct_1(E) & v1_funct_2(E,u1_struct_0(C),u1_struct_0(A)) & v1_hahnban1(E,A,C) & v2_hahnban1(E,A,C) & m2_relset_1(E,u1_struct_0(C),u1_struct_0(A)) ) => ( D != k7_hahnban1(A,B) => ( k16_bilinear(A,B,C,k11_bilinear(A,B,C,D,E)) = k9_vectsp10(A,C,E) & k18_bilinear(A,B,C,k11_bilinear(A,B,C,D,E)) = k11_bilinear(A,B,k6_vectsp10(A,C,k9_vectsp10(A,C,E)),D,k11_vectsp10(A,C,E)) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d20_bilinear,t54_bilinear,d11_vectsp10,d1_funct_2,d1_funct_2,t9_domain_1,t23_vectsp10,d11_bilinear,t36_vectsp10,d11_bilinear,d22_bilinear,t9_funct_1]), [file(bilinear,t56_bilinear),interesting(0.52)]). fof(t36_bilinear,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_rlvect_1(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & v4_group_1(A) & v7_vectsp_1(A) & v8_vectsp_1(A) & l3_vectsp_1(A) ) => ! [B] : ( ( ~ v3_struct_0(B) & v3_rlvect_1(B) & v4_rlvect_1(B) & v5_rlvect_1(B) & v6_rlvect_1(B) & v12_vectsp_1(B,A) & l4_vectsp_1(B,A) ) => ! [C] : ( ( ~ v3_struct_0(C) & v3_rlvect_1(C) & v4_rlvect_1(C) & v5_rlvect_1(C) & v6_rlvect_1(C) & v12_vectsp_1(C,A) & l4_vectsp_1(C,A) ) => ! [D] : ( m1_subset_1(D,u1_struct_0(B)) => ! [E] : ( m1_subset_1(E,u1_struct_0(B)) => ! [F] : ( m1_subset_1(F,u1_struct_0(C)) => ! [G] : ( ( v1_funct_1(G) & v1_funct_2(G,k2_zfmisc_1(u1_struct_0(B),u1_struct_0(C)),u1_struct_0(A)) & v2_bilinear(G,A,B,C) & v4_bilinear(G,A,B,C) & m2_relset_1(G,k2_zfmisc_1(u1_struct_0(B),u1_struct_0(C)),u1_struct_0(A)) ) => k8_funct_2(k2_zfmisc_1(u1_struct_0(B),u1_struct_0(C)),u1_struct_0(A),G,k1_domain_1(u1_struct_0(B),u1_struct_0(C),k6_rlvect_1(B,D,E),F)) = k6_rlvect_1(A,k8_funct_2(k2_zfmisc_1(u1_struct_0(B),u1_struct_0(C)),u1_struct_0(A),G,k1_domain_1(u1_struct_0(B),u1_struct_0(C),D,F)),k8_funct_2(k2_zfmisc_1(u1_struct_0(B),u1_struct_0(C)),u1_struct_0(A),G,k1_domain_1(u1_struct_0(B),u1_struct_0(C),E,F))) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d11_rlvect_1,t27_bilinear,t59_vectsp_1,t32_bilinear,t41_vectsp_1,d11_rlvect_1,d19_vectsp_1]), [file(bilinear,t36_bilinear),interesting(0.47)]). fof(t37_bilinear,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_rlvect_1(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & v4_group_1(A) & v7_vectsp_1(A) & v8_vectsp_1(A) & l3_vectsp_1(A) ) => ! [B] : ( ( ~ v3_struct_0(B) & v3_rlvect_1(B) & v4_rlvect_1(B) & v5_rlvect_1(B) & v6_rlvect_1(B) & v12_vectsp_1(B,A) & l4_vectsp_1(B,A) ) => ! [C] : ( ( ~ v3_struct_0(C) & v3_rlvect_1(C) & v4_rlvect_1(C) & v5_rlvect_1(C) & v6_rlvect_1(C) & v12_vectsp_1(C,A) & l4_vectsp_1(C,A) ) => ! [D] : ( m1_subset_1(D,u1_struct_0(B)) => ! [E] : ( m1_subset_1(E,u1_struct_0(C)) => ! [F] : ( m1_subset_1(F,u1_struct_0(C)) => ! [G] : ( ( v1_funct_1(G) & v1_funct_2(G,k2_zfmisc_1(u1_struct_0(B),u1_struct_0(C)),u1_struct_0(A)) & v1_bilinear(G,A,B,C) & v3_bilinear(G,A,B,C) & m2_relset_1(G,k2_zfmisc_1(u1_struct_0(B),u1_struct_0(C)),u1_struct_0(A)) ) => k8_funct_2(k2_zfmisc_1(u1_struct_0(B),u1_struct_0(C)),u1_struct_0(A),G,k1_domain_1(u1_struct_0(B),u1_struct_0(C),D,k6_rlvect_1(C,E,F))) = k6_rlvect_1(A,k8_funct_2(k2_zfmisc_1(u1_struct_0(B),u1_struct_0(C)),u1_struct_0(A),G,k1_domain_1(u1_struct_0(B),u1_struct_0(C),D,E)),k8_funct_2(k2_zfmisc_1(u1_struct_0(B),u1_struct_0(C)),u1_struct_0(A),G,k1_domain_1(u1_struct_0(B),u1_struct_0(C),D,F))) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d11_rlvect_1,t28_bilinear,t59_vectsp_1,t33_bilinear,t41_vectsp_1,d11_rlvect_1,d19_vectsp_1]), [file(bilinear,t37_bilinear),interesting(0.47)]). fof(t57_bilinear,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_rlvect_1(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & v4_group_1(A) & v7_group_1(A) & v7_vectsp_1(A) & v8_vectsp_1(A) & v9_vectsp_1(A) & ~ v10_vectsp_1(A) & l3_vectsp_1(A) ) => ! [B] : ( ( ~ v3_struct_0(B) & v3_rlvect_1(B) & v4_rlvect_1(B) & v5_rlvect_1(B) & v6_rlvect_1(B) & v12_vectsp_1(B,A) & ~ v3_realset2(B) & l4_vectsp_1(B,A) ) => ! [C] : ( ( ~ v3_struct_0(C) & v3_rlvect_1(C) & v4_rlvect_1(C) & v5_rlvect_1(C) & v6_rlvect_1(C) & v12_vectsp_1(C,A) & ~ v3_realset2(C) & l4_vectsp_1(C,A) ) => ! [D] : ( ( v1_funct_1(D) & v1_funct_2(D,u1_struct_0(B),u1_struct_0(A)) & ~ v5_seqm_3(D) & v1_hahnban1(D,A,B) & v2_hahnban1(D,A,B) & m2_relset_1(D,u1_struct_0(B),u1_struct_0(A)) ) => ! [E] : ( ( v1_funct_1(E) & v1_funct_2(E,u1_struct_0(C),u1_struct_0(A)) & ~ v5_seqm_3(E) & v1_hahnban1(E,A,C) & v2_hahnban1(E,A,C) & m2_relset_1(E,u1_struct_0(C),u1_struct_0(A)) ) => k19_bilinear(A,B,C,k11_bilinear(A,B,C,D,E)) = k11_bilinear(A,k6_vectsp10(A,B,k9_vectsp10(A,B,D)),k6_vectsp10(A,C,k9_vectsp10(A,C,E)),k11_vectsp10(A,B,D),k11_vectsp10(A,C,E)) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t55_bilinear,t49_bilinear,t55_bilinear,t56_bilinear]), [file(bilinear,t57_bilinear),interesting(0.44)]). fof(t34_bilinear,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & v4_group_1(A) & v7_vectsp_1(A) & v8_vectsp_1(A) & l3_vectsp_1(A) ) => ! [B] : ( ( ~ v3_struct_0(B) & v4_rlvect_1(B) & v5_rlvect_1(B) & v6_rlvect_1(B) & v12_vectsp_1(B,A) & l4_vectsp_1(B,A) ) => ! [C] : ( ( ~ v3_struct_0(C) & v4_rlvect_1(C) & v5_rlvect_1(C) & v6_rlvect_1(C) & v12_vectsp_1(C,A) & l4_vectsp_1(C,A) ) => ! [D] : ( ( v1_funct_1(D) & v1_funct_2(D,k2_zfmisc_1(u1_struct_0(B),u1_struct_0(C)),u1_struct_0(A)) & v4_bilinear(D,A,B,C) & m2_relset_1(D,k2_zfmisc_1(u1_struct_0(B),u1_struct_0(C)),u1_struct_0(A)) ) => ! [E] : ( m1_subset_1(E,u1_struct_0(C)) => k8_funct_2(k2_zfmisc_1(u1_struct_0(B),u1_struct_0(C)),u1_struct_0(A),D,k1_domain_1(u1_struct_0(B),u1_struct_0(C),k1_rlvect_1(B),E)) = k1_rlvect_1(A) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t2_vectsp10,t32_bilinear,t39_vectsp_1]), [file(bilinear,t34_bilinear),interesting(0.40)]). fof(t35_bilinear,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & v4_group_1(A) & v7_vectsp_1(A) & v8_vectsp_1(A) & l3_vectsp_1(A) ) => ! [B] : ( ( ~ v3_struct_0(B) & v4_rlvect_1(B) & v5_rlvect_1(B) & v6_rlvect_1(B) & v12_vectsp_1(B,A) & l4_vectsp_1(B,A) ) => ! [C] : ( ( ~ v3_struct_0(C) & v4_rlvect_1(C) & v5_rlvect_1(C) & v6_rlvect_1(C) & v12_vectsp_1(C,A) & l4_vectsp_1(C,A) ) => ! [D] : ( ( v1_funct_1(D) & v1_funct_2(D,k2_zfmisc_1(u1_struct_0(B),u1_struct_0(C)),u1_struct_0(A)) & v3_bilinear(D,A,B,C) & m2_relset_1(D,k2_zfmisc_1(u1_struct_0(B),u1_struct_0(C)),u1_struct_0(A)) ) => ! [E] : ( m1_subset_1(E,u1_struct_0(B)) => k8_funct_2(k2_zfmisc_1(u1_struct_0(B),u1_struct_0(C)),u1_struct_0(A),D,k1_domain_1(u1_struct_0(B),u1_struct_0(C),E,k1_rlvect_1(C))) = k1_rlvect_1(A) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t2_vectsp10,t33_bilinear,t39_vectsp_1]), [file(bilinear,t35_bilinear),interesting(0.40)]). fof(t38_bilinear,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_rlvect_1(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & v4_group_1(A) & v7_vectsp_1(A) & v8_vectsp_1(A) & l3_vectsp_1(A) ) => ! [B] : ( ( ~ v3_struct_0(B) & v3_rlvect_1(B) & v4_rlvect_1(B) & v5_rlvect_1(B) & v6_rlvect_1(B) & v12_vectsp_1(B,A) & l4_vectsp_1(B,A) ) => ! [C] : ( ( ~ v3_struct_0(C) & v3_rlvect_1(C) & v4_rlvect_1(C) & v5_rlvect_1(C) & v6_rlvect_1(C) & v12_vectsp_1(C,A) & l4_vectsp_1(C,A) ) => ! [D] : ( m1_subset_1(D,u1_struct_0(B)) => ! [E] : ( m1_subset_1(E,u1_struct_0(B)) => ! [F] : ( m1_subset_1(F,u1_struct_0(C)) => ! [G] : ( m1_subset_1(G,u1_struct_0(C)) => ! [H] : ( ( v1_funct_1(H) & v1_funct_2(H,k2_zfmisc_1(u1_struct_0(B),u1_struct_0(C)),u1_struct_0(A)) & v1_bilinear(H,A,B,C) & v2_bilinear(H,A,B,C) & v3_bilinear(H,A,B,C) & v4_bilinear(H,A,B,C) & m2_relset_1(H,k2_zfmisc_1(u1_struct_0(B),u1_struct_0(C)),u1_struct_0(A)) ) => k8_funct_2(k2_zfmisc_1(u1_struct_0(B),u1_struct_0(C)),u1_struct_0(A),H,k1_domain_1(u1_struct_0(B),u1_struct_0(C),k6_rlvect_1(B,D,E),k6_rlvect_1(C,F,G))) = k6_rlvect_1(A,k6_rlvect_1(A,k8_funct_2(k2_zfmisc_1(u1_struct_0(B),u1_struct_0(C)),u1_struct_0(A),H,k1_domain_1(u1_struct_0(B),u1_struct_0(C),D,F)),k8_funct_2(k2_zfmisc_1(u1_struct_0(B),u1_struct_0(C)),u1_struct_0(A),H,k1_domain_1(u1_struct_0(B),u1_struct_0(C),D,G))),k6_rlvect_1(A,k8_funct_2(k2_zfmisc_1(u1_struct_0(B),u1_struct_0(C)),u1_struct_0(A),H,k1_domain_1(u1_struct_0(B),u1_struct_0(C),E,F)),k8_funct_2(k2_zfmisc_1(u1_struct_0(B),u1_struct_0(C)),u1_struct_0(A),H,k1_domain_1(u1_struct_0(B),u1_struct_0(C),E,G)))) ) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t36_bilinear,t37_bilinear,t37_bilinear]), [file(bilinear,t38_bilinear),interesting(0.38)]). fof(t50_bilinear,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_rlvect_1(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & v4_group_1(A) & v7_vectsp_1(A) & v8_vectsp_1(A) & l3_vectsp_1(A) ) => ! [B] : ( ( ~ v3_struct_0(B) & v3_rlvect_1(B) & v4_rlvect_1(B) & v5_rlvect_1(B) & v6_rlvect_1(B) & v12_vectsp_1(B,A) & l4_vectsp_1(B,A) ) => ! [C] : ( ( ~ v3_struct_0(C) & v3_rlvect_1(C) & v4_rlvect_1(C) & v5_rlvect_1(C) & v6_rlvect_1(C) & v12_vectsp_1(C,A) & l4_vectsp_1(C,A) ) => ! [D] : ( ( v1_funct_1(D) & v1_funct_2(D,k2_zfmisc_1(u1_struct_0(B),u1_struct_0(C)),u1_struct_0(A)) & v1_bilinear(D,A,B,C) & v2_bilinear(D,A,B,C) & v3_bilinear(D,A,B,C) & v4_bilinear(D,A,B,C) & m2_relset_1(D,k2_zfmisc_1(u1_struct_0(B),u1_struct_0(C)),u1_struct_0(A)) ) => ( k12_bilinear(A,k6_vectsp10(A,B,k15_bilinear(A,B,C,D)),k6_vectsp10(A,C,k16_bilinear(A,B,C,D)),k19_bilinear(A,B,C,D)) = k12_bilinear(A,k6_vectsp10(A,B,k15_bilinear(A,B,C,D)),k6_vectsp10(A,C,k16_bilinear(A,k6_vectsp10(A,B,k15_bilinear(A,B,C,D)),C,k17_bilinear(A,B,C,D))),k18_bilinear(A,k6_vectsp10(A,B,k15_bilinear(A,B,C,D)),C,k17_bilinear(A,B,C,D))) & k13_bilinear(A,k6_vectsp10(A,B,k15_bilinear(A,B,C,D)),k6_vectsp10(A,C,k16_bilinear(A,B,C,D)),k19_bilinear(A,B,C,D)) = k13_bilinear(A,k6_vectsp10(A,B,k15_bilinear(A,B,C,D)),k6_vectsp10(A,C,k16_bilinear(A,k6_vectsp10(A,B,k15_bilinear(A,B,C,D)),C,k17_bilinear(A,B,C,D))),k18_bilinear(A,k6_vectsp10(A,B,k15_bilinear(A,B,C,D)),C,k17_bilinear(A,B,C,D))) & k12_bilinear(A,k6_vectsp10(A,B,k15_bilinear(A,B,C,D)),k6_vectsp10(A,C,k16_bilinear(A,B,C,D)),k19_bilinear(A,B,C,D)) = k12_bilinear(A,k6_vectsp10(A,B,k15_bilinear(A,B,k6_vectsp10(A,C,k16_bilinear(A,B,C,D)),k18_bilinear(A,B,C,D))),k6_vectsp10(A,C,k16_bilinear(A,B,C,D)),k17_bilinear(A,B,k6_vectsp10(A,C,k16_bilinear(A,B,C,D)),k18_bilinear(A,B,C,D))) & k13_bilinear(A,k6_vectsp10(A,B,k15_bilinear(A,B,C,D)),k6_vectsp10(A,C,k16_bilinear(A,B,C,D)),k19_bilinear(A,B,C,D)) = k13_bilinear(A,k6_vectsp10(A,B,k15_bilinear(A,B,k6_vectsp10(A,C,k16_bilinear(A,B,C,D)),k18_bilinear(A,B,C,D))),k6_vectsp10(A,C,k16_bilinear(A,B,C,D)),k17_bilinear(A,B,k6_vectsp10(A,C,k16_bilinear(A,B,C,D)),k18_bilinear(A,B,C,D))) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d3_tarski,t47_bilinear,t49_bilinear,d10_xboole_0,d3_tarski,t47_bilinear,t49_bilinear,d3_tarski,t47_bilinear,t49_bilinear,d10_xboole_0,d3_tarski,t47_bilinear,t49_bilinear,d3_tarski,t48_bilinear,t49_bilinear,d10_xboole_0,d3_tarski,t48_bilinear,t49_bilinear,d3_tarski,t48_bilinear,t49_bilinear,d10_xboole_0,d3_tarski,t48_bilinear,t49_bilinear]), [file(bilinear,t50_bilinear),interesting(0.20)]). fof(t39_bilinear,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & v4_group_1(A) & v7_vectsp_1(A) & v8_vectsp_1(A) & l3_vectsp_1(A) ) => ! [B] : ( ( ~ v3_struct_0(B) & v4_rlvect_1(B) & v5_rlvect_1(B) & v6_rlvect_1(B) & v12_vectsp_1(B,A) & l4_vectsp_1(B,A) ) => ! [C] : ( ( ~ v3_struct_0(C) & v4_rlvect_1(C) & v5_rlvect_1(C) & v6_rlvect_1(C) & v12_vectsp_1(C,A) & l4_vectsp_1(C,A) ) => ! [D] : ( m1_subset_1(D,u1_struct_0(B)) => ! [E] : ( m1_subset_1(E,u1_struct_0(B)) => ! [F] : ( m1_subset_1(F,u1_struct_0(C)) => ! [G] : ( m1_subset_1(G,u1_struct_0(C)) => ! [H] : ( m1_subset_1(H,u1_struct_0(A)) => ! [I] : ( m1_subset_1(I,u1_struct_0(A)) => ! [J] : ( ( v1_funct_1(J) & v1_funct_2(J,k2_zfmisc_1(u1_struct_0(B),u1_struct_0(C)),u1_struct_0(A)) & v1_bilinear(J,A,B,C) & v2_bilinear(J,A,B,C) & v3_bilinear(J,A,B,C) & v4_bilinear(J,A,B,C) & m2_relset_1(J,k2_zfmisc_1(u1_struct_0(B),u1_struct_0(C)),u1_struct_0(A)) ) => k8_funct_2(k2_zfmisc_1(u1_struct_0(B),u1_struct_0(C)),u1_struct_0(A),J,k1_domain_1(u1_struct_0(B),u1_struct_0(C),k2_rlvect_1(B,D,k6_vectsp_1(A,B,H,E)),k2_rlvect_1(C,F,k6_vectsp_1(A,C,I,G)))) = k2_rlvect_1(A,k2_rlvect_1(A,k8_funct_2(k2_zfmisc_1(u1_struct_0(B),u1_struct_0(C)),u1_struct_0(A),J,k1_domain_1(u1_struct_0(B),u1_struct_0(C),D,F)),k1_group_1(A,I,k8_funct_2(k2_zfmisc_1(u1_struct_0(B),u1_struct_0(C)),u1_struct_0(A),J,k1_domain_1(u1_struct_0(B),u1_struct_0(C),D,G)))),k2_rlvect_1(A,k1_group_1(A,H,k8_funct_2(k2_zfmisc_1(u1_struct_0(B),u1_struct_0(C)),u1_struct_0(A),J,k1_domain_1(u1_struct_0(B),u1_struct_0(C),E,F))),k1_group_1(A,H,k1_group_1(A,I,k8_funct_2(k2_zfmisc_1(u1_struct_0(B),u1_struct_0(C)),u1_struct_0(A),J,k1_domain_1(u1_struct_0(B),u1_struct_0(C),E,G)))))) ) ) ) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t29_bilinear,t33_bilinear,t32_bilinear,t32_bilinear,t33_bilinear]), [file(bilinear,t39_bilinear),interesting(0.02)]). fof(d1_funct_2,definition,( ! [A,B,C] : ( m2_relset_1(C,A,B) => ( ( ( B = k1_xboole_0 => A = k1_xboole_0 ) => ( v1_funct_2(C,A,B) <=> A = k4_relset_1(A,B,C) ) ) & ( B = k1_xboole_0 => ( A = k1_xboole_0 | ( v1_funct_2(C,A,B) <=> C = k1_xboole_0 ) ) ) ) ) ), file(funct_2,d1_funct_2), [interesting(0.00)]). fof(t36_funct_5,theorem,( ! [A,B,C,D] : ( ( v1_relat_1(D) & v1_funct_1(D) ) => ~ ( k2_zfmisc_1(A,B) != k1_xboole_0 & k1_relat_1(D) = k2_zfmisc_1(A,B) & r2_hidden(C,A) & ! [E] : ( ( v1_relat_1(E) & v1_funct_1(E) ) => ~ ( k1_funct_1(k3_funct_5(D),C) = E & k1_relat_1(E) = B & r1_tarski(k2_relat_1(E),k2_relat_1(D)) & ! [F] : ( r2_hidden(F,B) => k1_funct_1(E,F) = k1_funct_1(D,k4_tarski(C,F)) ) ) ) ) ) ), file(funct_5,t36_funct_5), [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(t4_funct_2,theorem,( ! [A,B] : ( ( v1_relat_1(B) & v1_funct_1(B) ) => ( r1_tarski(k2_relat_1(B),A) => ( v1_funct_1(B) & v1_funct_2(B,k1_relat_1(B),A) & m2_relset_1(B,k1_relat_1(B),A) ) ) ) ), file(funct_2,t4_funct_2), [interesting(0.00)]). fof(t39_funct_5,theorem,( ! [A,B,C,D] : ( ( v1_relat_1(D) & v1_funct_1(D) ) => ~ ( k2_zfmisc_1(A,B) != k1_xboole_0 & k1_relat_1(D) = k2_zfmisc_1(A,B) & r2_hidden(C,B) & ! [E] : ( ( v1_relat_1(E) & v1_funct_1(E) ) => ~ ( k1_funct_1(k5_funct_5(D),C) = E & k1_relat_1(E) = A & r1_tarski(k2_relat_1(E),k2_relat_1(D)) & ! [F] : ( r2_hidden(F,A) => k1_funct_1(E,F) = k1_funct_1(D,k4_tarski(F,C)) ) ) ) ) ) ), file(funct_5,t39_funct_5), [interesting(0.00)]). fof(l18_bilinear,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & l1_struct_0(A) ) => ! [B] : ( ( ~ v3_struct_0(B) & l4_vectsp_1(B,A) ) => ! [C] : ( ( ~ v3_struct_0(C) & l4_vectsp_1(C,A) ) => ! [D] : ( ( v1_funct_1(D) & v1_funct_2(D,k2_zfmisc_1(u1_struct_0(B),u1_struct_0(C)),u1_struct_0(A)) & m2_relset_1(D,k2_zfmisc_1(u1_struct_0(B),u1_struct_0(C)),u1_struct_0(A)) ) => ! [E] : ( m1_subset_1(E,u1_struct_0(B)) => ! [F] : ( m1_subset_1(F,u1_struct_0(C)) => ( v1_funct_1(k1_funct_1(k3_funct_5(D),E)) & v1_funct_2(k1_funct_1(k3_funct_5(D),E),u1_struct_0(C),u1_struct_0(A)) & m2_relset_1(k1_funct_1(k3_funct_5(D),E),u1_struct_0(C),u1_struct_0(A)) & v1_funct_1(k1_funct_1(k5_funct_5(D),F)) & v1_funct_2(k1_funct_1(k5_funct_5(D),F),u1_struct_0(B),u1_struct_0(A)) & m2_relset_1(k1_funct_1(k5_funct_5(D),F),u1_struct_0(B),u1_struct_0(A)) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d1_funct_2,t36_funct_5,t1_xboole_1,t4_funct_2,t39_funct_5,t1_xboole_1,t4_funct_2]), [file(bilinear,l18_bilinear),interesting(0.00)]). fof(d3_bilinear,definition,( ! [A] : ( ( ~ v3_struct_0(A) & l1_rlvect_1(A) ) => ! [B] : ( ( ~ v3_struct_0(B) & l4_vectsp_1(B,A) ) => ! [C] : ( ( ~ v3_struct_0(C) & l4_vectsp_1(C,A) ) => ! [D] : ( ( v1_funct_1(D) & v1_funct_2(D,k2_zfmisc_1(u1_struct_0(B),u1_struct_0(C)),u1_struct_0(A)) & m2_relset_1(D,k2_zfmisc_1(u1_struct_0(B),u1_struct_0(C)),u1_struct_0(A)) ) => ! [E] : ( ( v1_funct_1(E) & v1_funct_2(E,k2_zfmisc_1(u1_struct_0(B),u1_struct_0(C)),u1_struct_0(A)) & m2_relset_1(E,k2_zfmisc_1(u1_struct_0(B),u1_struct_0(C)),u1_struct_0(A)) ) => ! [F] : ( ( v1_funct_1(F) & v1_funct_2(F,k2_zfmisc_1(u1_struct_0(B),u1_struct_0(C)),u1_struct_0(A)) & m2_relset_1(F,k2_zfmisc_1(u1_struct_0(B),u1_struct_0(C)),u1_struct_0(A)) ) => ( F = k2_bilinear(A,B,C,D,E) <=> ! [G] : ( m1_subset_1(G,u1_struct_0(B)) => ! [H] : ( m1_subset_1(H,u1_struct_0(C)) => k8_funct_2(k2_zfmisc_1(u1_struct_0(B),u1_struct_0(C)),u1_struct_0(A),F,k1_domain_1(u1_struct_0(B),u1_struct_0(C),G,H)) = k2_rlvect_1(A,k8_funct_2(k2_zfmisc_1(u1_struct_0(B),u1_struct_0(C)),u1_struct_0(A),D,k1_domain_1(u1_struct_0(B),u1_struct_0(C),G,H)),k8_funct_2(k2_zfmisc_1(u1_struct_0(B),u1_struct_0(C)),u1_struct_0(A),E,k1_domain_1(u1_struct_0(B),u1_struct_0(C),G,H))) ) ) ) ) ) ) ) ) ) ), file(bilinear,d3_bilinear), [interesting(0.00)]). fof(t120_funct_2,theorem,( ! [A,B,C,D] : ( ( v1_funct_1(D) & v1_funct_2(D,k2_zfmisc_1(A,B),C) & m2_relset_1(D,k2_zfmisc_1(A,B),C) ) => ! [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] : ( m1_subset_1(F,A) => ! [G] : ( m1_subset_1(G,B) => k1_funct_1(D,k4_tarski(F,G)) = k1_funct_1(E,k4_tarski(F,G)) ) ) => D = E ) ) ) ), file(funct_2,t120_funct_2), [interesting(0.00)]). fof(l9_bilinear,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_rlvect_1(A) & l1_rlvect_1(A) ) => ! [B] : ( ( ~ v3_struct_0(B) & l4_vectsp_1(B,A) ) => ! [C] : ( ( ~ v3_struct_0(C) & l4_vectsp_1(C,A) ) => ! [D] : ( ( v1_funct_1(D) & v1_funct_2(D,k2_zfmisc_1(u1_struct_0(B),u1_struct_0(C)),u1_struct_0(A)) & m2_relset_1(D,k2_zfmisc_1(u1_struct_0(B),u1_struct_0(C)),u1_struct_0(A)) ) => ! [E] : ( ( v1_funct_1(E) & v1_funct_2(E,k2_zfmisc_1(u1_struct_0(B),u1_struct_0(C)),u1_struct_0(A)) & m2_relset_1(E,k2_zfmisc_1(u1_struct_0(B),u1_struct_0(C)),u1_struct_0(A)) ) => k2_bilinear(A,B,C,D,E) = k2_bilinear(A,B,C,E,D) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d3_bilinear,d3_bilinear,t120_funct_2]), [file(bilinear,l9_bilinear),interesting(0.00)]). fof(t9_bilinear,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & l1_struct_0(A) ) => ! [B] : ( ( ~ v3_struct_0(B) & l4_vectsp_1(B,A) ) => ! [C] : ( ( ~ v3_struct_0(C) & l4_vectsp_1(C,A) ) => ! [D] : ( ( v1_funct_1(D) & v1_funct_2(D,k2_zfmisc_1(u1_struct_0(B),u1_struct_0(C)),u1_struct_0(A)) & m2_relset_1(D,k2_zfmisc_1(u1_struct_0(B),u1_struct_0(C)),u1_struct_0(A)) ) => ! [E] : ( m1_subset_1(E,u1_struct_0(B)) => ( k4_relset_1(u1_struct_0(C),u1_struct_0(A),k9_bilinear(A,B,C,D,E)) = u1_struct_0(C) & r1_tarski(k5_relset_1(u1_struct_0(C),u1_struct_0(A),k9_bilinear(A,B,C,D,E)),u1_struct_0(A)) & ! [F] : ( m1_subset_1(F,u1_struct_0(C)) => k8_funct_2(u1_struct_0(C),u1_struct_0(A),k9_bilinear(A,B,C,D,E),F) = k8_funct_2(k2_zfmisc_1(u1_struct_0(B),u1_struct_0(C)),u1_struct_0(A),D,k1_domain_1(u1_struct_0(B),u1_struct_0(C),E,F)) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d1_funct_2,t36_funct_5]), [file(bilinear,t9_bilinear),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(t1_bilinear,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & l2_struct_0(A) ) => ! [B] : ( ( ~ v3_struct_0(B) & l4_vectsp_1(B,A) ) => ! [C] : ( ( ~ v3_struct_0(C) & l4_vectsp_1(C,A) ) => ! [D] : ( m1_subset_1(D,u1_struct_0(B)) => ! [E] : ( m1_subset_1(E,u1_struct_0(C)) => k8_funct_2(k2_zfmisc_1(u1_struct_0(B),u1_struct_0(C)),u1_struct_0(A),k1_bilinear(A,B,C),k1_domain_1(u1_struct_0(B),u1_struct_0(C),D,E)) = k1_rlvect_1(A) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t13_funcop_1]), [file(bilinear,t1_bilinear),interesting(0.00)]). fof(t22_hahnban1,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & l2_struct_0(A) ) => ! [B] : ( ( ~ v3_struct_0(B) & l4_vectsp_1(B,A) ) => ! [C] : ( m1_subset_1(C,u1_struct_0(B)) => k8_funct_2(u1_struct_0(B),u1_struct_0(A),k7_hahnban1(A,B),C) = k1_rlvect_1(A) ) ) ) ), file(hahnban1,t22_hahnban1), [interesting(0.00)]). fof(t113_funct_2,theorem,( ! [A,B,C] : ( ( v1_funct_1(C) & v1_funct_2(C,A,B) & m2_relset_1(C,A,B) ) => ! [D] : ( ( v1_funct_1(D) & v1_funct_2(D,A,B) & m2_relset_1(D,A,B) ) => ( ! [E] : ( m1_subset_1(E,A) => k1_funct_1(C,E) = k1_funct_1(D,E) ) => C = D ) ) ) ), file(funct_2,t113_funct_2), [interesting(0.00)]). fof(t10_bilinear,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & l1_struct_0(A) ) => ! [B] : ( ( ~ v3_struct_0(B) & l4_vectsp_1(B,A) ) => ! [C] : ( ( ~ v3_struct_0(C) & l4_vectsp_1(C,A) ) => ! [D] : ( ( v1_funct_1(D) & v1_funct_2(D,k2_zfmisc_1(u1_struct_0(B),u1_struct_0(C)),u1_struct_0(A)) & m2_relset_1(D,k2_zfmisc_1(u1_struct_0(B),u1_struct_0(C)),u1_struct_0(A)) ) => ! [E] : ( m1_subset_1(E,u1_struct_0(C)) => ( k4_relset_1(u1_struct_0(B),u1_struct_0(A),k10_bilinear(A,B,C,D,E)) = u1_struct_0(B) & r1_tarski(k5_relset_1(u1_struct_0(B),u1_struct_0(A),k10_bilinear(A,B,C,D,E)),u1_struct_0(A)) & ! [F] : ( m1_subset_1(F,u1_struct_0(B)) => k8_funct_2(u1_struct_0(B),u1_struct_0(A),k10_bilinear(A,B,C,D,E),F) = k8_funct_2(k2_zfmisc_1(u1_struct_0(B),u1_struct_0(C)),u1_struct_0(A),D,k1_domain_1(u1_struct_0(B),u1_struct_0(C),F,E)) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d1_funct_2,t39_funct_5]), [file(bilinear,t10_bilinear),interesting(0.00)]). fof(d6_hahnban1,definition,( ! [A] : ( ( ~ v3_struct_0(A) & l1_rlvect_1(A) ) => ! [B] : ( ( ~ v3_struct_0(B) & l4_vectsp_1(B,A) ) => ! [C] : ( ( v1_funct_1(C) & v1_funct_2(C,u1_struct_0(B),u1_struct_0(A)) & m2_relset_1(C,u1_struct_0(B),u1_struct_0(A)) ) => ! [D] : ( ( v1_funct_1(D) & v1_funct_2(D,u1_struct_0(B),u1_struct_0(A)) & m2_relset_1(D,u1_struct_0(B),u1_struct_0(A)) ) => ! [E] : ( ( v1_funct_1(E) & v1_funct_2(E,u1_struct_0(B),u1_struct_0(A)) & m2_relset_1(E,u1_struct_0(B),u1_struct_0(A)) ) => ( E = k3_hahnban1(A,B,C,D) <=> ! [F] : ( m1_subset_1(F,u1_struct_0(B)) => k8_funct_2(u1_struct_0(B),u1_struct_0(A),E,F) = k2_rlvect_1(A,k8_funct_2(u1_struct_0(B),u1_struct_0(A),C,F),k8_funct_2(u1_struct_0(B),u1_struct_0(A),D,F)) ) ) ) ) ) ) ) ), file(hahnban1,d6_hahnban1), [interesting(0.00)]). fof(t13_bilinear,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & l1_rlvect_1(A) ) => ! [B] : ( ( ~ v3_struct_0(B) & l4_vectsp_1(B,A) ) => ! [C] : ( ( ~ v3_struct_0(C) & l4_vectsp_1(C,A) ) => ! [D] : ( ( v1_funct_1(D) & v1_funct_2(D,k2_zfmisc_1(u1_struct_0(B),u1_struct_0(C)),u1_struct_0(A)) & m2_relset_1(D,k2_zfmisc_1(u1_struct_0(B),u1_struct_0(C)),u1_struct_0(A)) ) => ! [E] : ( ( v1_funct_1(E) & v1_funct_2(E,k2_zfmisc_1(u1_struct_0(B),u1_struct_0(C)),u1_struct_0(A)) & m2_relset_1(E,k2_zfmisc_1(u1_struct_0(B),u1_struct_0(C)),u1_struct_0(A)) ) => ! [F] : ( m1_subset_1(F,u1_struct_0(C)) => k10_bilinear(A,B,C,k2_bilinear(A,B,C,D,E),F) = k3_hahnban1(A,B,k10_bilinear(A,B,C,D,F),k10_bilinear(A,B,C,E,F)) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t10_bilinear,d3_bilinear,t10_bilinear,t10_bilinear,d6_hahnban1,t113_funct_2]), [file(bilinear,t13_bilinear),interesting(0.00)]). fof(t14_bilinear,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & l1_rlvect_1(A) ) => ! [B] : ( ( ~ v3_struct_0(B) & l4_vectsp_1(B,A) ) => ! [C] : ( ( ~ v3_struct_0(C) & l4_vectsp_1(C,A) ) => ! [D] : ( ( v1_funct_1(D) & v1_funct_2(D,k2_zfmisc_1(u1_struct_0(B),u1_struct_0(C)),u1_struct_0(A)) & m2_relset_1(D,k2_zfmisc_1(u1_struct_0(B),u1_struct_0(C)),u1_struct_0(A)) ) => ! [E] : ( ( v1_funct_1(E) & v1_funct_2(E,k2_zfmisc_1(u1_struct_0(B),u1_struct_0(C)),u1_struct_0(A)) & m2_relset_1(E,k2_zfmisc_1(u1_struct_0(B),u1_struct_0(C)),u1_struct_0(A)) ) => ! [F] : ( m1_subset_1(F,u1_struct_0(B)) => k9_bilinear(A,B,C,k2_bilinear(A,B,C,D,E),F) = k3_hahnban1(A,C,k9_bilinear(A,B,C,D,F),k9_bilinear(A,B,C,E,F)) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t9_bilinear,d3_bilinear,t9_bilinear,t9_bilinear,d6_hahnban1,t113_funct_2]), [file(bilinear,t14_bilinear),interesting(0.00)]). fof(d4_bilinear,definition,( ! [A] : ( ( ~ v3_struct_0(A) & l1_group_1(A) ) => ! [B] : ( ( ~ v3_struct_0(B) & l4_vectsp_1(B,A) ) => ! [C] : ( ( ~ v3_struct_0(C) & l4_vectsp_1(C,A) ) => ! [D] : ( ( v1_funct_1(D) & v1_funct_2(D,k2_zfmisc_1(u1_struct_0(B),u1_struct_0(C)),u1_struct_0(A)) & m2_relset_1(D,k2_zfmisc_1(u1_struct_0(B),u1_struct_0(C)),u1_struct_0(A)) ) => ! [E] : ( m1_subset_1(E,u1_struct_0(A)) => ! [F] : ( ( v1_funct_1(F) & v1_funct_2(F,k2_zfmisc_1(u1_struct_0(B),u1_struct_0(C)),u1_struct_0(A)) & m2_relset_1(F,k2_zfmisc_1(u1_struct_0(B),u1_struct_0(C)),u1_struct_0(A)) ) => ( F = k3_bilinear(A,B,C,D,E) <=> ! [G] : ( m1_subset_1(G,u1_struct_0(B)) => ! [H] : ( m1_subset_1(H,u1_struct_0(C)) => k8_funct_2(k2_zfmisc_1(u1_struct_0(B),u1_struct_0(C)),u1_struct_0(A),F,k1_domain_1(u1_struct_0(B),u1_struct_0(C),G,H)) = k1_group_1(A,E,k8_funct_2(k2_zfmisc_1(u1_struct_0(B),u1_struct_0(C)),u1_struct_0(A),D,k1_domain_1(u1_struct_0(B),u1_struct_0(C),G,H))) ) ) ) ) ) ) ) ) ) ), file(bilinear,d4_bilinear), [interesting(0.00)]). fof(d9_hahnban1,definition,( ! [A] : ( ( ~ v3_struct_0(A) & l1_group_1(A) ) => ! [B] : ( ( ~ v3_struct_0(B) & l4_vectsp_1(B,A) ) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( ( v1_funct_1(D) & v1_funct_2(D,u1_struct_0(B),u1_struct_0(A)) & m2_relset_1(D,u1_struct_0(B),u1_struct_0(A)) ) => ! [E] : ( ( v1_funct_1(E) & v1_funct_2(E,u1_struct_0(B),u1_struct_0(A)) & m2_relset_1(E,u1_struct_0(B),u1_struct_0(A)) ) => ( E = k6_hahnban1(A,B,C,D) <=> ! [F] : ( m1_subset_1(F,u1_struct_0(B)) => k8_funct_2(u1_struct_0(B),u1_struct_0(A),E,F) = k1_group_1(A,C,k8_funct_2(u1_struct_0(B),u1_struct_0(A),D,F)) ) ) ) ) ) ) ) ), file(hahnban1,d9_hahnban1), [interesting(0.00)]). fof(d5_bilinear,definition,( ! [A] : ( ( ~ v3_struct_0(A) & l1_rlvect_1(A) ) => ! [B] : ( ( ~ v3_struct_0(B) & l4_vectsp_1(B,A) ) => ! [C] : ( ( ~ v3_struct_0(C) & l4_vectsp_1(C,A) ) => ! [D] : ( ( v1_funct_1(D) & v1_funct_2(D,k2_zfmisc_1(u1_struct_0(B),u1_struct_0(C)),u1_struct_0(A)) & m2_relset_1(D,k2_zfmisc_1(u1_struct_0(B),u1_struct_0(C)),u1_struct_0(A)) ) => ! [E] : ( ( v1_funct_1(E) & v1_funct_2(E,k2_zfmisc_1(u1_struct_0(B),u1_struct_0(C)),u1_struct_0(A)) & m2_relset_1(E,k2_zfmisc_1(u1_struct_0(B),u1_struct_0(C)),u1_struct_0(A)) ) => ( E = k4_bilinear(A,B,C,D) <=> ! [F] : ( m1_subset_1(F,u1_struct_0(B)) => ! [G] : ( m1_subset_1(G,u1_struct_0(C)) => k8_funct_2(k2_zfmisc_1(u1_struct_0(B),u1_struct_0(C)),u1_struct_0(A),E,k1_domain_1(u1_struct_0(B),u1_struct_0(C),F,G)) = k5_rlvect_1(A,k8_funct_2(k2_zfmisc_1(u1_struct_0(B),u1_struct_0(C)),u1_struct_0(A),D,k1_domain_1(u1_struct_0(B),u1_struct_0(C),F,G))) ) ) ) ) ) ) ) ) ), file(bilinear,d5_bilinear), [interesting(0.00)]). fof(d7_hahnban1,definition,( ! [A] : ( ( ~ v3_struct_0(A) & l1_rlvect_1(A) ) => ! [B] : ( ( ~ v3_struct_0(B) & l4_vectsp_1(B,A) ) => ! [C] : ( ( v1_funct_1(C) & v1_funct_2(C,u1_struct_0(B),u1_struct_0(A)) & m2_relset_1(C,u1_struct_0(B),u1_struct_0(A)) ) => ! [D] : ( ( v1_funct_1(D) & v1_funct_2(D,u1_struct_0(B),u1_struct_0(A)) & m2_relset_1(D,u1_struct_0(B),u1_struct_0(A)) ) => ( D = k4_hahnban1(A,B,C) <=> ! [E] : ( m1_subset_1(E,u1_struct_0(B)) => k8_funct_2(u1_struct_0(B),u1_struct_0(A),D,E) = k5_rlvect_1(A,k8_funct_2(u1_struct_0(B),u1_struct_0(A),C,E)) ) ) ) ) ) ) ), file(hahnban1,d7_hahnban1), [interesting(0.00)]). fof(d8_bilinear,definition,( ! [A] : ( ( ~ v3_struct_0(A) & l1_rlvect_1(A) ) => ! [B] : ( ( ~ v3_struct_0(B) & l4_vectsp_1(B,A) ) => ! [C] : ( ( ~ v3_struct_0(C) & l4_vectsp_1(C,A) ) => ! [D] : ( ( v1_funct_1(D) & v1_funct_2(D,k2_zfmisc_1(u1_struct_0(B),u1_struct_0(C)),u1_struct_0(A)) & m2_relset_1(D,k2_zfmisc_1(u1_struct_0(B),u1_struct_0(C)),u1_struct_0(A)) ) => ! [E] : ( ( v1_funct_1(E) & v1_funct_2(E,k2_zfmisc_1(u1_struct_0(B),u1_struct_0(C)),u1_struct_0(A)) & m2_relset_1(E,k2_zfmisc_1(u1_struct_0(B),u1_struct_0(C)),u1_struct_0(A)) ) => ! [F] : ( ( v1_funct_1(F) & v1_funct_2(F,k2_zfmisc_1(u1_struct_0(B),u1_struct_0(C)),u1_struct_0(A)) & m2_relset_1(F,k2_zfmisc_1(u1_struct_0(B),u1_struct_0(C)),u1_struct_0(A)) ) => ( F = k7_bilinear(A,B,C,D,E) <=> ! [G] : ( m1_subset_1(G,u1_struct_0(B)) => ! [H] : ( m1_subset_1(H,u1_struct_0(C)) => k8_funct_2(k2_zfmisc_1(u1_struct_0(B),u1_struct_0(C)),u1_struct_0(A),F,k1_domain_1(u1_struct_0(B),u1_struct_0(C),G,H)) = k6_rlvect_1(A,k8_funct_2(k2_zfmisc_1(u1_struct_0(B),u1_struct_0(C)),u1_struct_0(A),D,k1_domain_1(u1_struct_0(B),u1_struct_0(C),G,H)),k8_funct_2(k2_zfmisc_1(u1_struct_0(B),u1_struct_0(C)),u1_struct_0(A),E,k1_domain_1(u1_struct_0(B),u1_struct_0(C),G,H))) ) ) ) ) ) ) ) ) ) ), file(bilinear,d8_bilinear), [interesting(0.00)]). fof(d11_rlvect_1,definition,( ! [A] : ( ( ~ v3_struct_0(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) = k2_rlvect_1(A,B,k5_rlvect_1(A,C)) ) ) ) ), file(rlvect_1,d11_rlvect_1), [interesting(0.00)]). fof(t19_bilinear,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & l1_rlvect_1(A) ) => ! [B] : ( ( ~ v3_struct_0(B) & l4_vectsp_1(B,A) ) => ! [C] : ( ( ~ v3_struct_0(C) & l4_vectsp_1(C,A) ) => ! [D] : ( ( v1_funct_1(D) & v1_funct_2(D,k2_zfmisc_1(u1_struct_0(B),u1_struct_0(C)),u1_struct_0(A)) & m2_relset_1(D,k2_zfmisc_1(u1_struct_0(B),u1_struct_0(C)),u1_struct_0(A)) ) => ! [E] : ( ( v1_funct_1(E) & v1_funct_2(E,k2_zfmisc_1(u1_struct_0(B),u1_struct_0(C)),u1_struct_0(A)) & m2_relset_1(E,k2_zfmisc_1(u1_struct_0(B),u1_struct_0(C)),u1_struct_0(A)) ) => ! [F] : ( m1_subset_1(F,u1_struct_0(C)) => k10_bilinear(A,B,C,k7_bilinear(A,B,C,D,E),F) = k5_hahnban1(A,B,k10_bilinear(A,B,C,D,F),k10_bilinear(A,B,C,E,F)) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t10_bilinear,d8_bilinear,t10_bilinear,t10_bilinear,d11_rlvect_1,d7_hahnban1,d6_hahnban1,t113_funct_2]), [file(bilinear,t19_bilinear),interesting(0.00)]). fof(t20_bilinear,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & l1_rlvect_1(A) ) => ! [B] : ( ( ~ v3_struct_0(B) & l4_vectsp_1(B,A) ) => ! [C] : ( ( ~ v3_struct_0(C) & l4_vectsp_1(C,A) ) => ! [D] : ( ( v1_funct_1(D) & v1_funct_2(D,k2_zfmisc_1(u1_struct_0(B),u1_struct_0(C)),u1_struct_0(A)) & m2_relset_1(D,k2_zfmisc_1(u1_struct_0(B),u1_struct_0(C)),u1_struct_0(A)) ) => ! [E] : ( ( v1_funct_1(E) & v1_funct_2(E,k2_zfmisc_1(u1_struct_0(B),u1_struct_0(C)),u1_struct_0(A)) & m2_relset_1(E,k2_zfmisc_1(u1_struct_0(B),u1_struct_0(C)),u1_struct_0(A)) ) => ! [F] : ( m1_subset_1(F,u1_struct_0(B)) => k9_bilinear(A,B,C,k7_bilinear(A,B,C,D,E),F) = k5_hahnban1(A,C,k9_bilinear(A,B,C,D,F),k9_bilinear(A,B,C,E,F)) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t9_bilinear,d8_bilinear,t9_bilinear,t9_bilinear,d11_rlvect_1,d7_hahnban1,d6_hahnban1,t113_funct_2]), [file(bilinear,t20_bilinear),interesting(0.00)]). fof(t12_pre_topc,theorem,( ! [A] : ( l1_struct_0(A) => k2_pre_topc(A) = u1_struct_0(A) ) ), file(pre_topc,t12_pre_topc), [interesting(0.00)]). fof(d11_bilinear,definition,( ! [A] : ( ( ~ v3_struct_0(A) & l1_group_1(A) ) => ! [B] : ( ( ~ v3_struct_0(B) & l4_vectsp_1(B,A) ) => ! [C] : ( ( ~ v3_struct_0(C) & l4_vectsp_1(C,A) ) => ! [D] : ( ( v1_funct_1(D) & v1_funct_2(D,u1_struct_0(B),u1_struct_0(A)) & m2_relset_1(D,u1_struct_0(B),u1_struct_0(A)) ) => ! [E] : ( ( v1_funct_1(E) & v1_funct_2(E,u1_struct_0(C),u1_struct_0(A)) & m2_relset_1(E,u1_struct_0(C),u1_struct_0(A)) ) => ! [F] : ( ( v1_funct_1(F) & v1_funct_2(F,k2_zfmisc_1(u1_struct_0(B),u1_struct_0(C)),u1_struct_0(A)) & m2_relset_1(F,k2_zfmisc_1(u1_struct_0(B),u1_struct_0(C)),u1_struct_0(A)) ) => ( F = k11_bilinear(A,B,C,D,E) <=> ! [G] : ( m1_subset_1(G,u1_struct_0(B)) => ! [H] : ( m1_subset_1(H,u1_struct_0(C)) => k8_funct_2(k2_zfmisc_1(u1_struct_0(B),u1_struct_0(C)),u1_struct_0(A),F,k1_domain_1(u1_struct_0(B),u1_struct_0(C),G,H)) = k1_group_1(A,k8_funct_2(u1_struct_0(B),u1_struct_0(A),D,G),k8_funct_2(u1_struct_0(C),u1_struct_0(A),E,H)) ) ) ) ) ) ) ) ) ) ), file(bilinear,d11_bilinear), [interesting(0.00)]). fof(t36_vectsp_1,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & v4_vectsp_1(A) & l3_vectsp_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => k1_group_1(A,B,k1_rlvect_1(A)) = k1_rlvect_1(A) ) ) ), file(vectsp_1,t36_vectsp_1), [interesting(0.00)]). fof(t23_bilinear,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & v4_vectsp_1(A) & l3_vectsp_1(A) ) => ! [B] : ( ( ~ v3_struct_0(B) & l4_vectsp_1(B,A) ) => ! [C] : ( ( ~ v3_struct_0(C) & l4_vectsp_1(C,A) ) => ! [D] : ( ( v1_funct_1(D) & v1_funct_2(D,u1_struct_0(B),u1_struct_0(A)) & m2_relset_1(D,u1_struct_0(B),u1_struct_0(A)) ) => k11_bilinear(A,B,C,D,k7_hahnban1(A,C)) = k1_bilinear(A,B,C) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t21_bilinear,t1_bilinear,t120_funct_2]), [file(bilinear,t23_bilinear),interesting(0.00)]). fof(t39_vectsp_1,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & v5_vectsp_1(A) & l3_vectsp_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => k1_group_1(A,k1_rlvect_1(A),B) = k1_rlvect_1(A) ) ) ), file(vectsp_1,t39_vectsp_1), [interesting(0.00)]). fof(t24_bilinear,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & v5_vectsp_1(A) & l3_vectsp_1(A) ) => ! [B] : ( ( ~ v3_struct_0(B) & l4_vectsp_1(B,A) ) => ! [C] : ( ( ~ v3_struct_0(C) & l4_vectsp_1(C,A) ) => ! [D] : ( ( v1_funct_1(D) & v1_funct_2(D,u1_struct_0(C),u1_struct_0(A)) & m2_relset_1(D,u1_struct_0(C),u1_struct_0(A)) ) => k11_bilinear(A,B,C,k7_hahnban1(A,B),D) = k1_bilinear(A,B,C) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t22_bilinear,t1_bilinear,t120_funct_2]), [file(bilinear,t24_bilinear),interesting(0.00)]). fof(t25_bilinear,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & l1_group_1(A) ) => ! [B] : ( ( ~ v3_struct_0(B) & l4_vectsp_1(B,A) ) => ! [C] : ( ( ~ v3_struct_0(C) & l4_vectsp_1(C,A) ) => ! [D] : ( ( v1_funct_1(D) & v1_funct_2(D,u1_struct_0(B),u1_struct_0(A)) & m2_relset_1(D,u1_struct_0(B),u1_struct_0(A)) ) => ! [E] : ( ( v1_funct_1(E) & v1_funct_2(E,u1_struct_0(C),u1_struct_0(A)) & m2_relset_1(E,u1_struct_0(C),u1_struct_0(A)) ) => ! [F] : ( m1_subset_1(F,u1_struct_0(B)) => k9_bilinear(A,B,C,k11_bilinear(A,B,C,D,E),F) = k6_hahnban1(A,C,k8_funct_2(u1_struct_0(B),u1_struct_0(A),D,F),E) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t9_bilinear,d11_bilinear,d9_hahnban1,t113_funct_2]), [file(bilinear,t25_bilinear),interesting(0.00)]). fof(t26_bilinear,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v7_group_1(A) & l1_group_1(A) ) => ! [B] : ( ( ~ v3_struct_0(B) & l4_vectsp_1(B,A) ) => ! [C] : ( ( ~ v3_struct_0(C) & l4_vectsp_1(C,A) ) => ! [D] : ( ( v1_funct_1(D) & v1_funct_2(D,u1_struct_0(B),u1_struct_0(A)) & m2_relset_1(D,u1_struct_0(B),u1_struct_0(A)) ) => ! [E] : ( ( v1_funct_1(E) & v1_funct_2(E,u1_struct_0(C),u1_struct_0(A)) & m2_relset_1(E,u1_struct_0(C),u1_struct_0(A)) ) => ! [F] : ( m1_subset_1(F,u1_struct_0(C)) => k10_bilinear(A,B,C,k11_bilinear(A,B,C,D,E),F) = k6_hahnban1(A,B,k8_funct_2(u1_struct_0(C),u1_struct_0(A),E,F),D) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t10_bilinear,d11_bilinear,d9_hahnban1,t113_funct_2]), [file(bilinear,t26_bilinear),interesting(0.00)]). fof(d7_rlvect_1,definition,( ! [A] : ( ( ~ v3_struct_0(A) & l1_rlvect_1(A) ) => ( v5_rlvect_1(A) <=> ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => k2_rlvect_1(A,B,k1_rlvect_1(A)) = B ) ) ) ), file(rlvect_1,d7_rlvect_1), [interesting(0.00)]). fof(t2_vectsp10,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & v4_group_1(A) & v7_vectsp_1(A) & v8_vectsp_1(A) & l3_vectsp_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( ( ~ v3_struct_0(C) & v4_rlvect_1(C) & v5_rlvect_1(C) & v6_rlvect_1(C) & v12_vectsp_1(C,A) & l4_vectsp_1(C,A) ) => ! [D] : ( m1_subset_1(D,u1_struct_0(C)) => ( k6_vectsp_1(A,C,k1_rlvect_1(A),D) = k1_rlvect_1(C) & k6_vectsp_1(A,C,B,k1_rlvect_1(C)) = k1_rlvect_1(C) ) ) ) ) ) ), file(vectsp10,t2_vectsp10), [interesting(0.00)]). fof(d15_bilinear,definition,( ! [A] : ( ( ~ v3_struct_0(A) & l1_group_1(A) ) => ! [B] : ( ( ~ v3_struct_0(B) & l4_vectsp_1(B,A) ) => ! [C] : ( ( ~ v3_struct_0(C) & l4_vectsp_1(C,A) ) => ! [D] : ( ( v1_funct_1(D) & v1_funct_2(D,k2_zfmisc_1(u1_struct_0(B),u1_struct_0(C)),u1_struct_0(A)) & m2_relset_1(D,k2_zfmisc_1(u1_struct_0(B),u1_struct_0(C)),u1_struct_0(A)) ) => ( v4_bilinear(D,A,B,C) <=> ! [E] : ( m1_subset_1(E,u1_struct_0(C)) => v2_hahnban1(k10_bilinear(A,B,C,D,E),A,B) ) ) ) ) ) ) ), file(bilinear,d15_bilinear), [interesting(0.00)]). fof(d12_hahnban1,definition,( ! [A] : ( ( ~ v3_struct_0(A) & l1_group_1(A) ) => ! [B] : ( ( ~ v3_struct_0(B) & l4_vectsp_1(B,A) ) => ! [C] : ( ( v1_funct_1(C) & v1_funct_2(C,u1_struct_0(B),u1_struct_0(A)) & m2_relset_1(C,u1_struct_0(B),u1_struct_0(A)) ) => ( v2_hahnban1(C,A,B) <=> ! [D] : ( m1_subset_1(D,u1_struct_0(B)) => ! [E] : ( m1_subset_1(E,u1_struct_0(A)) => k8_funct_2(u1_struct_0(B),u1_struct_0(A),C,k6_vectsp_1(A,B,E,D)) = k1_group_1(A,E,k8_funct_2(u1_struct_0(B),u1_struct_0(A),C,D)) ) ) ) ) ) ) ), file(hahnban1,d12_hahnban1), [interesting(0.00)]). fof(t32_bilinear,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & l1_group_1(A) ) => ! [B] : ( ( ~ v3_struct_0(B) & l4_vectsp_1(B,A) ) => ! [C] : ( ( ~ v3_struct_0(C) & l4_vectsp_1(C,A) ) => ! [D] : ( m1_subset_1(D,u1_struct_0(B)) => ! [E] : ( m1_subset_1(E,u1_struct_0(C)) => ! [F] : ( m1_subset_1(F,u1_struct_0(A)) => ! [G] : ( ( v1_funct_1(G) & v1_funct_2(G,k2_zfmisc_1(u1_struct_0(B),u1_struct_0(C)),u1_struct_0(A)) & m2_relset_1(G,k2_zfmisc_1(u1_struct_0(B),u1_struct_0(C)),u1_struct_0(A)) ) => ( v4_bilinear(G,A,B,C) => k8_funct_2(k2_zfmisc_1(u1_struct_0(B),u1_struct_0(C)),u1_struct_0(A),G,k1_domain_1(u1_struct_0(B),u1_struct_0(C),k6_vectsp_1(A,B,F,D),E)) = k1_group_1(A,F,k8_funct_2(k2_zfmisc_1(u1_struct_0(B),u1_struct_0(C)),u1_struct_0(A),G,k1_domain_1(u1_struct_0(B),u1_struct_0(C),D,E))) ) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d15_bilinear,t10_bilinear,d12_hahnban1,t10_bilinear]), [file(bilinear,t32_bilinear),interesting(0.00)]). fof(d14_bilinear,definition,( ! [A] : ( ( ~ v3_struct_0(A) & l1_group_1(A) ) => ! [B] : ( ( ~ v3_struct_0(B) & l4_vectsp_1(B,A) ) => ! [C] : ( ( ~ v3_struct_0(C) & l4_vectsp_1(C,A) ) => ! [D] : ( ( v1_funct_1(D) & v1_funct_2(D,k2_zfmisc_1(u1_struct_0(B),u1_struct_0(C)),u1_struct_0(A)) & m2_relset_1(D,k2_zfmisc_1(u1_struct_0(B),u1_struct_0(C)),u1_struct_0(A)) ) => ( v3_bilinear(D,A,B,C) <=> ! [E] : ( m1_subset_1(E,u1_struct_0(B)) => v2_hahnban1(k9_bilinear(A,B,C,D,E),A,C) ) ) ) ) ) ) ), file(bilinear,d14_bilinear), [interesting(0.00)]). fof(t33_bilinear,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & l1_group_1(A) ) => ! [B] : ( ( ~ v3_struct_0(B) & l4_vectsp_1(B,A) ) => ! [C] : ( ( ~ v3_struct_0(C) & l4_vectsp_1(C,A) ) => ! [D] : ( m1_subset_1(D,u1_struct_0(B)) => ! [E] : ( m1_subset_1(E,u1_struct_0(C)) => ! [F] : ( m1_subset_1(F,u1_struct_0(A)) => ! [G] : ( ( v1_funct_1(G) & v1_funct_2(G,k2_zfmisc_1(u1_struct_0(B),u1_struct_0(C)),u1_struct_0(A)) & m2_relset_1(G,k2_zfmisc_1(u1_struct_0(B),u1_struct_0(C)),u1_struct_0(A)) ) => ( v3_bilinear(G,A,B,C) => k8_funct_2(k2_zfmisc_1(u1_struct_0(B),u1_struct_0(C)),u1_struct_0(A),G,k1_domain_1(u1_struct_0(B),u1_struct_0(C),D,k6_vectsp_1(A,C,F,E))) = k1_group_1(A,F,k8_funct_2(k2_zfmisc_1(u1_struct_0(B),u1_struct_0(C)),u1_struct_0(A),G,k1_domain_1(u1_struct_0(B),u1_struct_0(C),D,E))) ) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d14_bilinear,t9_bilinear,d12_hahnban1,t9_bilinear]), [file(bilinear,t33_bilinear),interesting(0.00)]). fof(d13_bilinear,definition,( ! [A] : ( ( ~ v3_struct_0(A) & l1_rlvect_1(A) ) => ! [B] : ( ( ~ v3_struct_0(B) & l4_vectsp_1(B,A) ) => ! [C] : ( ( ~ v3_struct_0(C) & l4_vectsp_1(C,A) ) => ! [D] : ( ( v1_funct_1(D) & v1_funct_2(D,k2_zfmisc_1(u1_struct_0(B),u1_struct_0(C)),u1_struct_0(A)) & m2_relset_1(D,k2_zfmisc_1(u1_struct_0(B),u1_struct_0(C)),u1_struct_0(A)) ) => ( v2_bilinear(D,A,B,C) <=> ! [E] : ( m1_subset_1(E,u1_struct_0(C)) => v1_hahnban1(k10_bilinear(A,B,C,D,E),A,B) ) ) ) ) ) ) ), file(bilinear,d13_bilinear), [interesting(0.00)]). fof(d11_hahnban1,definition,( ! [A] : ( ( ~ v3_struct_0(A) & l1_rlvect_1(A) ) => ! [B] : ( ( ~ v3_struct_0(B) & l4_vectsp_1(B,A) ) => ! [C] : ( ( v1_funct_1(C) & v1_funct_2(C,u1_struct_0(B),u1_struct_0(A)) & m2_relset_1(C,u1_struct_0(B),u1_struct_0(A)) ) => ( v1_hahnban1(C,A,B) <=> ! [D] : ( m1_subset_1(D,u1_struct_0(B)) => ! [E] : ( m1_subset_1(E,u1_struct_0(B)) => k8_funct_2(u1_struct_0(B),u1_struct_0(A),C,k2_rlvect_1(B,D,E)) = k2_rlvect_1(A,k8_funct_2(u1_struct_0(B),u1_struct_0(A),C,D),k8_funct_2(u1_struct_0(B),u1_struct_0(A),C,E)) ) ) ) ) ) ) ), file(hahnban1,d11_hahnban1), [interesting(0.00)]). fof(t27_bilinear,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & l1_rlvect_1(A) ) => ! [B] : ( ( ~ v3_struct_0(B) & l4_vectsp_1(B,A) ) => ! [C] : ( ( ~ v3_struct_0(C) & l4_vectsp_1(C,A) ) => ! [D] : ( m1_subset_1(D,u1_struct_0(B)) => ! [E] : ( m1_subset_1(E,u1_struct_0(B)) => ! [F] : ( m1_subset_1(F,u1_struct_0(C)) => ! [G] : ( ( v1_funct_1(G) & v1_funct_2(G,k2_zfmisc_1(u1_struct_0(B),u1_struct_0(C)),u1_struct_0(A)) & m2_relset_1(G,k2_zfmisc_1(u1_struct_0(B),u1_struct_0(C)),u1_struct_0(A)) ) => ( v2_bilinear(G,A,B,C) => k8_funct_2(k2_zfmisc_1(u1_struct_0(B),u1_struct_0(C)),u1_struct_0(A),G,k1_domain_1(u1_struct_0(B),u1_struct_0(C),k2_rlvect_1(B,D,E),F)) = k2_rlvect_1(A,k8_funct_2(k2_zfmisc_1(u1_struct_0(B),u1_struct_0(C)),u1_struct_0(A),G,k1_domain_1(u1_struct_0(B),u1_struct_0(C),D,F)),k8_funct_2(k2_zfmisc_1(u1_struct_0(B),u1_struct_0(C)),u1_struct_0(A),G,k1_domain_1(u1_struct_0(B),u1_struct_0(C),E,F))) ) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d13_bilinear,t10_bilinear,d11_hahnban1,t10_bilinear,t10_bilinear]), [file(bilinear,t27_bilinear),interesting(0.00)]). fof(d12_bilinear,definition,( ! [A] : ( ( ~ v3_struct_0(A) & l1_rlvect_1(A) ) => ! [B] : ( ( ~ v3_struct_0(B) & l4_vectsp_1(B,A) ) => ! [C] : ( ( ~ v3_struct_0(C) & l4_vectsp_1(C,A) ) => ! [D] : ( ( v1_funct_1(D) & v1_funct_2(D,k2_zfmisc_1(u1_struct_0(B),u1_struct_0(C)),u1_struct_0(A)) & m2_relset_1(D,k2_zfmisc_1(u1_struct_0(B),u1_struct_0(C)),u1_struct_0(A)) ) => ( v1_bilinear(D,A,B,C) <=> ! [E] : ( m1_subset_1(E,u1_struct_0(B)) => v1_hahnban1(k9_bilinear(A,B,C,D,E),A,C) ) ) ) ) ) ) ), file(bilinear,d12_bilinear), [interesting(0.00)]). fof(t28_bilinear,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & l1_rlvect_1(A) ) => ! [B] : ( ( ~ v3_struct_0(B) & l4_vectsp_1(B,A) ) => ! [C] : ( ( ~ v3_struct_0(C) & l4_vectsp_1(C,A) ) => ! [D] : ( m1_subset_1(D,u1_struct_0(B)) => ! [E] : ( m1_subset_1(E,u1_struct_0(C)) => ! [F] : ( m1_subset_1(F,u1_struct_0(C)) => ! [G] : ( ( v1_funct_1(G) & v1_funct_2(G,k2_zfmisc_1(u1_struct_0(B),u1_struct_0(C)),u1_struct_0(A)) & m2_relset_1(G,k2_zfmisc_1(u1_struct_0(B),u1_struct_0(C)),u1_struct_0(A)) ) => ( v1_bilinear(G,A,B,C) => k8_funct_2(k2_zfmisc_1(u1_struct_0(B),u1_struct_0(C)),u1_struct_0(A),G,k1_domain_1(u1_struct_0(B),u1_struct_0(C),D,k2_rlvect_1(C,E,F))) = k2_rlvect_1(A,k8_funct_2(k2_zfmisc_1(u1_struct_0(B),u1_struct_0(C)),u1_struct_0(A),G,k1_domain_1(u1_struct_0(B),u1_struct_0(C),D,E)),k8_funct_2(k2_zfmisc_1(u1_struct_0(B),u1_struct_0(C)),u1_struct_0(A),G,k1_domain_1(u1_struct_0(B),u1_struct_0(C),D,F))) ) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d12_bilinear,t9_bilinear,d11_hahnban1,t9_bilinear,t9_bilinear]), [file(bilinear,t28_bilinear),interesting(0.00)]). fof(t29_bilinear,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v5_rlvect_1(A) & l1_rlvect_1(A) ) => ! [B] : ( ( ~ v3_struct_0(B) & l4_vectsp_1(B,A) ) => ! [C] : ( ( ~ v3_struct_0(C) & l4_vectsp_1(C,A) ) => ! [D] : ( m1_subset_1(D,u1_struct_0(B)) => ! [E] : ( m1_subset_1(E,u1_struct_0(B)) => ! [F] : ( m1_subset_1(F,u1_struct_0(C)) => ! [G] : ( m1_subset_1(G,u1_struct_0(C)) => ! [H] : ( ( v1_funct_1(H) & v1_funct_2(H,k2_zfmisc_1(u1_struct_0(B),u1_struct_0(C)),u1_struct_0(A)) & v1_bilinear(H,A,B,C) & v2_bilinear(H,A,B,C) & m2_relset_1(H,k2_zfmisc_1(u1_struct_0(B),u1_struct_0(C)),u1_struct_0(A)) ) => k8_funct_2(k2_zfmisc_1(u1_struct_0(B),u1_struct_0(C)),u1_struct_0(A),H,k1_domain_1(u1_struct_0(B),u1_struct_0(C),k2_rlvect_1(B,D,E),k2_rlvect_1(C,F,G))) = k2_rlvect_1(A,k2_rlvect_1(A,k8_funct_2(k2_zfmisc_1(u1_struct_0(B),u1_struct_0(C)),u1_struct_0(A),H,k1_domain_1(u1_struct_0(B),u1_struct_0(C),D,F)),k8_funct_2(k2_zfmisc_1(u1_struct_0(B),u1_struct_0(C)),u1_struct_0(A),H,k1_domain_1(u1_struct_0(B),u1_struct_0(C),D,G))),k2_rlvect_1(A,k8_funct_2(k2_zfmisc_1(u1_struct_0(B),u1_struct_0(C)),u1_struct_0(A),H,k1_domain_1(u1_struct_0(B),u1_struct_0(C),E,F)),k8_funct_2(k2_zfmisc_1(u1_struct_0(B),u1_struct_0(C)),u1_struct_0(A),H,k1_domain_1(u1_struct_0(B),u1_struct_0(C),E,G)))) ) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t27_bilinear,t28_bilinear,t28_bilinear]), [file(bilinear,t29_bilinear),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(t3_bilinear,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v4_rlvect_1(A) & l1_rlvect_1(A) ) => ! [B] : ( ( ~ v3_struct_0(B) & l4_vectsp_1(B,A) ) => ! [C] : ( ( ~ v3_struct_0(C) & l4_vectsp_1(C,A) ) => ! [D] : ( ( v1_funct_1(D) & v1_funct_2(D,k2_zfmisc_1(u1_struct_0(B),u1_struct_0(C)),u1_struct_0(A)) & m2_relset_1(D,k2_zfmisc_1(u1_struct_0(B),u1_struct_0(C)),u1_struct_0(A)) ) => ! [E] : ( ( v1_funct_1(E) & v1_funct_2(E,k2_zfmisc_1(u1_struct_0(B),u1_struct_0(C)),u1_struct_0(A)) & m2_relset_1(E,k2_zfmisc_1(u1_struct_0(B),u1_struct_0(C)),u1_struct_0(A)) ) => ! [F] : ( ( v1_funct_1(F) & v1_funct_2(F,k2_zfmisc_1(u1_struct_0(B),u1_struct_0(C)),u1_struct_0(A)) & m2_relset_1(F,k2_zfmisc_1(u1_struct_0(B),u1_struct_0(C)),u1_struct_0(A)) ) => k2_bilinear(A,B,C,k2_bilinear(A,B,C,D,E),F) = k2_bilinear(A,B,C,D,k2_bilinear(A,B,C,E,F)) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d3_bilinear,d3_bilinear,d6_rlvect_1,d3_bilinear,d3_bilinear,t120_funct_2]), [file(bilinear,t3_bilinear),interesting(0.00)]). fof(t59_vectsp_1,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_rlvect_1(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & v4_group_1(A) & v7_vectsp_1(A) & v8_vectsp_1(A) & l3_vectsp_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( ( ~ v3_struct_0(C) & v4_rlvect_1(C) & v5_rlvect_1(C) & v6_rlvect_1(C) & v12_vectsp_1(C,A) & l4_vectsp_1(C,A) ) => ! [D] : ( m1_subset_1(D,u1_struct_0(C)) => ( k6_vectsp_1(A,C,k1_rlvect_1(A),D) = k1_rlvect_1(C) & k6_vectsp_1(A,C,k5_rlvect_1(A,k2_group_1(A)),D) = k5_rlvect_1(C,D) & k6_vectsp_1(A,C,B,k1_rlvect_1(C)) = k1_rlvect_1(C) ) ) ) ) ) ), file(vectsp_1,t59_vectsp_1), [interesting(0.00)]). fof(t41_vectsp_1,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & v5_vectsp_1(A) & l3_vectsp_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => k1_group_1(A,k5_rlvect_1(A,B),C) = k5_rlvect_1(A,k1_group_1(A,B,C)) ) ) ) ), file(vectsp_1,t41_vectsp_1), [interesting(0.00)]). fof(d19_vectsp_1,definition,( ! [A] : ( ( ~ v3_struct_0(A) & l1_vectsp_1(A) ) => ( v8_vectsp_1(A) <=> ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => k1_group_1(A,k2_group_1(A),B) = B ) ) ) ), file(vectsp_1,d19_vectsp_1), [interesting(0.00)]). fof(t40_bilinear,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_rlvect_1(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & v4_group_1(A) & v7_vectsp_1(A) & v8_vectsp_1(A) & l3_vectsp_1(A) ) => ! [B] : ( ( ~ v3_struct_0(B) & v3_rlvect_1(B) & v4_rlvect_1(B) & v5_rlvect_1(B) & v6_rlvect_1(B) & v12_vectsp_1(B,A) & l4_vectsp_1(B,A) ) => ! [C] : ( ( ~ v3_struct_0(C) & v3_rlvect_1(C) & v4_rlvect_1(C) & v5_rlvect_1(C) & v6_rlvect_1(C) & v12_vectsp_1(C,A) & l4_vectsp_1(C,A) ) => ! [D] : ( m1_subset_1(D,u1_struct_0(B)) => ! [E] : ( m1_subset_1(E,u1_struct_0(B)) => ! [F] : ( m1_subset_1(F,u1_struct_0(C)) => ! [G] : ( m1_subset_1(G,u1_struct_0(C)) => ! [H] : ( m1_subset_1(H,u1_struct_0(A)) => ! [I] : ( m1_subset_1(I,u1_struct_0(A)) => ! [J] : ( ( v1_funct_1(J) & v1_funct_2(J,k2_zfmisc_1(u1_struct_0(B),u1_struct_0(C)),u1_struct_0(A)) & v1_bilinear(J,A,B,C) & v2_bilinear(J,A,B,C) & v3_bilinear(J,A,B,C) & v4_bilinear(J,A,B,C) & m2_relset_1(J,k2_zfmisc_1(u1_struct_0(B),u1_struct_0(C)),u1_struct_0(A)) ) => k8_funct_2(k2_zfmisc_1(u1_struct_0(B),u1_struct_0(C)),u1_struct_0(A),J,k1_domain_1(u1_struct_0(B),u1_struct_0(C),k6_rlvect_1(B,D,k6_vectsp_1(A,B,H,E)),k6_rlvect_1(C,F,k6_vectsp_1(A,C,I,G)))) = k6_rlvect_1(A,k6_rlvect_1(A,k8_funct_2(k2_zfmisc_1(u1_struct_0(B),u1_struct_0(C)),u1_struct_0(A),J,k1_domain_1(u1_struct_0(B),u1_struct_0(C),D,F)),k1_group_1(A,I,k8_funct_2(k2_zfmisc_1(u1_struct_0(B),u1_struct_0(C)),u1_struct_0(A),J,k1_domain_1(u1_struct_0(B),u1_struct_0(C),D,G)))),k6_rlvect_1(A,k1_group_1(A,H,k8_funct_2(k2_zfmisc_1(u1_struct_0(B),u1_struct_0(C)),u1_struct_0(A),J,k1_domain_1(u1_struct_0(B),u1_struct_0(C),E,F))),k1_group_1(A,H,k1_group_1(A,I,k8_funct_2(k2_zfmisc_1(u1_struct_0(B),u1_struct_0(C)),u1_struct_0(A),J,k1_domain_1(u1_struct_0(B),u1_struct_0(C),E,G)))))) ) ) ) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t38_bilinear,t33_bilinear,t32_bilinear,t32_bilinear,t33_bilinear]), [file(bilinear,t40_bilinear),interesting(0.00)]). fof(d5_seqm_3,definition,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) ) => ( v5_seqm_3(A) <=> ! [B,C] : ( ( r2_hidden(B,k1_relat_1(A)) & r2_hidden(C,k1_relat_1(A)) ) => k1_funct_1(A,B) = k1_funct_1(A,C) ) ) ) ), file(seqm_3,d5_seqm_3), [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(t30_bilinear,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & l3_vectsp_1(A) ) => ! [B] : ( ( ~ v3_struct_0(B) & v5_rlvect_1(B) & l4_vectsp_1(B,A) ) => ! [C] : ( ( ~ v3_struct_0(C) & v5_rlvect_1(C) & l4_vectsp_1(C,A) ) => ! [D] : ( ( v1_funct_1(D) & v1_funct_2(D,k2_zfmisc_1(u1_struct_0(B),u1_struct_0(C)),u1_struct_0(A)) & v1_bilinear(D,A,B,C) & m2_relset_1(D,k2_zfmisc_1(u1_struct_0(B),u1_struct_0(C)),u1_struct_0(A)) ) => ! [E] : ( m1_subset_1(E,u1_struct_0(B)) => k8_funct_2(k2_zfmisc_1(u1_struct_0(B),u1_struct_0(C)),u1_struct_0(A),D,k1_domain_1(u1_struct_0(B),u1_struct_0(C),E,k1_rlvect_1(C))) = k1_rlvect_1(A) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d7_rlvect_1,t28_bilinear,t22_rlvect_1]), [file(bilinear,t30_bilinear),interesting(0.00)]). fof(t31_bilinear,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & l3_vectsp_1(A) ) => ! [B] : ( ( ~ v3_struct_0(B) & v5_rlvect_1(B) & l4_vectsp_1(B,A) ) => ! [C] : ( ( ~ v3_struct_0(C) & v5_rlvect_1(C) & l4_vectsp_1(C,A) ) => ! [D] : ( ( v1_funct_1(D) & v1_funct_2(D,k2_zfmisc_1(u1_struct_0(B),u1_struct_0(C)),u1_struct_0(A)) & v2_bilinear(D,A,B,C) & m2_relset_1(D,k2_zfmisc_1(u1_struct_0(B),u1_struct_0(C)),u1_struct_0(A)) ) => ! [E] : ( m1_subset_1(E,u1_struct_0(C)) => k8_funct_2(k2_zfmisc_1(u1_struct_0(B),u1_struct_0(C)),u1_struct_0(A),D,k1_domain_1(u1_struct_0(B),u1_struct_0(C),k1_rlvect_1(B),E)) = k1_rlvect_1(A) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d7_rlvect_1,t27_bilinear,t22_rlvect_1]), [file(bilinear,t31_bilinear),interesting(0.00)]). fof(t9_domain_1,theorem,( ! [A,B] : ( ~ v1_xboole_0(B) => ! [C] : ( ~ v1_xboole_0(C) => ~ ( r2_hidden(A,k2_zfmisc_1(B,C)) & ! [D] : ( m1_subset_1(D,B) => ! [E] : ( m1_subset_1(E,C) => A != k4_tarski(D,E) ) ) ) ) ) ), file(domain_1,t9_domain_1), [interesting(0.00)]). fof(t41_bilinear,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & l3_vectsp_1(A) ) => ! [B] : ( ( ~ v3_struct_0(B) & v5_rlvect_1(B) & l4_vectsp_1(B,A) ) => ! [C] : ( ( ~ v3_struct_0(C) & v5_rlvect_1(C) & l4_vectsp_1(C,A) ) => ! [D] : ( ( v1_funct_1(D) & v1_funct_2(D,k2_zfmisc_1(u1_struct_0(B),u1_struct_0(C)),u1_struct_0(A)) & m2_relset_1(D,k2_zfmisc_1(u1_struct_0(B),u1_struct_0(C)),u1_struct_0(A)) ) => ( ( v1_bilinear(D,A,B,C) | v2_bilinear(D,A,B,C) ) => ( v5_seqm_3(D) <=> ! [E] : ( m1_subset_1(E,u1_struct_0(B)) => ! [F] : ( m1_subset_1(F,u1_struct_0(C)) => k8_funct_2(k2_zfmisc_1(u1_struct_0(B),u1_struct_0(C)),u1_struct_0(A),D,k1_domain_1(u1_struct_0(B),u1_struct_0(C),E,F)) = k1_rlvect_1(A) ) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d1_funct_2,d5_seqm_3,t30_bilinear,d5_seqm_3,t31_bilinear,t9_domain_1,t9_domain_1,d5_seqm_3]), [file(bilinear,t41_bilinear),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(t42_bilinear,theorem,( ! [A] : ( l2_struct_0(A) => ! [B] : ( ( ~ v3_struct_0(B) & l4_vectsp_1(B,A) ) => ! [C] : ( ( v1_funct_1(C) & v1_funct_2(C,k2_zfmisc_1(u1_struct_0(B),u1_struct_0(B)),u1_struct_0(A)) & m2_relset_1(C,k2_zfmisc_1(u1_struct_0(B),u1_struct_0(B)),u1_struct_0(A)) ) => ( r1_tarski(k12_bilinear(A,B,B,C),k14_bilinear(A,B,C)) & r1_tarski(k13_bilinear(A,B,B,C),k14_bilinear(A,B,C)) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d3_tarski,d3_tarski]), [file(bilinear,t42_bilinear),interesting(0.00)]). fof(d1_vectsp_4,definition,( ! [A] : ( ( ~ v3_struct_0(A) & l1_group_1(A) ) => ! [B] : ( ( ~ v3_struct_0(B) & l4_vectsp_1(B,A) ) => ! [C] : ( m1_subset_1(C,k1_zfmisc_1(u1_struct_0(B))) => ( v1_vectsp_4(C,A,B) <=> ( ! [D] : ( m1_subset_1(D,u1_struct_0(B)) => ! [E] : ( m1_subset_1(E,u1_struct_0(B)) => ( ( r2_hidden(D,C) & r2_hidden(E,C) ) => r2_hidden(k2_rlvect_1(B,D,E),C) ) ) ) & ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ! [E] : ( m1_subset_1(E,u1_struct_0(B)) => ( r2_hidden(E,C) => r2_hidden(k6_vectsp_1(A,B,D,E),C) ) ) ) ) ) ) ) ) ), file(vectsp_4,d1_vectsp_4), [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(d20_bilinear,definition,( ! [A] : ( ( ~ v3_struct_0(A) & v3_rlvect_1(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & v4_group_1(A) & v7_vectsp_1(A) & v8_vectsp_1(A) & l3_vectsp_1(A) ) => ! [B] : ( ( ~ v3_struct_0(B) & l4_vectsp_1(B,A) ) => ! [C] : ( ( ~ v3_struct_0(C) & v3_rlvect_1(C) & v4_rlvect_1(C) & v5_rlvect_1(C) & v6_rlvect_1(C) & v12_vectsp_1(C,A) & l4_vectsp_1(C,A) ) => ! [D] : ( ( v1_funct_1(D) & v1_funct_2(D,k2_zfmisc_1(u1_struct_0(B),u1_struct_0(C)),u1_struct_0(A)) & v1_bilinear(D,A,B,C) & v3_bilinear(D,A,B,C) & m2_relset_1(D,k2_zfmisc_1(u1_struct_0(B),u1_struct_0(C)),u1_struct_0(A)) ) => ! [E] : ( ( ~ v3_struct_0(E) & v11_vectsp_1(E,A) & m1_vectsp_4(E,A,C) ) => ( E = k16_bilinear(A,B,C,D) <=> u1_struct_0(E) = k13_bilinear(A,B,C,D) ) ) ) ) ) ) ), file(bilinear,d20_bilinear), [interesting(0.00)]). fof(t23_vectsp10,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_rlvect_1(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & v4_group_1(A) & v7_vectsp_1(A) & v8_vectsp_1(A) & l3_vectsp_1(A) ) => ! [B] : ( ( ~ v3_struct_0(B) & v3_rlvect_1(B) & v4_rlvect_1(B) & v5_rlvect_1(B) & v6_rlvect_1(B) & v12_vectsp_1(B,A) & l4_vectsp_1(B,A) ) => ! [C] : ( m1_vectsp_4(C,A,B) => ! [D] : ( m1_subset_1(D,u1_struct_0(k6_vectsp10(A,B,C))) => ( m2_vectsp_4(D,A,B,C) & ? [E] : ( m1_subset_1(E,u1_struct_0(B)) & D = k3_vectsp_4(A,B,E,C) ) ) ) ) ) ) ), file(vectsp10,t23_vectsp10), [interesting(0.00)]). fof(d21_bilinear,definition,( ! [A] : ( ( ~ v3_struct_0(A) & v3_rlvect_1(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & v4_group_1(A) & v7_vectsp_1(A) & v8_vectsp_1(A) & l3_vectsp_1(A) ) => ! [B] : ( ( ~ v3_struct_0(B) & v3_rlvect_1(B) & v4_rlvect_1(B) & v5_rlvect_1(B) & v6_rlvect_1(B) & v12_vectsp_1(B,A) & l4_vectsp_1(B,A) ) => ! [C] : ( ( ~ v3_struct_0(C) & l4_vectsp_1(C,A) ) => ! [D] : ( ( v1_funct_1(D) & v1_funct_2(D,k2_zfmisc_1(u1_struct_0(B),u1_struct_0(C)),u1_struct_0(A)) & v2_bilinear(D,A,B,C) & v4_bilinear(D,A,B,C) & m2_relset_1(D,k2_zfmisc_1(u1_struct_0(B),u1_struct_0(C)),u1_struct_0(A)) ) => ! [E] : ( ( v1_funct_1(E) & v1_funct_2(E,k2_zfmisc_1(u1_struct_0(k6_vectsp10(A,B,k15_bilinear(A,B,C,D))),u1_struct_0(C)),u1_struct_0(A)) & v2_bilinear(E,A,k6_vectsp10(A,B,k15_bilinear(A,B,C,D)),C) & v4_bilinear(E,A,k6_vectsp10(A,B,k15_bilinear(A,B,C,D)),C) & m2_relset_1(E,k2_zfmisc_1(u1_struct_0(k6_vectsp10(A,B,k15_bilinear(A,B,C,D))),u1_struct_0(C)),u1_struct_0(A)) ) => ( E = k17_bilinear(A,B,C,D) <=> ! [F] : ( m1_subset_1(F,u1_struct_0(k6_vectsp10(A,B,k15_bilinear(A,B,C,D)))) => ! [G] : ( m1_subset_1(G,u1_struct_0(C)) => ! [H] : ( m1_subset_1(H,u1_struct_0(B)) => ( F = k3_vectsp_4(A,B,H,k15_bilinear(A,B,C,D)) => k8_funct_2(k2_zfmisc_1(u1_struct_0(k6_vectsp10(A,B,k15_bilinear(A,B,C,D))),u1_struct_0(C)),u1_struct_0(A),E,k1_domain_1(u1_struct_0(k6_vectsp10(A,B,k15_bilinear(A,B,C,D))),u1_struct_0(C),F,G)) = k8_funct_2(k2_zfmisc_1(u1_struct_0(B),u1_struct_0(C)),u1_struct_0(A),D,k1_domain_1(u1_struct_0(B),u1_struct_0(C),H,G)) ) ) ) ) ) ) ) ) ) ) ), file(bilinear,d21_bilinear), [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(t24_vectsp10,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_rlvect_1(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & v4_group_1(A) & v7_vectsp_1(A) & v8_vectsp_1(A) & l3_vectsp_1(A) ) => ! [B] : ( ( ~ v3_struct_0(B) & v3_rlvect_1(B) & v4_rlvect_1(B) & v5_rlvect_1(B) & v6_rlvect_1(B) & v12_vectsp_1(B,A) & l4_vectsp_1(B,A) ) => ! [C] : ( m1_vectsp_4(C,A,B) => ! [D] : ( m1_subset_1(D,u1_struct_0(B)) => ( m2_vectsp_4(k3_vectsp_4(A,B,D,C),A,B,C) & m1_subset_1(k3_vectsp_4(A,B,D,C),u1_struct_0(k6_vectsp10(A,B,C))) ) ) ) ) ) ), file(vectsp10,t24_vectsp10), [interesting(0.00)]). fof(t37_vectsp_4,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_rlvect_1(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & v4_group_1(A) & v7_vectsp_1(A) & v8_vectsp_1(A) & l3_vectsp_1(A) ) => ! [B] : ( ( ~ v3_struct_0(B) & v3_rlvect_1(B) & v4_rlvect_1(B) & v5_rlvect_1(B) & v6_rlvect_1(B) & v12_vectsp_1(B,A) & l4_vectsp_1(B,A) ) => ! [C] : ( ( v11_vectsp_1(C,A) & m1_vectsp_4(C,A,B) ) => ! [D] : ( ( v11_vectsp_1(D,A) & m1_vectsp_4(D,A,B) ) => ( u1_struct_0(C) = u1_struct_0(D) => C = D ) ) ) ) ) ), file(vectsp_4,t37_vectsp_4), [interesting(0.00)]). fof(d19_bilinear,definition,( ! [A] : ( ( ~ v3_struct_0(A) & v3_rlvect_1(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & v4_group_1(A) & v7_vectsp_1(A) & v8_vectsp_1(A) & l3_vectsp_1(A) ) => ! [B] : ( ( ~ v3_struct_0(B) & v3_rlvect_1(B) & v4_rlvect_1(B) & v5_rlvect_1(B) & v6_rlvect_1(B) & v12_vectsp_1(B,A) & l4_vectsp_1(B,A) ) => ! [C] : ( ( ~ v3_struct_0(C) & l4_vectsp_1(C,A) ) => ! [D] : ( ( v1_funct_1(D) & v1_funct_2(D,k2_zfmisc_1(u1_struct_0(B),u1_struct_0(C)),u1_struct_0(A)) & v2_bilinear(D,A,B,C) & v4_bilinear(D,A,B,C) & m2_relset_1(D,k2_zfmisc_1(u1_struct_0(B),u1_struct_0(C)),u1_struct_0(A)) ) => ! [E] : ( ( ~ v3_struct_0(E) & v11_vectsp_1(E,A) & m1_vectsp_4(E,A,B) ) => ( E = k15_bilinear(A,B,C,D) <=> u1_struct_0(E) = k12_bilinear(A,B,C,D) ) ) ) ) ) ) ), file(bilinear,d19_bilinear), [interesting(0.00)]). fof(d22_bilinear,definition,( ! [A] : ( ( ~ v3_struct_0(A) & v3_rlvect_1(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & v4_group_1(A) & v7_vectsp_1(A) & v8_vectsp_1(A) & l3_vectsp_1(A) ) => ! [B] : ( ( ~ v3_struct_0(B) & l4_vectsp_1(B,A) ) => ! [C] : ( ( ~ v3_struct_0(C) & v3_rlvect_1(C) & v4_rlvect_1(C) & v5_rlvect_1(C) & v6_rlvect_1(C) & v12_vectsp_1(C,A) & l4_vectsp_1(C,A) ) => ! [D] : ( ( v1_funct_1(D) & v1_funct_2(D,k2_zfmisc_1(u1_struct_0(B),u1_struct_0(C)),u1_struct_0(A)) & v1_bilinear(D,A,B,C) & v3_bilinear(D,A,B,C) & m2_relset_1(D,k2_zfmisc_1(u1_struct_0(B),u1_struct_0(C)),u1_struct_0(A)) ) => ! [E] : ( ( v1_funct_1(E) & v1_funct_2(E,k2_zfmisc_1(u1_struct_0(B),u1_struct_0(k6_vectsp10(A,C,k16_bilinear(A,B,C,D)))),u1_struct_0(A)) & v1_bilinear(E,A,B,k6_vectsp10(A,C,k16_bilinear(A,B,C,D))) & v3_bilinear(E,A,B,k6_vectsp10(A,C,k16_bilinear(A,B,C,D))) & m2_relset_1(E,k2_zfmisc_1(u1_struct_0(B),u1_struct_0(k6_vectsp10(A,C,k16_bilinear(A,B,C,D)))),u1_struct_0(A)) ) => ( E = k18_bilinear(A,B,C,D) <=> ! [F] : ( m1_subset_1(F,u1_struct_0(k6_vectsp10(A,C,k16_bilinear(A,B,C,D)))) => ! [G] : ( m1_subset_1(G,u1_struct_0(B)) => ! [H] : ( m1_subset_1(H,u1_struct_0(C)) => ( F = k3_vectsp_4(A,C,H,k16_bilinear(A,B,C,D)) => k8_funct_2(k2_zfmisc_1(u1_struct_0(B),u1_struct_0(k6_vectsp10(A,C,k16_bilinear(A,B,C,D)))),u1_struct_0(A),E,k1_domain_1(u1_struct_0(B),u1_struct_0(k6_vectsp10(A,C,k16_bilinear(A,B,C,D))),G,F)) = k8_funct_2(k2_zfmisc_1(u1_struct_0(B),u1_struct_0(C)),u1_struct_0(A),D,k1_domain_1(u1_struct_0(B),u1_struct_0(C),G,H)) ) ) ) ) ) ) ) ) ) ) ), file(bilinear,d22_bilinear), [interesting(0.00)]). fof(d23_bilinear,definition,( ! [A] : ( ( ~ v3_struct_0(A) & v3_rlvect_1(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & v4_group_1(A) & v7_vectsp_1(A) & v8_vectsp_1(A) & l3_vectsp_1(A) ) => ! [B] : ( ( ~ v3_struct_0(B) & v3_rlvect_1(B) & v4_rlvect_1(B) & v5_rlvect_1(B) & v6_rlvect_1(B) & v12_vectsp_1(B,A) & l4_vectsp_1(B,A) ) => ! [C] : ( ( ~ v3_struct_0(C) & v3_rlvect_1(C) & v4_rlvect_1(C) & v5_rlvect_1(C) & v6_rlvect_1(C) & v12_vectsp_1(C,A) & l4_vectsp_1(C,A) ) => ! [D] : ( ( v1_funct_1(D) & v1_funct_2(D,k2_zfmisc_1(u1_struct_0(B),u1_struct_0(C)),u1_struct_0(A)) & v1_bilinear(D,A,B,C) & v2_bilinear(D,A,B,C) & v3_bilinear(D,A,B,C) & v4_bilinear(D,A,B,C) & m2_relset_1(D,k2_zfmisc_1(u1_struct_0(B),u1_struct_0(C)),u1_struct_0(A)) ) => ! [E] : ( ( v1_funct_1(E) & v1_funct_2(E,k2_zfmisc_1(u1_struct_0(k6_vectsp10(A,B,k15_bilinear(A,B,C,D))),u1_struct_0(k6_vectsp10(A,C,k16_bilinear(A,B,C,D)))),u1_struct_0(A)) & v1_bilinear(E,A,k6_vectsp10(A,B,k15_bilinear(A,B,C,D)),k6_vectsp10(A,C,k16_bilinear(A,B,C,D))) & v2_bilinear(E,A,k6_vectsp10(A,B,k15_bilinear(A,B,C,D)),k6_vectsp10(A,C,k16_bilinear(A,B,C,D))) & v3_bilinear(E,A,k6_vectsp10(A,B,k15_bilinear(A,B,C,D)),k6_vectsp10(A,C,k16_bilinear(A,B,C,D))) & v4_bilinear(E,A,k6_vectsp10(A,B,k15_bilinear(A,B,C,D)),k6_vectsp10(A,C,k16_bilinear(A,B,C,D))) & m2_relset_1(E,k2_zfmisc_1(u1_struct_0(k6_vectsp10(A,B,k15_bilinear(A,B,C,D))),u1_struct_0(k6_vectsp10(A,C,k16_bilinear(A,B,C,D)))),u1_struct_0(A)) ) => ( E = k19_bilinear(A,B,C,D) <=> ! [F] : ( m1_subset_1(F,u1_struct_0(k6_vectsp10(A,B,k15_bilinear(A,B,C,D)))) => ! [G] : ( m1_subset_1(G,u1_struct_0(k6_vectsp10(A,C,k16_bilinear(A,B,C,D)))) => ! [H] : ( m1_subset_1(H,u1_struct_0(B)) => ! [I] : ( m1_subset_1(I,u1_struct_0(C)) => ( ( F = k3_vectsp_4(A,B,H,k15_bilinear(A,B,C,D)) & G = k3_vectsp_4(A,C,I,k16_bilinear(A,B,C,D)) ) => k8_funct_2(k2_zfmisc_1(u1_struct_0(k6_vectsp10(A,B,k15_bilinear(A,B,C,D))),u1_struct_0(k6_vectsp10(A,C,k16_bilinear(A,B,C,D)))),u1_struct_0(A),E,k1_domain_1(u1_struct_0(k6_vectsp10(A,B,k15_bilinear(A,B,C,D))),u1_struct_0(k6_vectsp10(A,C,k16_bilinear(A,B,C,D))),F,G)) = k8_funct_2(k2_zfmisc_1(u1_struct_0(B),u1_struct_0(C)),u1_struct_0(A),D,k1_domain_1(u1_struct_0(B),u1_struct_0(C),H,I)) ) ) ) ) ) ) ) ) ) ) ) ), file(bilinear,d23_bilinear), [interesting(0.00)]). fof(t9_funct_1,theorem,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) ) => ! [B] : ( ( v1_relat_1(B) & v1_funct_1(B) ) => ( ( k1_relat_1(A) = k1_relat_1(B) & ! [C] : ( r2_hidden(C,k1_relat_1(A)) => k1_funct_1(A,C) = k1_funct_1(B,C) ) ) => A = B ) ) ) ), file(funct_1,t9_funct_1), [interesting(0.00)]). fof(d9_vectsp10,definition,( ! [A] : ( ( ~ v3_struct_0(A) & l2_struct_0(A) ) => ! [B] : ( ( ~ v3_struct_0(B) & l4_vectsp_1(B,A) ) => ! [C] : ( ( v1_funct_1(C) & v1_funct_2(C,u1_struct_0(B),u1_struct_0(A)) & m2_relset_1(C,u1_struct_0(B),u1_struct_0(A)) ) => k8_vectsp10(A,B,C) = a_3_1_vectsp10(A,B,C) ) ) ) ), file(vectsp10,d9_vectsp10), [interesting(0.00)]). fof(t44_vectsp_1,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & v4_group_1(A) & v7_group_1(A) & v7_vectsp_1(A) & v8_vectsp_1(A) & v9_vectsp_1(A) & l3_vectsp_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ( k10_group_1(A,B,C) = k1_rlvect_1(A) <=> ( B = k1_rlvect_1(A) | C = k1_rlvect_1(A) ) ) ) ) ) ), file(vectsp_1,t44_vectsp_1), [interesting(0.00)]). fof(t51_bilinear,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & v7_vectsp_1(A) & l3_vectsp_1(A) ) => ! [B] : ( ( ~ v3_struct_0(B) & l4_vectsp_1(B,A) ) => ! [C] : ( ( ~ v3_struct_0(C) & l4_vectsp_1(C,A) ) => ! [D] : ( ( v1_funct_1(D) & v1_funct_2(D,u1_struct_0(B),u1_struct_0(A)) & m2_relset_1(D,u1_struct_0(B),u1_struct_0(A)) ) => ! [E] : ( ( v1_funct_1(E) & v1_funct_2(E,u1_struct_0(C),u1_struct_0(A)) & m2_relset_1(E,u1_struct_0(C),u1_struct_0(A)) ) => r1_tarski(k8_vectsp10(A,B,D),k12_bilinear(A,B,C,k11_bilinear(A,B,C,D,E))) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d9_vectsp10,d3_tarski,d11_bilinear,t39_vectsp_1]), [file(bilinear,t51_bilinear),interesting(0.00)]). fof(d11_vectsp10,definition,( ! [A] : ( ( ~ v3_struct_0(A) & v3_rlvect_1(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & v4_group_1(A) & v7_vectsp_1(A) & v8_vectsp_1(A) & l3_vectsp_1(A) ) => ! [B] : ( ( ~ v3_struct_0(B) & v3_rlvect_1(B) & v4_rlvect_1(B) & v5_rlvect_1(B) & v6_rlvect_1(B) & v12_vectsp_1(B,A) & l4_vectsp_1(B,A) ) => ! [C] : ( ( v1_funct_1(C) & v1_funct_2(C,u1_struct_0(B),u1_struct_0(A)) & v1_hahnban1(C,A,B) & v2_hahnban1(C,A,B) & m2_relset_1(C,u1_struct_0(B),u1_struct_0(A)) ) => ! [D] : ( ( ~ v3_struct_0(D) & v11_vectsp_1(D,A) & m1_vectsp_4(D,A,B) ) => ( D = k9_vectsp10(A,B,C) <=> u1_struct_0(D) = k8_vectsp10(A,B,C) ) ) ) ) ) ), file(vectsp10,d11_vectsp10), [interesting(0.00)]). fof(t36_vectsp10,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_rlvect_1(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & v4_group_1(A) & v7_vectsp_1(A) & v8_vectsp_1(A) & l3_vectsp_1(A) ) => ! [B] : ( ( ~ v3_struct_0(B) & v3_rlvect_1(B) & v4_rlvect_1(B) & v5_rlvect_1(B) & v6_rlvect_1(B) & v12_vectsp_1(B,A) & l4_vectsp_1(B,A) ) => ! [C] : ( ( v1_funct_1(C) & v1_funct_2(C,u1_struct_0(B),u1_struct_0(A)) & v1_hahnban1(C,A,B) & v2_hahnban1(C,A,B) & m2_relset_1(C,u1_struct_0(B),u1_struct_0(A)) ) => ! [D] : ( m1_subset_1(D,u1_struct_0(k6_vectsp10(A,B,k9_vectsp10(A,B,C)))) => ! [E] : ( m1_subset_1(E,u1_struct_0(B)) => ( D = k3_vectsp_4(A,B,E,k9_vectsp10(A,B,C)) => k8_funct_2(u1_struct_0(k6_vectsp10(A,B,k9_vectsp10(A,B,C))),u1_struct_0(A),k11_vectsp10(A,B,C),D) = k8_funct_2(u1_struct_0(B),u1_struct_0(A),C,E) ) ) ) ) ) ) ), file(vectsp10,t36_vectsp10), [interesting(0.00)]). fof(t53_bilinear,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & v7_vectsp_1(A) & l3_vectsp_1(A) ) => ! [B] : ( ( ~ v3_struct_0(B) & l4_vectsp_1(B,A) ) => ! [C] : ( ( ~ v3_struct_0(C) & l4_vectsp_1(C,A) ) => ! [D] : ( ( v1_funct_1(D) & v1_funct_2(D,u1_struct_0(B),u1_struct_0(A)) & m2_relset_1(D,u1_struct_0(B),u1_struct_0(A)) ) => ! [E] : ( ( v1_funct_1(E) & v1_funct_2(E,u1_struct_0(C),u1_struct_0(A)) & m2_relset_1(E,u1_struct_0(C),u1_struct_0(A)) ) => r1_tarski(k8_vectsp10(A,C,E),k13_bilinear(A,B,C,k11_bilinear(A,B,C,D,E))) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d9_vectsp10,d3_tarski,d11_bilinear,t36_vectsp_1]), [file(bilinear,t53_bilinear),interesting(0.00)]). fof(d26_bilinear,definition,( ! [A] : ( l1_struct_0(A) => ! [B] : ( l4_vectsp_1(B,A) => ! [C] : ( ( v1_funct_1(C) & v1_funct_2(C,k2_zfmisc_1(u1_struct_0(B),u1_struct_0(B)),u1_struct_0(A)) & m2_relset_1(C,k2_zfmisc_1(u1_struct_0(B),u1_struct_0(B)),u1_struct_0(A)) ) => ( v7_bilinear(C,A,B) <=> ! [D] : ( m1_subset_1(D,u1_struct_0(B)) => ! [E] : ( m1_subset_1(E,u1_struct_0(B)) => k1_funct_1(C,k4_tarski(D,E)) = k1_funct_1(C,k4_tarski(E,D)) ) ) ) ) ) ) ), file(bilinear,d26_bilinear), [interesting(0.00)]). fof(t58_bilinear,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & v4_vectsp_1(A) & l3_vectsp_1(A) ) => ! [B] : ( ( ~ v3_struct_0(B) & l4_vectsp_1(B,A) ) => ! [C] : ( ( v1_funct_1(C) & v1_funct_2(C,k2_zfmisc_1(u1_struct_0(B),u1_struct_0(B)),u1_struct_0(A)) & v1_bilinear(C,A,B,B) & v2_bilinear(C,A,B,B) & v3_bilinear(C,A,B,B) & v4_bilinear(C,A,B,B) & v7_bilinear(C,A,B) & m2_relset_1(C,k2_zfmisc_1(u1_struct_0(B),u1_struct_0(B)),u1_struct_0(A)) ) => k12_bilinear(A,B,B,C) = k13_bilinear(A,B,B,C) ) ) ) ), inference(mizar_proof,[status(thm)],[d3_tarski,d26_bilinear,d10_xboole_0,d3_tarski,d26_bilinear]), [file(bilinear,t58_bilinear),interesting(0.00)]). fof(d11_vectsp_1,definition,( ! [A] : ( ( ~ v3_struct_0(A) & l3_vectsp_1(A) ) => ( v4_vectsp_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)) => k1_group_1(A,B,k2_rlvect_1(A,C,D)) = k2_rlvect_1(A,k1_group_1(A,B,C),k1_group_1(A,B,D)) ) ) ) ) ) ), file(vectsp_1,d11_vectsp_1), [interesting(0.00)]). fof(d27_bilinear,definition,( ! [A] : ( l2_struct_0(A) => ! [B] : ( l4_vectsp_1(B,A) => ! [C] : ( ( v1_funct_1(C) & v1_funct_2(C,k2_zfmisc_1(u1_struct_0(B),u1_struct_0(B)),u1_struct_0(A)) & m2_relset_1(C,k2_zfmisc_1(u1_struct_0(B),u1_struct_0(B)),u1_struct_0(A)) ) => ( v8_bilinear(C,A,B) <=> ! [D] : ( m1_subset_1(D,u1_struct_0(B)) => k1_funct_1(C,k4_tarski(D,D)) = k1_rlvect_1(A) ) ) ) ) ) ), file(bilinear,d27_bilinear), [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(t19_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) = k1_rlvect_1(A) => B = k5_rlvect_1(A,C) ) ) ) ) ), file(rlvect_1,t19_rlvect_1), [interesting(0.00)]). fof(t59_bilinear,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & l1_rlvect_1(A) ) => ! [B] : ( ( ~ v3_struct_0(B) & l4_vectsp_1(B,A) ) => ! [C] : ( ( v1_funct_1(C) & v1_funct_2(C,k2_zfmisc_1(u1_struct_0(B),u1_struct_0(B)),u1_struct_0(A)) & v1_bilinear(C,A,B,B) & v2_bilinear(C,A,B,B) & v8_bilinear(C,A,B) & m2_relset_1(C,k2_zfmisc_1(u1_struct_0(B),u1_struct_0(B)),u1_struct_0(A)) ) => ! [D] : ( m1_subset_1(D,u1_struct_0(B)) => ! [E] : ( m1_subset_1(E,u1_struct_0(B)) => k8_funct_2(k2_zfmisc_1(u1_struct_0(B),u1_struct_0(B)),u1_struct_0(A),C,k1_domain_1(u1_struct_0(B),u1_struct_0(B),D,E)) = k5_rlvect_1(A,k8_funct_2(k2_zfmisc_1(u1_struct_0(B),u1_struct_0(B)),u1_struct_0(A),C,k1_domain_1(u1_struct_0(B),u1_struct_0(B),E,D))) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d27_bilinear,t29_bilinear,d27_bilinear,d27_bilinear,d7_rlvect_1,t10_rlvect_1,t19_rlvect_1]), [file(bilinear,t59_bilinear),interesting(0.00)]). fof(t25_rlvect_1,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & l1_rlvect_1(A) ) => k5_rlvect_1(A,k1_rlvect_1(A)) = k1_rlvect_1(A) ) ), file(rlvect_1,t25_rlvect_1), [interesting(0.00)]). fof(d12_vectsp_1,definition,( ! [A] : ( ( ~ v3_struct_0(A) & l3_vectsp_1(A) ) => ( v5_vectsp_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)) => k1_group_1(A,k2_rlvect_1(A,C,D),B) = k2_rlvect_1(A,k1_group_1(A,C,B),k1_group_1(A,D,B)) ) ) ) ) ) ), file(vectsp_1,d12_vectsp_1), [interesting(0.00)]). fof(d4_group_1,definition,( ! [A] : ( ( ~ v3_struct_0(A) & l1_group_1(A) ) => ( v4_group_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)) => k1_group_1(A,k1_group_1(A,B,C),D) = k1_group_1(A,B,k1_group_1(A,C,D)) ) ) ) ) ) ), file(group_1,d4_group_1), [interesting(0.00)]). fof(t7_bilinear,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v4_group_1(A) & l3_vectsp_1(A) ) => ! [B] : ( ( ~ v3_struct_0(B) & l4_vectsp_1(B,A) ) => ! [C] : ( ( ~ v3_struct_0(C) & l4_vectsp_1(C,A) ) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ! [E] : ( m1_subset_1(E,u1_struct_0(A)) => ! [F] : ( ( v1_funct_1(F) & v1_funct_2(F,k2_zfmisc_1(u1_struct_0(B),u1_struct_0(C)),u1_struct_0(A)) & m2_relset_1(F,k2_zfmisc_1(u1_struct_0(B),u1_struct_0(C)),u1_struct_0(A)) ) => k3_bilinear(A,B,C,F,k1_group_1(A,D,E)) = k3_bilinear(A,B,C,k3_bilinear(A,B,C,F,E),D) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d4_bilinear,d4_group_1,d4_bilinear,d4_bilinear,t120_funct_2]), [file(bilinear,t7_bilinear),interesting(0.00)]). fof(t8_bilinear,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v8_vectsp_1(A) & l3_vectsp_1(A) ) => ! [B] : ( ( ~ v3_struct_0(B) & l4_vectsp_1(B,A) ) => ! [C] : ( ( ~ v3_struct_0(C) & l4_vectsp_1(C,A) ) => ! [D] : ( ( v1_funct_1(D) & v1_funct_2(D,k2_zfmisc_1(u1_struct_0(B),u1_struct_0(C)),u1_struct_0(A)) & m2_relset_1(D,k2_zfmisc_1(u1_struct_0(B),u1_struct_0(C)),u1_struct_0(A)) ) => k3_bilinear(A,B,C,D,k2_group_1(A)) = D ) ) ) ) ), inference(mizar_proof,[status(thm)],[d4_bilinear,d19_vectsp_1,t120_funct_2]), [file(bilinear,t8_bilinear),interesting(0.00)]).