fof(t44_bhsp_4,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) & v2_bhsp_1(A) & l1_bhsp_1(A) ) => ! [B] : ( ( v1_funct_1(B) & v1_funct_2(B,k5_numbers,u1_struct_0(A)) & m2_relset_1(B,k5_numbers,u1_struct_0(A)) ) => ( ( v4_bhsp_3(A) & v2_bhsp_4(B,A) ) => v1_bhsp_4(B,A) ) ) ) ), inference(mizar_proof,[status(thm)],[d8_bhsp_4,t3_seq_2,t25_series_1,t143_complex1,t10_xreal_1,t2_xreal_1,t41_bhsp_4,t2_xreal_1,t10_bhsp_4]), [file(bhsp_4,t44_bhsp_4),interesting(1.00)]). fof(t14_bhsp_4,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) & v2_bhsp_1(A) & l1_bhsp_1(A) ) => ! [B] : ( ( v1_funct_1(B) & v1_funct_2(B,k5_numbers,u1_struct_0(A)) & m2_relset_1(B,k5_numbers,u1_struct_0(A)) ) => ( ? [C] : ( m2_subset_1(C,k1_numbers,k5_numbers) & v1_bhsp_4(k2_bhsp_3(A,B,C),A) ) => v1_bhsp_4(B,A) ) ) ) ), inference(mizar_proof,[status(thm)],[t13_bhsp_4,d2_bhsp_4,t57_funcop_1,t13_funcop_1,t1_bhsp_2,d1_bhsp_4,d5_bhsp_3,d5_bhsp_3,d1_bhsp_4,d1_bhsp_4,d6_rlvect_1,d5_bhsp_3,d5_bhsp_3,d1_bhsp_4,d5_bhsp_3,s1_nat_1,d5_normsp_1,t37_bhsp_3,t3_bhsp_2,t46_bhsp_3,d2_bhsp_4]), [file(bhsp_4,t14_bhsp_4),interesting(0.89)]). fof(t9_bhsp_4,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) & v2_bhsp_1(A) & l1_bhsp_1(A) ) => ! [B] : ( ( v1_funct_1(B) & v1_funct_2(B,k5_numbers,u1_struct_0(A)) & m2_relset_1(B,k5_numbers,u1_struct_0(A)) ) => ( v1_bhsp_4(B,A) => ( v1_bhsp_2(B,A) & k1_bhsp_2(A,B) = k1_rlvect_1(A) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d2_bhsp_4,t44_bhsp_3,t14_bhsp_2,t28_rlvect_1,d1_bhsp_4,d5_bhsp_3,d5_bhsp_3,d5_normsp_1,d5_normsp_1,d6_normsp_1,t28_rlvect_1,t10_rlvect_1,t113_funct_2,t83_bhsp_1,t4_bhsp_2,t46_bhsp_3,t43_bhsp_3,t33_bhsp_3]), [file(bhsp_4,t9_bhsp_4),interesting(0.87)]). fof(t13_bhsp_4,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) & v2_bhsp_1(A) & l1_bhsp_1(A) ) => ! [B] : ( ( v1_funct_1(B) & v1_funct_2(B,k5_numbers,u1_struct_0(A)) & m2_relset_1(B,k5_numbers,u1_struct_0(A)) ) => ( v1_bhsp_4(B,A) => ! [C] : ( m2_subset_1(C,k1_numbers,k5_numbers) => v1_bhsp_4(k2_bhsp_3(A,B,C),A) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t35_bhsp_3,d2_bhsp_4,t44_bhsp_3,t37_bhsp_3,t57_funcop_1,t13_funcop_1,t1_bhsp_2,t12_bhsp_4,t4_bhsp_2,d2_bhsp_4,s1_nat_1]), [file(bhsp_4,t13_bhsp_4),interesting(0.85)]). fof(t53_bhsp_4,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) & v2_bhsp_1(A) & l1_bhsp_1(A) ) => ! [B] : ( ( v1_funct_1(B) & v1_funct_2(B,k5_numbers,u1_struct_0(A)) & m2_relset_1(B,k5_numbers,u1_struct_0(A)) ) => ! [C] : ( ( v1_funct_1(C) & v1_funct_2(C,k5_numbers,k1_numbers) & m2_relset_1(C,k5_numbers,k1_numbers) ) => ( ( v4_bhsp_3(A) & v1_bhsp_3(B,A) & v3_bhsp_4(C) ) => v1_bhsp_3(k7_bhsp_4(A,B,C),A) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d7_bhsp_3,d6_bhsp_3,d1_xreal_0,d10_bhsp_4,t58_seq_4,t50_bhsp_4,t9_bhsp_3]), [file(bhsp_4,t53_bhsp_4),interesting(0.69)]). fof(t43_bhsp_4,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) & v2_bhsp_1(A) & l1_bhsp_1(A) ) => ! [B] : ( ( v1_funct_1(B) & v1_funct_2(B,k5_numbers,u1_struct_0(A)) & m2_relset_1(B,k5_numbers,u1_struct_0(A)) ) => ! [C] : ( m2_subset_1(C,k1_numbers,k5_numbers) => ! [D] : ( m2_subset_1(D,k1_numbers,k5_numbers) => r1_xreal_0(k3_bhsp_1(A,k4_bhsp_4(A,B,D,C)),k18_complex1(k6_bhsp_4(k2_bhsp_2(A,B),D,C))) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t42_bhsp_4]), [file(bhsp_4,t43_bhsp_4),interesting(0.67)]). fof(t42_bhsp_4,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) & v2_bhsp_1(A) & l1_bhsp_1(A) ) => ! [B] : ( ( v1_funct_1(B) & v1_funct_2(B,k5_numbers,u1_struct_0(A)) & m2_relset_1(B,k5_numbers,u1_struct_0(A)) ) => ! [C] : ( m2_subset_1(C,k1_numbers,k5_numbers) => ! [D] : ( m2_subset_1(D,k1_numbers,k5_numbers) => r1_xreal_0(k3_bhsp_1(A,k6_rlvect_1(A,k3_bhsp_4(A,B,D),k3_bhsp_4(A,B,C))),k18_complex1(k5_real_1(k5_bhsp_4(k2_bhsp_2(A,B),D),k5_bhsp_4(k2_bhsp_2(A,B),C)))) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t41_bhsp_4]), [file(bhsp_4,t42_bhsp_4),interesting(0.60)]). fof(t26_bhsp_4,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) & v2_bhsp_1(A) & l1_bhsp_1(A) ) => ! [B] : ( ( v1_funct_1(B) & v1_funct_2(B,k5_numbers,u1_struct_0(A)) & m2_relset_1(B,k5_numbers,u1_struct_0(A)) ) => ( v4_bhsp_3(A) => ( v1_bhsp_4(B,A) <=> ! [C] : ( m1_subset_1(C,k1_numbers) => ~ ( ~ r1_xreal_0(C,0) & ! [D] : ( m2_subset_1(D,k1_numbers,k5_numbers) => ? [E] : ( m2_subset_1(E,k1_numbers,k5_numbers) & ? [F] : ( m2_subset_1(F,k1_numbers,k5_numbers) & r1_xreal_0(D,E) & r1_xreal_0(D,F) & r1_xreal_0(C,k3_bhsp_1(A,k4_bhsp_4(A,B,E,F))) ) ) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t25_bhsp_4,t25_bhsp_4]), [file(bhsp_4,t26_bhsp_4),interesting(0.55)]). fof(t32_bhsp_4,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) & v2_bhsp_1(A) & l1_bhsp_1(A) ) => ! [B] : ( ( v1_funct_1(B) & v1_funct_2(B,k5_numbers,u1_struct_0(A)) & m2_relset_1(B,k5_numbers,u1_struct_0(A)) ) => ~ ( ! [C] : ( m2_subset_1(C,k1_numbers,k5_numbers) => k2_normsp_1(A,B,C) != k1_rlvect_1(A) ) & ? [C] : ( m2_subset_1(C,k1_numbers,k5_numbers) & ! [D] : ( m2_subset_1(D,k1_numbers,k5_numbers) => ( r1_xreal_0(C,D) => r1_xreal_0(1,k6_real_1(k3_bhsp_1(A,k2_normsp_1(A,B,k1_nat_1(D,1))),k3_bhsp_1(A,k2_normsp_1(A,B,D)))) ) ) ) & v1_bhsp_4(B,A) ) ) ) ), inference(mizar_proof,[status(thm)],[t32_bhsp_1,t34_bhsp_1,t29_nat_1,t32_bhsp_1,t34_bhsp_1,t118_real_2,t2_xreal_1,s1_nat_1,t28_nat_1,t31_bhsp_4,t9_bhsp_4]), [file(bhsp_4,t32_bhsp_4),interesting(0.55)]). fof(t52_bhsp_4,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) & v2_bhsp_1(A) & l1_bhsp_1(A) ) => ! [B] : ( ( v1_funct_1(B) & v1_funct_2(B,k5_numbers,u1_struct_0(A)) & m2_relset_1(B,k5_numbers,u1_struct_0(A)) ) => ! [C] : ( ( v1_funct_1(C) & v1_funct_2(C,k5_numbers,k1_numbers) & m2_relset_1(C,k5_numbers,k1_numbers) ) => ( ( v4_seq_2(C) & v1_bhsp_2(B,A) ) => ( v1_bhsp_2(k7_bhsp_4(A,B,C),A) & k1_bhsp_2(A,k7_bhsp_4(A,B,C)) = k3_rlvect_1(A,k1_bhsp_2(A,B),k2_seq_2(C)) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t50_bhsp_4,t27_seq_2,t15_seq_2,d1_xreal_0,t34_bhsp_1,t10_xreal_1,t127_real_2,d7_seq_2,d2_bhsp_2,t37_nat_1,t2_xreal_1,t37_nat_1,t2_xreal_1,d5_bhsp_1,d9_bhsp_4,t10_rlvect_1,t28_rlvect_1,t43_rlvect_1,t43_rlvect_1,t41_rlvect_1,t47_rlvect_1,t36_bhsp_1,t48_rlvect_1,t49_rlvect_1,t33_bhsp_1,t33_bhsp_1,t132_complex1,t34_bhsp_1,t98_xreal_1,t66_xreal_1,t10_xreal_1,t75_xcmplx_1,t75_xcmplx_1,t63_xcmplx_1,t90_xcmplx_1,t2_xreal_1,d5_bhsp_1,d2_bhsp_2]), [file(bhsp_4,t52_bhsp_4),interesting(0.52)]). fof(t55_bhsp_4,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) & v2_bhsp_1(A) & l1_bhsp_1(A) ) => ! [B] : ( ( v1_funct_1(B) & v1_funct_2(B,k5_numbers,u1_struct_0(A)) & m2_relset_1(B,k5_numbers,u1_struct_0(A)) ) => ! [C] : ( ( v1_funct_1(C) & v1_funct_2(C,k5_numbers,k1_numbers) & m2_relset_1(C,k5_numbers,k1_numbers) ) => ! [D] : ( m2_subset_1(D,k1_numbers,k5_numbers) => k2_normsp_1(A,k1_bhsp_4(A,k7_bhsp_4(A,B,C)),k1_nat_1(D,1)) = k6_rlvect_1(A,k2_normsp_1(A,k7_bhsp_4(A,k1_bhsp_4(A,B),C),k1_nat_1(D,1)),k2_normsp_1(A,k1_bhsp_4(A,k7_bhsp_4(A,k1_bhsp_4(A,B),k10_seq_1(k1_seqm_3(C,1),C))),D)) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t54_bhsp_4,t43_rlvect_1,t28_rlvect_1,t26_rlvect_1,t15_seq_1,t37_seq_1,t25_seq_1,t25_seq_1,t32_seq_1,t48_bhsp_4,t3_bhsp_4,d8_normsp_1,t29_rlvect_1]), [file(bhsp_4,t55_bhsp_4),interesting(0.49)]). fof(t25_bhsp_4,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) & v2_bhsp_1(A) & l1_bhsp_1(A) ) => ! [B] : ( ( v1_funct_1(B) & v1_funct_2(B,k5_numbers,u1_struct_0(A)) & m2_relset_1(B,k5_numbers,u1_struct_0(A)) ) => ( v4_bhsp_3(A) => ( v1_bhsp_4(B,A) <=> ! [C] : ( m1_subset_1(C,k1_numbers) => ~ ( ~ r1_xreal_0(C,0) & ! [D] : ( m2_subset_1(D,k1_numbers,k5_numbers) => ? [E] : ( m2_subset_1(E,k1_numbers,k5_numbers) & ? [F] : ( m2_subset_1(F,k1_numbers,k5_numbers) & r1_xreal_0(D,E) & r1_xreal_0(D,F) & r1_xreal_0(C,k3_bhsp_1(A,k6_rlvect_1(A,k3_bhsp_4(A,B,E),k3_bhsp_4(A,B,F)))) ) ) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t10_bhsp_4,t10_bhsp_4]), [file(bhsp_4,t25_bhsp_4),interesting(0.47)]). fof(t12_bhsp_4,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) & v2_bhsp_1(A) & l1_bhsp_1(A) ) => ! [B] : ( ( v1_funct_1(B) & v1_funct_2(B,k5_numbers,u1_struct_0(A)) & m2_relset_1(B,k5_numbers,u1_struct_0(A)) ) => ! [C] : ( ( v1_funct_1(C) & v1_funct_2(C,k5_numbers,u1_struct_0(A)) & m2_relset_1(C,k5_numbers,u1_struct_0(A)) ) => ( ! [D] : ( m2_subset_1(D,k1_numbers,k5_numbers) => k2_normsp_1(A,C,D) = k2_normsp_1(A,B,0) ) => k1_bhsp_4(A,k2_bhsp_3(A,B,1)) = k4_normsp_1(A,k2_bhsp_3(A,k1_bhsp_4(A,B),1),C) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d6_normsp_1,d5_bhsp_3,d1_bhsp_4,d1_bhsp_4,d6_rlvect_1,t28_rlvect_1,t10_rlvect_1,d5_bhsp_3,d6_normsp_1,d5_bhsp_3,d1_bhsp_4,d6_rlvect_1,d5_bhsp_3,d6_normsp_1,d5_bhsp_3,d1_bhsp_4]), [file(bhsp_4,t12_bhsp_4),interesting(0.45)]). fof(t39_bhsp_4,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) & v2_bhsp_1(A) & l1_bhsp_1(A) ) => ! [B] : ( ( v1_funct_1(B) & v1_funct_2(B,k5_numbers,u1_struct_0(A)) & m2_relset_1(B,k5_numbers,u1_struct_0(A)) ) => ! [C] : ( m2_subset_1(C,k1_numbers,k5_numbers) => r1_xreal_0(k3_bhsp_1(A,k2_normsp_1(A,k1_bhsp_4(A,B),C)),k2_seq_1(k5_numbers,k1_numbers,k1_series_1(k2_bhsp_2(A,B)),C)) ) ) ) ), inference(mizar_proof,[status(thm)],[d1_series_1,d3_bhsp_2,d1_bhsp_4,d1_bhsp_4,t36_bhsp_1,t8_xreal_1,t2_xreal_1,d3_bhsp_2,d1_series_1,s1_nat_1]), [file(bhsp_4,t39_bhsp_4),interesting(0.44)]). fof(t41_bhsp_4,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) & v2_bhsp_1(A) & l1_bhsp_1(A) ) => ! [B] : ( ( v1_funct_1(B) & v1_funct_2(B,k5_numbers,u1_struct_0(A)) & m2_relset_1(B,k5_numbers,u1_struct_0(A)) ) => ! [C] : ( m2_subset_1(C,k1_numbers,k5_numbers) => ! [D] : ( m2_subset_1(D,k1_numbers,k5_numbers) => r1_xreal_0(k3_bhsp_1(A,k6_rlvect_1(A,k2_normsp_1(A,k1_bhsp_4(A,B),D),k2_normsp_1(A,k1_bhsp_4(A,B),C))),k18_complex1(k5_real_1(k2_seq_1(k5_numbers,k1_numbers,k1_series_1(k2_bhsp_2(A,B)),D),k2_seq_1(k5_numbers,k1_numbers,k1_series_1(k2_bhsp_2(A,B)),C)))) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t28_rlvect_1,t32_bhsp_1,t132_complex1,t37_bhsp_4,d1_bhsp_4,d6_rlvect_1,t36_bhsp_1,t9_xreal_1,t2_xreal_1,t11_seqm_3,t50_xreal_1,d1_absvalue,t34_bhsp_1,t9_xreal_1,d1_series_1,d3_bhsp_2,d1_absvalue,s1_nat_1,t18_int_1,t28_rlvect_1,t32_bhsp_1,t132_complex1,t37_bhsp_4,d1_bhsp_4,t41_rlvect_1,t36_bhsp_1,t37_bhsp_1,t8_xreal_1,t2_xreal_1,t138_complex1,t11_seqm_3,t50_xreal_1,d1_absvalue,t34_bhsp_1,t9_xreal_1,t138_complex1,d1_series_1,d3_bhsp_2,d1_absvalue,s1_nat_1,t18_int_1]), [file(bhsp_4,t41_bhsp_4),interesting(0.41)]). fof(t36_bhsp_4,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) & v2_bhsp_1(A) & l1_bhsp_1(A) ) => ! [B] : ( ( v1_funct_1(B) & v1_funct_2(B,k5_numbers,u1_struct_0(A)) & m2_relset_1(B,k5_numbers,u1_struct_0(A)) ) => ! [C] : ( ( v1_funct_1(C) & v1_funct_2(C,k5_numbers,k1_numbers) & m2_relset_1(C,k5_numbers,k1_numbers) ) => ~ ( ! [D] : ( m2_subset_1(D,k1_numbers,k5_numbers) => k2_seq_1(k5_numbers,k1_numbers,C,D) = k2_power(D,k2_seq_1(k5_numbers,k1_numbers,k2_bhsp_2(A,B),D)) ) & v4_seq_2(C) & ~ r1_xreal_0(k2_seq_2(C),1) & v1_bhsp_4(B,A) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t52_xreal_1,d7_seq_2,t29_nat_1,t2_xreal_1,t34_bhsp_1,d3_bhsp_2,t9_seq_2,t8_xreal_1,t19_prepower,t29_nat_1,t2_xreal_1,t5_power,t31_bhsp_4,t9_bhsp_4]), [file(bhsp_4,t36_bhsp_4),interesting(0.40)]). fof(t35_bhsp_4,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) & v2_bhsp_1(A) & l1_bhsp_1(A) ) => ! [B] : ( ( v1_funct_1(B) & v1_funct_2(B,k5_numbers,u1_struct_0(A)) & m2_relset_1(B,k5_numbers,u1_struct_0(A)) ) => ! [C] : ( ( v1_funct_1(C) & v1_funct_2(C,k5_numbers,k1_numbers) & m2_relset_1(C,k5_numbers,k1_numbers) ) => ~ ( ! [D] : ( m2_subset_1(D,k1_numbers,k5_numbers) => k2_seq_1(k5_numbers,k1_numbers,C,D) = k2_power(D,k2_seq_1(k5_numbers,k1_numbers,k2_bhsp_2(A,B),D)) ) & ? [D] : ( m2_subset_1(D,k1_numbers,k5_numbers) & ! [E] : ( m2_subset_1(E,k1_numbers,k5_numbers) => ( r1_xreal_0(D,E) => r1_xreal_0(1,k2_seq_1(k5_numbers,k1_numbers,C,E)) ) ) ) & v1_bhsp_4(B,A) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t29_nat_1,t2_xreal_1,t34_bhsp_1,d3_bhsp_2,t19_prepower,t29_nat_1,t2_xreal_1,t5_power,t31_bhsp_4,t9_bhsp_4]), [file(bhsp_4,t35_bhsp_4),interesting(0.38)]). fof(t56_bhsp_4,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) & v2_bhsp_1(A) & l1_bhsp_1(A) ) => ! [B] : ( ( v1_funct_1(B) & v1_funct_2(B,k5_numbers,u1_struct_0(A)) & m2_relset_1(B,k5_numbers,u1_struct_0(A)) ) => ! [C] : ( ( v1_funct_1(C) & v1_funct_2(C,k5_numbers,k1_numbers) & m2_relset_1(C,k5_numbers,k1_numbers) ) => ! [D] : ( m2_subset_1(D,k1_numbers,k5_numbers) => k3_bhsp_4(A,k7_bhsp_4(A,B,C),k1_nat_1(D,1)) = k6_rlvect_1(A,k2_normsp_1(A,k7_bhsp_4(A,k1_bhsp_4(A,B),C),k1_nat_1(D,1)),k3_bhsp_4(A,k7_bhsp_4(A,k1_bhsp_4(A,B),k10_seq_1(k1_seqm_3(C,1),C)),D)) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t55_bhsp_4]), [file(bhsp_4,t56_bhsp_4),interesting(0.38)]). fof(t54_bhsp_4,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) & v2_bhsp_1(A) & l1_bhsp_1(A) ) => ! [B] : ( ( v1_funct_1(B) & v1_funct_2(B,k5_numbers,u1_struct_0(A)) & m2_relset_1(B,k5_numbers,u1_struct_0(A)) ) => ! [C] : ( ( v1_funct_1(C) & v1_funct_2(C,k5_numbers,k1_numbers) & m2_relset_1(C,k5_numbers,k1_numbers) ) => ! [D] : ( m2_subset_1(D,k1_numbers,k5_numbers) => k2_normsp_1(A,k1_bhsp_4(A,k7_bhsp_4(A,k1_bhsp_4(A,B),k10_seq_1(C,k1_seqm_3(C,1)))),D) = k6_rlvect_1(A,k2_normsp_1(A,k1_bhsp_4(A,k7_bhsp_4(A,B,C)),k1_nat_1(D,1)),k2_normsp_1(A,k7_bhsp_4(A,k1_bhsp_4(A,B),C),k1_nat_1(D,1))) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d1_bhsp_4,d1_bhsp_4,d9_bhsp_4,d9_bhsp_4,d1_bhsp_4,d9_bhsp_4,d1_bhsp_4,t15_seq_1,t11_seq_1,t14_seq_1,d9_seqm_3,t49_rlvect_1,d9_bhsp_4,d1_bhsp_4,d1_bhsp_4,d9_rlvect_1,t10_rlvect_1,t28_rlvect_1,d6_rlvect_1,d6_rlvect_1,d6_rlvect_1,t28_rlvect_1,t10_rlvect_1,t43_rlvect_1,t28_rlvect_1,d1_bhsp_4,t26_rlvect_1,d6_rlvect_1,d9_bhsp_4,d9_bhsp_4,d9_rlvect_1,d9_seqm_3,t14_seq_1,t11_seq_1,t15_seq_1,d6_rlvect_1,d6_rlvect_1,d9_bhsp_4,d1_bhsp_4,d9_rlvect_1,d1_bhsp_4,d9_bhsp_4,d6_rlvect_1,t28_rlvect_1,t10_rlvect_1,s1_nat_1]), [file(bhsp_4,t54_bhsp_4),interesting(0.37)]). fof(t10_bhsp_4,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) & v2_bhsp_1(A) & l1_bhsp_1(A) ) => ! [B] : ( ( v1_funct_1(B) & v1_funct_2(B,k5_numbers,u1_struct_0(A)) & m2_relset_1(B,k5_numbers,u1_struct_0(A)) ) => ( v4_bhsp_3(A) => ( v1_bhsp_4(B,A) <=> ! [C] : ( m1_subset_1(C,k1_numbers) => ~ ( ~ r1_xreal_0(C,0) & ! [D] : ( m2_subset_1(D,k1_numbers,k5_numbers) => ? [E] : ( m2_subset_1(E,k1_numbers,k5_numbers) & ? [F] : ( m2_subset_1(F,k1_numbers,k5_numbers) & r1_xreal_0(D,E) & r1_xreal_0(D,F) & r1_xreal_0(C,k3_bhsp_1(A,k6_rlvect_1(A,k2_normsp_1(A,k1_bhsp_4(A,B),E),k2_normsp_1(A,k1_bhsp_4(A,B),F)))) ) ) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d7_bhsp_3,d2_bhsp_4,t9_bhsp_3,t2_bhsp_3,t2_bhsp_3,d6_bhsp_3,d2_bhsp_4]), [file(bhsp_4,t10_bhsp_4),interesting(0.35)]). fof(t33_bhsp_4,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) & v2_bhsp_1(A) & l1_bhsp_1(A) ) => ! [B] : ( ( v1_funct_1(B) & v1_funct_2(B,k5_numbers,u1_struct_0(A)) & m2_relset_1(B,k5_numbers,u1_struct_0(A)) ) => ! [C] : ( ( v1_funct_1(C) & v1_funct_2(C,k5_numbers,k1_numbers) & m2_relset_1(C,k5_numbers,k1_numbers) ) => ~ ( ! [D] : ( m2_subset_1(D,k1_numbers,k5_numbers) => k2_normsp_1(A,B,D) != k1_rlvect_1(A) ) & ! [D] : ( m2_subset_1(D,k1_numbers,k5_numbers) => k2_seq_1(k5_numbers,k1_numbers,C,D) = k6_real_1(k3_bhsp_1(A,k2_normsp_1(A,B,k1_nat_1(D,1))),k3_bhsp_1(A,k2_normsp_1(A,B,D))) ) & v4_seq_2(C) & ~ r1_xreal_0(k2_seq_2(C),1) & v1_bhsp_4(B,A) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t52_xreal_1,d7_seq_2,t29_nat_1,t2_xreal_1,t9_seq_2,t8_xreal_1,t32_bhsp_4]), [file(bhsp_4,t33_bhsp_4),interesting(0.23)]). fof(s4_recdef_1,theorem,( ? [A] : ( v1_funct_1(A) & v1_funct_2(A,k5_numbers,f1_s4_recdef_1) & m2_relset_1(A,k5_numbers,f1_s4_recdef_1) & k8_funct_2(k5_numbers,f1_s4_recdef_1,A,0) = f2_s4_recdef_1 & ! [B] : ( m2_subset_1(B,k1_numbers,k5_numbers) => k8_funct_2(k5_numbers,f1_s4_recdef_1,A,k1_nat_1(B,1)) = f3_s4_recdef_1(B,k8_funct_2(k5_numbers,f1_s4_recdef_1,A,B)) ) ) ), file(recdef_1,s4_recdef_1), [interesting(0.00)]). fof(s1_bhsp_4,theorem,( ? [A] : ( v1_funct_1(A) & v1_funct_2(A,k5_numbers,u1_struct_0(f1_s1_bhsp_4)) & m2_relset_1(A,k5_numbers,u1_struct_0(f1_s1_bhsp_4)) & k2_normsp_1(f1_s1_bhsp_4,A,0) = f2_s1_bhsp_4 & ! [B] : ( m2_subset_1(B,k1_numbers,k5_numbers) => ! [C] : ( m1_subset_1(C,u1_struct_0(f1_s1_bhsp_4)) => ( C = k2_normsp_1(f1_s1_bhsp_4,A,B) => k2_normsp_1(f1_s1_bhsp_4,A,k1_nat_1(B,1)) = f3_s1_bhsp_4(B,C) ) ) ) ) ), inference(mizar_proof,[status(thm)],[s4_recdef_1]), [file(bhsp_4,s1_bhsp_4),interesting(0.00)]). fof(d2_bhsp_4,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) & v2_bhsp_1(A) & l1_bhsp_1(A) ) => ! [B] : ( ( v1_funct_1(B) & v1_funct_2(B,k5_numbers,u1_struct_0(A)) & m2_relset_1(B,k5_numbers,u1_struct_0(A)) ) => ( v1_bhsp_4(B,A) <=> v1_bhsp_2(k1_bhsp_4(A,B),A) ) ) ) ), file(bhsp_4,d2_bhsp_4), [interesting(0.00)]). fof(t24_bhsp_3,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) & v2_bhsp_1(A) & l1_bhsp_1(A) ) => ! [B] : ( ( v1_funct_1(B) & v1_funct_2(B,k5_numbers,u1_struct_0(A)) & m2_relset_1(B,k5_numbers,u1_struct_0(A)) ) => ( v1_bhsp_2(B,A) => v2_bhsp_3(B,A) ) ) ) ), file(bhsp_3,t24_bhsp_3), [interesting(0.00)]). fof(t11_bhsp_4,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) & v2_bhsp_1(A) & l1_bhsp_1(A) ) => ! [B] : ( ( v1_funct_1(B) & v1_funct_2(B,k5_numbers,u1_struct_0(A)) & m2_relset_1(B,k5_numbers,u1_struct_0(A)) ) => ( v1_bhsp_4(B,A) => v2_bhsp_3(k1_bhsp_4(A,B),A) ) ) ) ), inference(mizar_proof,[status(thm)],[d2_bhsp_4,t24_bhsp_3]), [file(bhsp_4,t11_bhsp_4),interesting(0.00)]). fof(t35_bhsp_3,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) & v2_bhsp_1(A) & l1_bhsp_1(A) ) => ! [B] : ( ( v1_funct_1(B) & v1_funct_2(B,k5_numbers,u1_struct_0(A)) & m2_relset_1(B,k5_numbers,u1_struct_0(A)) ) => k2_bhsp_3(A,B,0) = B ) ) ), file(bhsp_3,t35_bhsp_3), [interesting(0.00)]). fof(t44_bhsp_3,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) & v2_bhsp_1(A) & l1_bhsp_1(A) ) => ! [B] : ( ( v1_funct_1(B) & v1_funct_2(B,k5_numbers,u1_struct_0(A)) & m2_relset_1(B,k5_numbers,u1_struct_0(A)) ) => ! [C] : ( m2_subset_1(C,k1_numbers,k5_numbers) => ( v1_bhsp_2(B,A) => ( v1_bhsp_2(k2_bhsp_3(A,B,C),A) & k1_bhsp_2(A,k2_bhsp_3(A,B,C)) = k1_bhsp_2(A,B) ) ) ) ) ) ), file(bhsp_3,t44_bhsp_3), [interesting(0.00)]). fof(t37_bhsp_3,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) & v2_bhsp_1(A) & l1_bhsp_1(A) ) => ! [B] : ( ( v1_funct_1(B) & v1_funct_2(B,k5_numbers,u1_struct_0(A)) & m2_relset_1(B,k5_numbers,u1_struct_0(A)) ) => ! [C] : ( m2_subset_1(C,k1_numbers,k5_numbers) => ! [D] : ( m2_subset_1(D,k1_numbers,k5_numbers) => k2_bhsp_3(A,k2_bhsp_3(A,B,C),D) = k2_bhsp_3(A,B,k1_nat_1(C,D)) ) ) ) ) ), file(bhsp_3,t37_bhsp_3), [interesting(0.00)]). fof(t57_funcop_1,theorem,( ! [A,B,C] : ( r2_hidden(C,B) => ( v1_funct_1(k2_funcop_1(A,C)) & v1_funct_2(k2_funcop_1(A,C),A,B) & m2_relset_1(k2_funcop_1(A,C),A,B) ) ) ), file(funcop_1,t57_funcop_1), [interesting(0.00)]). fof(t13_funcop_1,theorem,( ! [A,B,C] : ( r2_hidden(B,A) => k1_funct_1(k2_funcop_1(A,C),B) = C ) ), file(funcop_1,t13_funcop_1), [interesting(0.00)]). fof(t1_bhsp_2,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) & v2_bhsp_1(A) & l1_bhsp_1(A) ) => ! [B] : ( ( v1_funct_1(B) & v1_funct_2(B,k5_numbers,u1_struct_0(A)) & m2_relset_1(B,k5_numbers,u1_struct_0(A)) ) => ( v5_seqm_3(B) => v1_bhsp_2(B,A) ) ) ) ), file(bhsp_2,t1_bhsp_2), [interesting(0.00)]). fof(d6_normsp_1,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] : ( ( v1_funct_1(B) & v1_funct_2(B,k5_numbers,u1_struct_0(A)) & m2_relset_1(B,k5_numbers,u1_struct_0(A)) ) => ! [C] : ( ( v1_funct_1(C) & v1_funct_2(C,k5_numbers,u1_struct_0(A)) & m2_relset_1(C,k5_numbers,u1_struct_0(A)) ) => ! [D] : ( ( v1_funct_1(D) & v1_funct_2(D,k5_numbers,u1_struct_0(A)) & m2_relset_1(D,k5_numbers,u1_struct_0(A)) ) => ( D = k4_normsp_1(A,B,C) <=> ! [E] : ( m2_subset_1(E,k1_numbers,k5_numbers) => k2_normsp_1(A,D,E) = k6_rlvect_1(A,k2_normsp_1(A,B,E),k2_normsp_1(A,C,E)) ) ) ) ) ) ) ), file(normsp_1,d6_normsp_1), [interesting(0.00)]). fof(d5_bhsp_3,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) & v2_bhsp_1(A) & l1_bhsp_1(A) ) => ! [B] : ( ( v1_funct_1(B) & v1_funct_2(B,k5_numbers,u1_struct_0(A)) & m2_relset_1(B,k5_numbers,u1_struct_0(A)) ) => ! [C] : ( m2_subset_1(C,k1_numbers,k5_numbers) => ! [D] : ( ( v1_funct_1(D) & v1_funct_2(D,k5_numbers,u1_struct_0(A)) & m2_relset_1(D,k5_numbers,u1_struct_0(A)) ) => ( D = k2_bhsp_3(A,B,C) <=> ! [E] : ( m2_subset_1(E,k1_numbers,k5_numbers) => k2_normsp_1(A,D,E) = k2_normsp_1(A,B,k1_nat_1(E,C)) ) ) ) ) ) ) ), file(bhsp_3,d5_bhsp_3), [interesting(0.00)]). fof(d1_bhsp_4,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) & v2_bhsp_1(A) & l1_bhsp_1(A) ) => ! [B] : ( ( v1_funct_1(B) & v1_funct_2(B,k5_numbers,u1_struct_0(A)) & m2_relset_1(B,k5_numbers,u1_struct_0(A)) ) => ! [C] : ( ( v1_funct_1(C) & v1_funct_2(C,k5_numbers,u1_struct_0(A)) & m2_relset_1(C,k5_numbers,u1_struct_0(A)) ) => ( C = k1_bhsp_4(A,B) <=> ( k2_normsp_1(A,C,0) = k2_normsp_1(A,B,0) & ! [D] : ( m2_subset_1(D,k1_numbers,k5_numbers) => k2_normsp_1(A,C,k1_nat_1(D,1)) = k4_rlvect_1(A,k2_normsp_1(A,C,D),k2_normsp_1(A,B,k1_nat_1(D,1))) ) ) ) ) ) ) ), file(bhsp_4,d1_bhsp_4), [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(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(t4_bhsp_2,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) & v2_bhsp_1(A) & l1_bhsp_1(A) ) => ! [B] : ( ( v1_funct_1(B) & v1_funct_2(B,k5_numbers,u1_struct_0(A)) & m2_relset_1(B,k5_numbers,u1_struct_0(A)) ) => ! [C] : ( ( v1_funct_1(C) & v1_funct_2(C,k5_numbers,u1_struct_0(A)) & m2_relset_1(C,k5_numbers,u1_struct_0(A)) ) => ( ( v1_bhsp_2(B,A) & v1_bhsp_2(C,A) ) => v1_bhsp_2(k4_normsp_1(A,B,C),A) ) ) ) ) ), file(bhsp_2,t4_bhsp_2), [interesting(0.00)]). fof(s1_nat_1,theorem, ( ( p1_s1_nat_1(0) & ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ( p1_s1_nat_1(A) => p1_s1_nat_1(k1_nat_1(A,1)) ) ) ) => ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => p1_s1_nat_1(A) ) ), file(nat_1,s1_nat_1), [interesting(0.00)]). fof(d5_normsp_1,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] : ( ( v1_funct_1(B) & v1_funct_2(B,k5_numbers,u1_struct_0(A)) & m2_relset_1(B,k5_numbers,u1_struct_0(A)) ) => ! [C] : ( ( v1_funct_1(C) & v1_funct_2(C,k5_numbers,u1_struct_0(A)) & m2_relset_1(C,k5_numbers,u1_struct_0(A)) ) => ! [D] : ( ( v1_funct_1(D) & v1_funct_2(D,k5_numbers,u1_struct_0(A)) & m2_relset_1(D,k5_numbers,u1_struct_0(A)) ) => ( D = k3_normsp_1(A,B,C) <=> ! [E] : ( m2_subset_1(E,k1_numbers,k5_numbers) => k2_normsp_1(A,D,E) = k4_rlvect_1(A,k2_normsp_1(A,B,E),k2_normsp_1(A,C,E)) ) ) ) ) ) ) ), file(normsp_1,d5_normsp_1), [interesting(0.00)]). fof(t3_bhsp_2,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) & v2_bhsp_1(A) & l1_bhsp_1(A) ) => ! [B] : ( ( v1_funct_1(B) & v1_funct_2(B,k5_numbers,u1_struct_0(A)) & m2_relset_1(B,k5_numbers,u1_struct_0(A)) ) => ! [C] : ( ( v1_funct_1(C) & v1_funct_2(C,k5_numbers,u1_struct_0(A)) & m2_relset_1(C,k5_numbers,u1_struct_0(A)) ) => ( ( v1_bhsp_2(B,A) & v1_bhsp_2(C,A) ) => v1_bhsp_2(k3_normsp_1(A,B,C),A) ) ) ) ) ), file(bhsp_2,t3_bhsp_2), [interesting(0.00)]). fof(t46_bhsp_3,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) & v2_bhsp_1(A) & l1_bhsp_1(A) ) => ! [B] : ( ( v1_funct_1(B) & v1_funct_2(B,k5_numbers,u1_struct_0(A)) & m2_relset_1(B,k5_numbers,u1_struct_0(A)) ) => ! [C] : ( ( v1_funct_1(C) & v1_funct_2(C,k5_numbers,u1_struct_0(A)) & m2_relset_1(C,k5_numbers,u1_struct_0(A)) ) => ( v1_bhsp_2(B,A) => ( ! [D] : ( m2_subset_1(D,k1_numbers,k5_numbers) => B != k2_bhsp_3(A,C,D) ) | v1_bhsp_2(C,A) ) ) ) ) ) ), file(bhsp_3,t46_bhsp_3), [interesting(0.00)]). fof(t15_bhsp_4,theorem,( $true ), file(bhsp_4,t15_bhsp_4), [interesting(0.00)]). fof(t19_bhsp_4,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) & v2_bhsp_1(A) & l1_bhsp_1(A) ) => ! [B] : ( ( v1_funct_1(B) & v1_funct_2(B,k5_numbers,u1_struct_0(A)) & m2_relset_1(B,k5_numbers,u1_struct_0(A)) ) => ! [C] : ( m2_subset_1(C,k1_numbers,k5_numbers) => k3_bhsp_4(A,B,k1_nat_1(C,1)) = k4_rlvect_1(A,k3_bhsp_4(A,B,C),k2_normsp_1(A,B,k1_nat_1(C,1))) ) ) ) ), inference(mizar_proof,[status(thm)],[d1_bhsp_4]), [file(bhsp_4,t19_bhsp_4),interesting(0.00)]). fof(t20_bhsp_4,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) & v2_bhsp_1(A) & l1_bhsp_1(A) ) => ! [B] : ( ( v1_funct_1(B) & v1_funct_2(B,k5_numbers,u1_struct_0(A)) & m2_relset_1(B,k5_numbers,u1_struct_0(A)) ) => ! [C] : ( m2_subset_1(C,k1_numbers,k5_numbers) => k2_normsp_1(A,B,k1_nat_1(C,1)) = k6_rlvect_1(A,k3_bhsp_4(A,B,k1_nat_1(C,1)),k3_bhsp_4(A,B,C)) ) ) ) ), inference(mizar_proof,[status(thm)],[t19_bhsp_4,d6_rlvect_1,t28_rlvect_1,t10_rlvect_1]), [file(bhsp_4,t20_bhsp_4),interesting(0.00)]). fof(t21_bhsp_4,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) & v2_bhsp_1(A) & l1_bhsp_1(A) ) => ! [B] : ( ( v1_funct_1(B) & v1_funct_2(B,k5_numbers,u1_struct_0(A)) & m2_relset_1(B,k5_numbers,u1_struct_0(A)) ) => k2_normsp_1(A,B,1) = k6_rlvect_1(A,k3_bhsp_4(A,B,1),k3_bhsp_4(A,B,0)) ) ) ), inference(mizar_proof,[status(thm)],[t20_bhsp_4]), [file(bhsp_4,t21_bhsp_4),interesting(0.00)]). fof(t22_bhsp_4,theorem,( $true ), file(bhsp_4,t22_bhsp_4), [interesting(0.00)]). fof(t17_bhsp_4,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) & v2_bhsp_1(A) & l1_bhsp_1(A) ) => ! [B] : ( ( v1_funct_1(B) & v1_funct_2(B,k5_numbers,u1_struct_0(A)) & m2_relset_1(B,k5_numbers,u1_struct_0(A)) ) => k3_bhsp_4(A,B,1) = k4_rlvect_1(A,k3_bhsp_4(A,B,0),k2_normsp_1(A,B,1)) ) ) ), inference(mizar_proof,[status(thm)],[d1_bhsp_4]), [file(bhsp_4,t17_bhsp_4),interesting(0.00)]). fof(t16_bhsp_4,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) & v2_bhsp_1(A) & l1_bhsp_1(A) ) => ! [B] : ( ( v1_funct_1(B) & v1_funct_2(B,k5_numbers,u1_struct_0(A)) & m2_relset_1(B,k5_numbers,u1_struct_0(A)) ) => k3_bhsp_4(A,B,0) = k2_normsp_1(A,B,0) ) ) ), inference(mizar_proof,[status(thm)],[d1_bhsp_4]), [file(bhsp_4,t16_bhsp_4),interesting(0.00)]). fof(t18_bhsp_4,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) & v2_bhsp_1(A) & l1_bhsp_1(A) ) => ! [B] : ( ( v1_funct_1(B) & v1_funct_2(B,k5_numbers,u1_struct_0(A)) & m2_relset_1(B,k5_numbers,u1_struct_0(A)) ) => k3_bhsp_4(A,B,1) = k4_rlvect_1(A,k2_normsp_1(A,B,0),k2_normsp_1(A,B,1)) ) ) ), inference(mizar_proof,[status(thm)],[t17_bhsp_4,t16_bhsp_4]), [file(bhsp_4,t18_bhsp_4),interesting(0.00)]). fof(t23_bhsp_4,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) & v2_bhsp_1(A) & l1_bhsp_1(A) ) => ! [B] : ( ( v1_funct_1(B) & v1_funct_2(B,k5_numbers,u1_struct_0(A)) & m2_relset_1(B,k5_numbers,u1_struct_0(A)) ) => k4_bhsp_4(A,B,1,0) = k2_normsp_1(A,B,1) ) ) ), inference(mizar_proof,[status(thm)],[t18_bhsp_4,t16_bhsp_4,d6_rlvect_1,t28_rlvect_1,t10_rlvect_1]), [file(bhsp_4,t23_bhsp_4),interesting(0.00)]). fof(t24_bhsp_4,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) & v2_bhsp_1(A) & l1_bhsp_1(A) ) => ! [B] : ( ( v1_funct_1(B) & v1_funct_2(B,k5_numbers,u1_struct_0(A)) & m2_relset_1(B,k5_numbers,u1_struct_0(A)) ) => ! [C] : ( m2_subset_1(C,k1_numbers,k5_numbers) => k4_bhsp_4(A,B,k1_nat_1(C,1),C) = k2_normsp_1(A,B,k1_nat_1(C,1)) ) ) ) ), inference(mizar_proof,[status(thm)],[t20_bhsp_4]), [file(bhsp_4,t24_bhsp_4),interesting(0.00)]). fof(d7_bhsp_3,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) & v2_bhsp_1(A) & l1_bhsp_1(A) ) => ( v4_bhsp_3(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) & v2_bhsp_1(A) & l1_bhsp_1(A) & v3_bhsp_3(A) ) ) ) ), file(bhsp_3,d7_bhsp_3), [interesting(0.00)]). fof(t9_bhsp_3,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) & v2_bhsp_1(A) & l1_bhsp_1(A) ) => ! [B] : ( ( v1_funct_1(B) & v1_funct_2(B,k5_numbers,u1_struct_0(A)) & m2_relset_1(B,k5_numbers,u1_struct_0(A)) ) => ( v1_bhsp_2(B,A) => v1_bhsp_3(B,A) ) ) ) ), file(bhsp_3,t9_bhsp_3), [interesting(0.00)]). fof(t2_bhsp_3,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) & v2_bhsp_1(A) & l1_bhsp_1(A) ) => ! [B] : ( ( v1_funct_1(B) & v1_funct_2(B,k5_numbers,u1_struct_0(A)) & m2_relset_1(B,k5_numbers,u1_struct_0(A)) ) => ( v1_bhsp_3(B,A) <=> ! [C] : ( m1_subset_1(C,k1_numbers) => ~ ( ~ r1_xreal_0(C,0) & ! [D] : ( m2_subset_1(D,k1_numbers,k5_numbers) => ? [E] : ( m2_subset_1(E,k1_numbers,k5_numbers) & ? [F] : ( m2_subset_1(F,k1_numbers,k5_numbers) & r1_xreal_0(D,E) & r1_xreal_0(D,F) & r1_xreal_0(C,k3_bhsp_1(A,k6_rlvect_1(A,k2_normsp_1(A,B,E),k2_normsp_1(A,B,F)))) ) ) ) ) ) ) ) ) ), file(bhsp_3,t2_bhsp_3), [interesting(0.00)]). fof(d6_bhsp_3,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) & v2_bhsp_1(A) & l1_bhsp_1(A) ) => ( v3_bhsp_3(A) <=> ! [B] : ( ( v1_funct_1(B) & v1_funct_2(B,k5_numbers,u1_struct_0(A)) & m2_relset_1(B,k5_numbers,u1_struct_0(A)) ) => ( v1_bhsp_3(B,A) => v1_bhsp_2(B,A) ) ) ) ) ), file(bhsp_3,d6_bhsp_3), [interesting(0.00)]). fof(d8_bhsp_4,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) & v2_bhsp_1(A) & l1_bhsp_1(A) ) => ! [B] : ( ( v1_funct_1(B) & v1_funct_2(B,k5_numbers,u1_struct_0(A)) & m2_relset_1(B,k5_numbers,u1_struct_0(A)) ) => ( v2_bhsp_4(B,A) <=> v1_series_1(k2_bhsp_2(A,B)) ) ) ) ), file(bhsp_4,d8_bhsp_4), [interesting(0.00)]). fof(t10_series_1,theorem,( ! [A] : ( ( v1_funct_1(A) & v1_funct_2(A,k5_numbers,k1_numbers) & m2_relset_1(A,k5_numbers,k1_numbers) ) => ! [B] : ( ( v1_funct_1(B) & v1_funct_2(B,k5_numbers,k1_numbers) & m2_relset_1(B,k5_numbers,k1_numbers) ) => ( ( v1_series_1(A) & v1_series_1(B) ) => ( v1_series_1(k9_seq_1(A,B)) & k2_series_1(k9_seq_1(A,B)) = k3_real_1(k2_series_1(A),k2_series_1(B)) ) ) ) ) ), file(series_1,t10_series_1), [interesting(0.00)]). fof(d3_bhsp_2,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) & v2_bhsp_1(A) & l1_bhsp_1(A) ) => ! [B] : ( ( v1_funct_1(B) & v1_funct_2(B,k5_numbers,u1_struct_0(A)) & m2_relset_1(B,k5_numbers,u1_struct_0(A)) ) => ! [C] : ( ( v1_funct_1(C) & v1_funct_2(C,k5_numbers,k1_numbers) & m2_relset_1(C,k5_numbers,k1_numbers) ) => ( C = k2_bhsp_2(A,B) <=> ! [D] : ( m2_subset_1(D,k1_numbers,k5_numbers) => k2_seq_1(k5_numbers,k1_numbers,C,D) = k3_bhsp_1(A,k2_normsp_1(A,B,D)) ) ) ) ) ) ), file(bhsp_2,d3_bhsp_2), [interesting(0.00)]). fof(t34_bhsp_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) & v2_bhsp_1(A) & l1_bhsp_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => r1_xreal_0(0,k3_bhsp_1(A,B)) ) ) ), file(bhsp_1,t34_bhsp_1), [interesting(0.00)]). fof(t36_bhsp_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) & v2_bhsp_1(A) & l1_bhsp_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => r1_xreal_0(k3_bhsp_1(A,k4_rlvect_1(A,B,C)),k3_real_1(k3_bhsp_1(A,B),k3_bhsp_1(A,C))) ) ) ) ), file(bhsp_1,t36_bhsp_1), [interesting(0.00)]). fof(t11_seq_1,theorem,( ! [A] : ( ( v1_funct_1(A) & v1_funct_2(A,k5_numbers,k1_numbers) & m2_relset_1(A,k5_numbers,k1_numbers) ) => ! [B] : ( ( v1_funct_1(B) & v1_funct_2(B,k5_numbers,k1_numbers) & m2_relset_1(B,k5_numbers,k1_numbers) ) => ! [C] : ( ( v1_funct_1(C) & v1_funct_2(C,k5_numbers,k1_numbers) & m2_relset_1(C,k5_numbers,k1_numbers) ) => ( A = k6_seq_1(k5_numbers,k1_numbers,B,C) <=> ! [D] : ( m2_subset_1(D,k1_numbers,k5_numbers) => k2_seq_1(k5_numbers,k1_numbers,A,D) = k3_real_1(k2_seq_1(k5_numbers,k1_numbers,B,D),k2_seq_1(k5_numbers,k1_numbers,C,D)) ) ) ) ) ) ), file(seq_1,t11_seq_1), [interesting(0.00)]). fof(t24_series_1,theorem,( ! [A] : ( ( v1_funct_1(A) & v1_funct_2(A,k5_numbers,k1_numbers) & m2_relset_1(A,k5_numbers,k1_numbers) ) => ! [B] : ( ( v1_funct_1(B) & v1_funct_2(B,k5_numbers,k1_numbers) & m2_relset_1(B,k5_numbers,k1_numbers) ) => ( ( ! [C] : ( m2_subset_1(C,k1_numbers,k5_numbers) => ( r1_xreal_0(0,k8_funct_2(k5_numbers,k1_numbers,A,C)) & r1_xreal_0(k8_funct_2(k5_numbers,k1_numbers,A,C),k8_funct_2(k5_numbers,k1_numbers,B,C)) ) ) & v1_series_1(B) ) => ( v1_series_1(A) & r1_xreal_0(k2_series_1(A),k2_series_1(B)) ) ) ) ) ), file(series_1,t24_series_1), [interesting(0.00)]). fof(t27_bhsp_4,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) & v2_bhsp_1(A) & l1_bhsp_1(A) ) => ! [B] : ( ( v1_funct_1(B) & v1_funct_2(B,k5_numbers,u1_struct_0(A)) & m2_relset_1(B,k5_numbers,u1_struct_0(A)) ) => ! [C] : ( ( v1_funct_1(C) & v1_funct_2(C,k5_numbers,u1_struct_0(A)) & m2_relset_1(C,k5_numbers,u1_struct_0(A)) ) => ( ( v2_bhsp_4(B,A) & v2_bhsp_4(C,A) ) => v2_bhsp_4(k8_bhsp_1(A,B,C),A) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d8_bhsp_4,d8_bhsp_4,t10_series_1,d3_bhsp_2,t34_bhsp_1,d3_bhsp_2,d5_normsp_1,t36_bhsp_1,d3_bhsp_2,d3_bhsp_2,t11_seq_1,t24_series_1,d8_bhsp_4]), [file(bhsp_4,t27_bhsp_4),interesting(0.00)]). fof(t13_series_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( ( v1_funct_1(B) & v1_funct_2(B,k5_numbers,k1_numbers) & m2_relset_1(B,k5_numbers,k1_numbers) ) => ( v1_series_1(B) => ( v1_series_1(k14_seq_1(B,A)) & k2_series_1(k14_seq_1(B,A)) = k3_xcmplx_0(A,k2_series_1(B)) ) ) ) ) ), file(series_1,t13_series_1), [interesting(0.00)]). fof(d8_normsp_1,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] : ( ( v1_funct_1(B) & v1_funct_2(B,k5_numbers,u1_struct_0(A)) & m2_relset_1(B,k5_numbers,u1_struct_0(A)) ) => ! [C] : ( m1_subset_1(C,k1_numbers) => ! [D] : ( ( v1_funct_1(D) & v1_funct_2(D,k5_numbers,u1_struct_0(A)) & m2_relset_1(D,k5_numbers,u1_struct_0(A)) ) => ( D = k6_normsp_1(A,B,C) <=> ! [E] : ( m2_subset_1(E,k1_numbers,k5_numbers) => k2_normsp_1(A,D,E) = k3_rlvect_1(A,k2_normsp_1(A,B,E),C) ) ) ) ) ) ) ), file(normsp_1,d8_normsp_1), [interesting(0.00)]). fof(t33_bhsp_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) & v2_bhsp_1(B) & l1_bhsp_1(B) ) => ! [C] : ( m1_subset_1(C,u1_struct_0(B)) => k3_bhsp_1(B,k3_rlvect_1(B,C,A)) = k4_real_1(k18_complex1(A),k3_bhsp_1(B,C)) ) ) ) ), file(bhsp_1,t33_bhsp_1), [interesting(0.00)]). fof(t13_seq_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( ( v1_funct_1(B) & v1_funct_2(B,k5_numbers,k1_numbers) & m2_relset_1(B,k5_numbers,k1_numbers) ) => ! [C] : ( ( v1_funct_1(C) & v1_funct_2(C,k5_numbers,k1_numbers) & m2_relset_1(C,k5_numbers,k1_numbers) ) => ( B = k14_seq_1(C,A) <=> ! [D] : ( m2_subset_1(D,k1_numbers,k5_numbers) => k2_seq_1(k5_numbers,k1_numbers,B,D) = k3_xcmplx_0(A,k2_seq_1(k5_numbers,k1_numbers,C,D)) ) ) ) ) ) ), file(seq_1,t13_seq_1), [interesting(0.00)]). fof(t28_bhsp_4,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) & v2_bhsp_1(A) & l1_bhsp_1(A) ) => ! [B] : ( m1_subset_1(B,k1_numbers) => ! [C] : ( ( v1_funct_1(C) & v1_funct_2(C,k5_numbers,u1_struct_0(A)) & m2_relset_1(C,k5_numbers,u1_struct_0(A)) ) => ( v2_bhsp_4(C,A) => v2_bhsp_4(k6_normsp_1(A,C,B),A) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d8_bhsp_4,t13_series_1,d3_bhsp_2,t34_bhsp_1,d3_bhsp_2,d8_normsp_1,t33_bhsp_1,d3_bhsp_2,t13_seq_1,t24_series_1,d8_bhsp_4]), [file(bhsp_4,t28_bhsp_4),interesting(0.00)]). fof(t29_bhsp_4,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) & v2_bhsp_1(A) & l1_bhsp_1(A) ) => ! [B] : ( ( v1_funct_1(B) & v1_funct_2(B,k5_numbers,u1_struct_0(A)) & m2_relset_1(B,k5_numbers,u1_struct_0(A)) ) => ! [C] : ( ( v1_funct_1(C) & v1_funct_2(C,k5_numbers,k1_numbers) & m2_relset_1(C,k5_numbers,k1_numbers) ) => ( ( ! [D] : ( m2_subset_1(D,k1_numbers,k5_numbers) => r1_xreal_0(k2_seq_1(k5_numbers,k1_numbers,k2_bhsp_2(A,B),D),k2_seq_1(k5_numbers,k1_numbers,C,D)) ) & v1_series_1(C) ) => v2_bhsp_4(B,A) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d3_bhsp_2,t34_bhsp_1,t24_series_1,d8_bhsp_4]), [file(bhsp_4,t29_bhsp_4),interesting(0.00)]). fof(t32_bhsp_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) & v2_bhsp_1(A) & l1_bhsp_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ( k3_bhsp_1(A,B) = 0 <=> B = k1_rlvect_1(A) ) ) ) ), file(bhsp_1,t32_bhsp_1), [interesting(0.00)]). fof(t30_series_1,theorem,( ! [A] : ( ( v1_funct_1(A) & v1_funct_2(A,k5_numbers,k1_numbers) & m2_relset_1(A,k5_numbers,k1_numbers) ) => ! [B] : ( ( v1_funct_1(B) & v1_funct_2(B,k5_numbers,k1_numbers) & m2_relset_1(B,k5_numbers,k1_numbers) ) => ( ( ! [C] : ( m2_subset_1(C,k1_numbers,k5_numbers) => ( ~ r1_xreal_0(k8_funct_2(k5_numbers,k1_numbers,A,C),0) & k8_funct_2(k5_numbers,k1_numbers,B,C) = k6_real_1(k8_funct_2(k5_numbers,k1_numbers,A,k1_nat_1(C,1)),k8_funct_2(k5_numbers,k1_numbers,A,C)) ) ) & v4_seq_2(B) ) => ( r1_xreal_0(1,k2_seq_2(B)) | v1_series_1(A) ) ) ) ) ), file(series_1,t30_series_1), [interesting(0.00)]). fof(t30_bhsp_4,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) & v2_bhsp_1(A) & l1_bhsp_1(A) ) => ! [B] : ( ( v1_funct_1(B) & v1_funct_2(B,k5_numbers,u1_struct_0(A)) & m2_relset_1(B,k5_numbers,u1_struct_0(A)) ) => ! [C] : ( ( v1_funct_1(C) & v1_funct_2(C,k5_numbers,k1_numbers) & m2_relset_1(C,k5_numbers,k1_numbers) ) => ( ( ! [D] : ( m2_subset_1(D,k1_numbers,k5_numbers) => ( k2_normsp_1(A,B,D) != k1_rlvect_1(A) & k2_seq_1(k5_numbers,k1_numbers,C,D) = k6_real_1(k3_bhsp_1(A,k2_normsp_1(A,B,k1_nat_1(D,1))),k3_bhsp_1(A,k2_normsp_1(A,B,D))) ) ) & v4_seq_2(C) ) => ( r1_xreal_0(1,k2_seq_2(C)) | v2_bhsp_4(B,A) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t32_bhsp_1,t34_bhsp_1,d3_bhsp_2,d3_bhsp_2,d3_bhsp_2,t30_series_1,d8_bhsp_4]), [file(bhsp_4,t30_bhsp_4),interesting(0.00)]). fof(t52_xreal_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ~ ( ~ r1_xreal_0(B,A) & r1_xreal_0(k6_xcmplx_0(B,A),0) ) ) ) ), file(xreal_1,t52_xreal_1), [interesting(0.00)]). fof(d7_seq_2,definition,( ! [A] : ( ( v1_funct_1(A) & v1_funct_2(A,k5_numbers,k1_numbers) & m2_relset_1(A,k5_numbers,k1_numbers) ) => ( v4_seq_2(A) => ! [B] : ( v1_xreal_0(B) => ( B = k1_seq_2(A) <=> ! [C] : ( v1_xreal_0(C) => ~ ( ~ r1_xreal_0(C,0) & ! [D] : ( m2_subset_1(D,k1_numbers,k5_numbers) => ? [E] : ( m2_subset_1(E,k1_numbers,k5_numbers) & r1_xreal_0(D,E) & r1_xreal_0(C,k18_complex1(k6_xcmplx_0(k2_seq_1(k5_numbers,k1_numbers,A,E),B))) ) ) ) ) ) ) ) ) ), file(seq_2,d7_seq_2), [interesting(0.00)]). fof(t29_nat_1,theorem,( ! [A] : ( v4_ordinal2(A) => ! [B] : ( v4_ordinal2(B) => r1_xreal_0(A,k2_xcmplx_0(A,B)) ) ) ), file(nat_1,t29_nat_1), [interesting(0.00)]). fof(t2_xreal_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ! [C] : ( v1_xreal_0(C) => ( ( r1_xreal_0(A,B) & r1_xreal_0(B,C) ) => r1_xreal_0(A,C) ) ) ) ) ), file(xreal_1,t2_xreal_1), [interesting(0.00)]). fof(t9_seq_2,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ( ( ~ r1_xreal_0(B,k4_xcmplx_0(A)) & ~ r1_xreal_0(A,B) ) <=> ~ r1_xreal_0(A,k18_complex1(B)) ) ) ) ), file(seq_2,t9_seq_2), [interesting(0.00)]). fof(t8_xreal_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ! [C] : ( v1_xreal_0(C) => ( r1_xreal_0(A,B) <=> r1_xreal_0(k2_xcmplx_0(A,C),k2_xcmplx_0(B,C)) ) ) ) ) ), file(xreal_1,t8_xreal_1), [interesting(0.00)]). fof(t118_real_2,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ( ~ r1_xreal_0(A,0) => ( ( r1_xreal_0(1,k7_xcmplx_0(B,A)) => r1_xreal_0(A,B) ) & ( r1_xreal_0(k7_xcmplx_0(B,A),1) => r1_xreal_0(B,A) ) & ( r1_xreal_0(k4_xcmplx_0(1),k7_xcmplx_0(B,A)) => ( r1_xreal_0(k4_xcmplx_0(A),B) & r1_xreal_0(k4_xcmplx_0(B),A) ) ) & ( r1_xreal_0(k7_xcmplx_0(B,A),k4_xcmplx_0(1)) => ( r1_xreal_0(B,k4_xcmplx_0(A)) & r1_xreal_0(A,k4_xcmplx_0(B)) ) ) ) ) ) ) ), file(real_2,t118_real_2), [interesting(0.00)]). fof(t28_nat_1,theorem,( ! [A] : ( v4_ordinal2(A) => ! [B] : ( v4_ordinal2(B) => ~ ( r1_xreal_0(A,B) & ! [C] : ( m2_subset_1(C,k1_numbers,k5_numbers) => B != k2_xcmplx_0(A,C) ) ) ) ) ), file(nat_1,t28_nat_1), [interesting(0.00)]). fof(t19_bhsp_2,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) & v2_bhsp_1(A) & l1_bhsp_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( ( v1_funct_1(C) & v1_funct_2(C,k5_numbers,u1_struct_0(A)) & m2_relset_1(C,k5_numbers,u1_struct_0(A)) ) => ( v1_bhsp_2(C,A) => ( k1_bhsp_2(A,C) = B <=> ! [D] : ( m1_subset_1(D,k1_numbers) => ~ ( ~ r1_xreal_0(D,0) & ! [E] : ( m2_subset_1(E,k1_numbers,k5_numbers) => ? [F] : ( m2_subset_1(F,k1_numbers,k5_numbers) & r1_xreal_0(E,F) & r1_xreal_0(D,k3_bhsp_1(A,k6_rlvect_1(A,k2_normsp_1(A,C,F),B))) ) ) ) ) ) ) ) ) ) ), file(bhsp_2,t19_bhsp_2), [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(t31_bhsp_4,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) & v2_bhsp_1(A) & l1_bhsp_1(A) ) => ! [B] : ( m1_subset_1(B,k1_numbers) => ! [C] : ( ( v1_funct_1(C) & v1_funct_2(C,k5_numbers,u1_struct_0(A)) & m2_relset_1(C,k5_numbers,u1_struct_0(A)) ) => ~ ( ~ r1_xreal_0(B,0) & ? [D] : ( m2_subset_1(D,k1_numbers,k5_numbers) & ! [E] : ( m2_subset_1(E,k1_numbers,k5_numbers) => ( r1_xreal_0(D,E) => r1_xreal_0(B,k3_bhsp_1(A,k2_normsp_1(A,C,E))) ) ) ) & v1_bhsp_2(C,A) & k1_bhsp_2(A,C) = k1_rlvect_1(A) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t19_bhsp_2,t29_nat_1,t2_xreal_1,t29_nat_1,t2_xreal_1,t26_rlvect_1]), [file(bhsp_4,t31_bhsp_4),interesting(0.00)]). fof(t14_bhsp_2,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) & v2_bhsp_1(A) & l1_bhsp_1(A) ) => ! [B] : ( ( v1_funct_1(B) & v1_funct_2(B,k5_numbers,u1_struct_0(A)) & m2_relset_1(B,k5_numbers,u1_struct_0(A)) ) => ! [C] : ( ( v1_funct_1(C) & v1_funct_2(C,k5_numbers,u1_struct_0(A)) & m2_relset_1(C,k5_numbers,u1_struct_0(A)) ) => ( ( v1_bhsp_2(B,A) & v1_bhsp_2(C,A) ) => k1_bhsp_2(A,k4_normsp_1(A,B,C)) = k6_rlvect_1(A,k1_bhsp_2(A,B),k1_bhsp_2(A,C)) ) ) ) ) ), file(bhsp_2,t14_bhsp_2), [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(t83_bhsp_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) & v2_bhsp_1(A) & l1_bhsp_1(A) ) => ! [B] : ( ( v1_funct_1(B) & v1_funct_2(B,k5_numbers,u1_struct_0(A)) & m2_relset_1(B,k5_numbers,u1_struct_0(A)) ) => ! [C] : ( ( v1_funct_1(C) & v1_funct_2(C,k5_numbers,u1_struct_0(A)) & m2_relset_1(C,k5_numbers,u1_struct_0(A)) ) => ! [D] : ( ( v1_funct_1(D) & v1_funct_2(D,k5_numbers,u1_struct_0(A)) & m2_relset_1(D,k5_numbers,u1_struct_0(A)) ) => k4_normsp_1(A,k8_bhsp_1(A,B,C),D) = k8_bhsp_1(A,B,k4_normsp_1(A,C,D)) ) ) ) ) ), file(bhsp_1,t83_bhsp_1), [interesting(0.00)]). fof(t43_bhsp_3,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) & v2_bhsp_1(A) & l1_bhsp_1(A) ) => ! [B] : ( ( v1_funct_1(B) & v1_funct_2(B,k5_numbers,u1_struct_0(A)) & m2_relset_1(B,k5_numbers,u1_struct_0(A)) ) => ! [C] : ( m2_subset_1(C,k1_numbers,k5_numbers) => m1_bhsp_3(k2_bhsp_3(A,B,C),A,B) ) ) ) ), file(bhsp_3,t43_bhsp_3), [interesting(0.00)]). fof(t33_bhsp_3,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) & v2_bhsp_1(A) & l1_bhsp_1(A) ) => ! [B] : ( ( v1_funct_1(B) & v1_funct_2(B,k5_numbers,u1_struct_0(A)) & m2_relset_1(B,k5_numbers,u1_struct_0(A)) ) => ! [C] : ( ( v1_funct_1(C) & v1_funct_2(C,k5_numbers,u1_struct_0(A)) & m2_relset_1(C,k5_numbers,u1_struct_0(A)) ) => ( ( m1_bhsp_3(B,A,C) & v1_bhsp_2(C,A) ) => k1_bhsp_2(A,B) = k1_bhsp_2(A,C) ) ) ) ) ), file(bhsp_3,t33_bhsp_3), [interesting(0.00)]). fof(t32_series_1,theorem,( ! [A] : ( ( v1_funct_1(A) & v1_funct_2(A,k5_numbers,k1_numbers) & m2_relset_1(A,k5_numbers,k1_numbers) ) => ! [B] : ( ( v1_funct_1(B) & v1_funct_2(B,k5_numbers,k1_numbers) & m2_relset_1(B,k5_numbers,k1_numbers) ) => ( ( ! [C] : ( m2_subset_1(C,k1_numbers,k5_numbers) => ( r1_xreal_0(0,k8_funct_2(k5_numbers,k1_numbers,A,C)) & k8_funct_2(k5_numbers,k1_numbers,B,C) = k2_power(C,k8_funct_2(k5_numbers,k1_numbers,A,C)) ) ) & v4_seq_2(B) ) => ( r1_xreal_0(1,k2_seq_2(B)) | v1_series_1(A) ) ) ) ) ), file(series_1,t32_series_1), [interesting(0.00)]). fof(t34_bhsp_4,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) & v2_bhsp_1(A) & l1_bhsp_1(A) ) => ! [B] : ( ( v1_funct_1(B) & v1_funct_2(B,k5_numbers,u1_struct_0(A)) & m2_relset_1(B,k5_numbers,u1_struct_0(A)) ) => ! [C] : ( ( v1_funct_1(C) & v1_funct_2(C,k5_numbers,k1_numbers) & m2_relset_1(C,k5_numbers,k1_numbers) ) => ( ( ! [D] : ( m2_subset_1(D,k1_numbers,k5_numbers) => k2_seq_1(k5_numbers,k1_numbers,C,D) = k2_power(D,k3_bhsp_1(A,k2_normsp_1(A,B,D))) ) & v4_seq_2(C) ) => ( r1_xreal_0(1,k2_seq_2(C)) | v2_bhsp_4(B,A) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d3_bhsp_2,t34_bhsp_1,d3_bhsp_2,t32_series_1,d8_bhsp_4]), [file(bhsp_4,t34_bhsp_4),interesting(0.00)]). fof(t19_prepower,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v4_ordinal2(B) => ( r1_xreal_0(1,A) => r1_xreal_0(1,k2_newton(A,B)) ) ) ) ), file(prepower,t19_prepower), [interesting(0.00)]). fof(t5_power,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( m2_subset_1(B,k1_numbers,k5_numbers) => ( ~ ( ~ ( r1_xreal_0(1,B) & r1_xreal_0(0,A) ) & ! [C] : ( m2_subset_1(C,k1_numbers,k5_numbers) => B != k1_nat_1(k2_nat_1(2,C),1) ) ) => ( k2_newton(k1_power(B,A),B) = A & k1_power(B,k2_newton(A,B)) = A ) ) ) ) ), file(power,t5_power), [interesting(0.00)]). fof(d1_series_1,definition,( ! [A] : ( ( v1_funct_1(A) & v1_funct_2(A,k5_numbers,k1_numbers) & m2_relset_1(A,k5_numbers,k1_numbers) ) => ! [B] : ( ( v1_funct_1(B) & v1_funct_2(B,k5_numbers,k1_numbers) & m2_relset_1(B,k5_numbers,k1_numbers) ) => ( B = k1_series_1(A) <=> ( k8_funct_2(k5_numbers,k1_numbers,B,0) = k8_funct_2(k5_numbers,k1_numbers,A,0) & ! [C] : ( m2_subset_1(C,k1_numbers,k5_numbers) => k8_funct_2(k5_numbers,k1_numbers,B,k1_nat_1(C,1)) = k3_real_1(k8_funct_2(k5_numbers,k1_numbers,B,C),k8_funct_2(k5_numbers,k1_numbers,A,k1_nat_1(C,1))) ) ) ) ) ) ), file(series_1,d1_series_1), [interesting(0.00)]). fof(d13_seqm_3,definition,( ! [A] : ( ( v1_funct_1(A) & v1_funct_2(A,k5_numbers,k1_numbers) & m2_relset_1(A,k5_numbers,k1_numbers) ) => ( v3_seqm_3(A) <=> ! [B] : ( m2_subset_1(B,k1_numbers,k5_numbers) => r1_xreal_0(k2_seq_1(k5_numbers,k1_numbers,A,B),k2_seq_1(k5_numbers,k1_numbers,A,k1_nat_1(B,1))) ) ) ) ), file(seqm_3,d13_seqm_3), [interesting(0.00)]). fof(t37_bhsp_4,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) & v2_bhsp_1(A) & l1_bhsp_1(A) ) => ! [B] : ( ( v1_funct_1(B) & v1_funct_2(B,k5_numbers,u1_struct_0(A)) & m2_relset_1(B,k5_numbers,u1_struct_0(A)) ) => v3_seqm_3(k1_series_1(k2_bhsp_2(A,B))) ) ) ), inference(mizar_proof,[status(thm)],[t34_bhsp_1,d3_bhsp_2,t8_xreal_1,d1_series_1,d13_seqm_3]), [file(bhsp_4,t37_bhsp_4),interesting(0.00)]). fof(t21_seqm_3,theorem,( ! [A] : ( ( v1_funct_1(A) & v1_funct_2(A,k5_numbers,k1_numbers) & m2_relset_1(A,k5_numbers,k1_numbers) ) => ( v3_seqm_3(A) => ! [B] : ( m2_subset_1(B,k1_numbers,k5_numbers) => r1_xreal_0(k2_seq_1(k5_numbers,k1_numbers,A,0),k2_seq_1(k5_numbers,k1_numbers,A,B)) ) ) ) ), file(seqm_3,t21_seqm_3), [interesting(0.00)]). fof(t38_bhsp_4,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) & v2_bhsp_1(A) & l1_bhsp_1(A) ) => ! [B] : ( ( v1_funct_1(B) & v1_funct_2(B,k5_numbers,u1_struct_0(A)) & m2_relset_1(B,k5_numbers,u1_struct_0(A)) ) => ! [C] : ( m2_subset_1(C,k1_numbers,k5_numbers) => r1_xreal_0(0,k2_seq_1(k5_numbers,k1_numbers,k1_series_1(k2_bhsp_2(A,B)),C)) ) ) ) ), inference(mizar_proof,[status(thm)],[t37_bhsp_4,t21_seqm_3,t34_bhsp_1,d3_bhsp_2,d1_series_1]), [file(bhsp_4,t38_bhsp_4),interesting(0.00)]). fof(t40_bhsp_4,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) & v2_bhsp_1(A) & l1_bhsp_1(A) ) => ! [B] : ( ( v1_funct_1(B) & v1_funct_2(B,k5_numbers,u1_struct_0(A)) & m2_relset_1(B,k5_numbers,u1_struct_0(A)) ) => ! [C] : ( m2_subset_1(C,k1_numbers,k5_numbers) => r1_xreal_0(k3_bhsp_1(A,k3_bhsp_4(A,B,C)),k5_bhsp_4(k2_bhsp_2(A,B),C)) ) ) ) ), inference(mizar_proof,[status(thm)],[t39_bhsp_4]), [file(bhsp_4,t40_bhsp_4),interesting(0.00)]). fof(t132_complex1,theorem,( ! [A] : ( v1_xcmplx_0(A) => r1_xreal_0(0,k17_complex1(A)) ) ), file(complex1,t132_complex1), [interesting(0.00)]). fof(t9_xreal_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ! [C] : ( v1_xreal_0(C) => ! [D] : ( v1_xreal_0(D) => ( ( r1_xreal_0(A,B) & r1_xreal_0(C,D) ) => r1_xreal_0(k2_xcmplx_0(A,C),k2_xcmplx_0(B,D)) ) ) ) ) ) ), file(xreal_1,t9_xreal_1), [interesting(0.00)]). fof(t11_seqm_3,theorem,( ! [A] : ( ( v1_funct_1(A) & v1_funct_2(A,k5_numbers,k1_numbers) & m2_relset_1(A,k5_numbers,k1_numbers) ) => ( v3_seqm_3(A) <=> ! [B] : ( m2_subset_1(B,k1_numbers,k5_numbers) => ! [C] : ( m2_subset_1(C,k1_numbers,k5_numbers) => r1_xreal_0(k2_seq_1(k5_numbers,k1_numbers,A,B),k2_seq_1(k5_numbers,k1_numbers,A,k1_nat_1(B,C))) ) ) ) ) ), file(seqm_3,t11_seqm_3), [interesting(0.00)]). fof(t50_xreal_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ( r1_xreal_0(A,B) => r1_xreal_0(0,k6_xcmplx_0(B,A)) ) ) ) ), file(xreal_1,t50_xreal_1), [interesting(0.00)]). fof(d1_absvalue,definition,( ! [A] : ( v1_xreal_0(A) => ( ( r1_xreal_0(0,A) => k16_complex1(A) = A ) & ( ~ r1_xreal_0(0,A) => k16_complex1(A) = k4_xcmplx_0(A) ) ) ) ), file(absvalue,d1_absvalue), [interesting(0.00)]). fof(t18_int_1,theorem,( ! [A] : ( v1_int_1(A) => ! [B] : ( v1_int_1(B) => ( r1_xreal_0(A,B) => r2_hidden(k6_xcmplx_0(B,A),k5_numbers) ) ) ) ), file(int_1,t18_int_1), [interesting(0.00)]). fof(t41_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)) => k6_rlvect_1(A,B,k2_rlvect_1(A,C,D)) = k6_rlvect_1(A,k6_rlvect_1(A,B,D),C) ) ) ) ) ), file(rlvect_1,t41_rlvect_1), [interesting(0.00)]). fof(t37_bhsp_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) & v2_bhsp_1(A) & l1_bhsp_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => k3_bhsp_1(A,k5_rlvect_1(A,B)) = k3_bhsp_1(A,B) ) ) ), file(bhsp_1,t37_bhsp_1), [interesting(0.00)]). fof(t138_complex1,theorem,( ! [A] : ( v1_xcmplx_0(A) => k17_complex1(k4_xcmplx_0(A)) = k17_complex1(A) ) ), file(complex1,t138_complex1), [interesting(0.00)]). fof(t3_seq_2,theorem,( ! [A] : ( v1_xreal_0(A) => ( ~ r1_xreal_0(A,0) => ( ~ r1_xreal_0(k7_xcmplx_0(A,2),0) & ~ r1_xreal_0(k7_xcmplx_0(A,4),0) ) ) ) ), file(seq_2,t3_seq_2), [interesting(0.00)]). fof(t25_series_1,theorem,( ! [A] : ( ( v1_funct_1(A) & v1_funct_2(A,k5_numbers,k1_numbers) & m2_relset_1(A,k5_numbers,k1_numbers) ) => ( v1_series_1(A) <=> ! [B] : ( v1_xreal_0(B) => ~ ( ~ r1_xreal_0(B,0) & ! [C] : ( m2_subset_1(C,k1_numbers,k5_numbers) => ? [D] : ( m2_subset_1(D,k1_numbers,k5_numbers) & r1_xreal_0(C,D) & r1_xreal_0(B,k18_complex1(k5_real_1(k8_funct_2(k5_numbers,k1_numbers,k1_series_1(A),D),k8_funct_2(k5_numbers,k1_numbers,k1_series_1(A),C)))) ) ) ) ) ) ) ), file(series_1,t25_series_1), [interesting(0.00)]). fof(t143_complex1,theorem,( ! [A] : ( v1_xcmplx_0(A) => ! [B] : ( v1_xcmplx_0(B) => r1_xreal_0(k17_complex1(k6_xcmplx_0(A,B)),k3_real_1(k17_complex1(A),k17_complex1(B))) ) ) ), file(complex1,t143_complex1), [interesting(0.00)]). fof(t10_xreal_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ! [C] : ( v1_xreal_0(C) => ! [D] : ( v1_xreal_0(D) => ~ ( ~ r1_xreal_0(B,A) & r1_xreal_0(C,D) & r1_xreal_0(k2_xcmplx_0(B,D),k2_xcmplx_0(A,C)) ) ) ) ) ) ), file(xreal_1,t10_xreal_1), [interesting(0.00)]). fof(d9_bhsp_4,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) & v2_bhsp_1(A) & l1_bhsp_1(A) ) => ! [B] : ( ( v1_funct_1(B) & v1_funct_2(B,k5_numbers,u1_struct_0(A)) & m2_relset_1(B,k5_numbers,u1_struct_0(A)) ) => ! [C] : ( ( v1_funct_1(C) & v1_funct_2(C,k5_numbers,k1_numbers) & m2_relset_1(C,k5_numbers,k1_numbers) ) => ! [D] : ( ( v1_funct_1(D) & v1_funct_2(D,k5_numbers,u1_struct_0(A)) & m2_relset_1(D,k5_numbers,u1_struct_0(A)) ) => ( D = k7_bhsp_4(A,B,C) <=> ! [E] : ( m2_subset_1(E,k1_numbers,k5_numbers) => k2_normsp_1(A,D,E) = k3_rlvect_1(A,k2_normsp_1(A,B,E),k2_seq_1(k5_numbers,k1_numbers,C,E)) ) ) ) ) ) ) ), file(bhsp_4,d9_bhsp_4), [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(t45_bhsp_4,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) & v2_bhsp_1(A) & l1_bhsp_1(A) ) => ! [B] : ( ( v1_funct_1(B) & v1_funct_2(B,k5_numbers,u1_struct_0(A)) & m2_relset_1(B,k5_numbers,u1_struct_0(A)) ) => ! [C] : ( ( v1_funct_1(C) & v1_funct_2(C,k5_numbers,u1_struct_0(A)) & m2_relset_1(C,k5_numbers,u1_struct_0(A)) ) => ! [D] : ( ( v1_funct_1(D) & v1_funct_2(D,k5_numbers,k1_numbers) & m2_relset_1(D,k5_numbers,k1_numbers) ) => k7_bhsp_4(A,k8_bhsp_1(A,B,C),D) = k8_bhsp_1(A,k7_bhsp_4(A,B,D),k7_bhsp_4(A,C,D)) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d9_bhsp_4,d5_normsp_1,d9_rlvect_1,d9_bhsp_4,d9_bhsp_4,d5_normsp_1,t113_funct_2]), [file(bhsp_4,t45_bhsp_4),interesting(0.00)]). fof(t46_bhsp_4,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) & v2_bhsp_1(A) & l1_bhsp_1(A) ) => ! [B] : ( ( v1_funct_1(B) & v1_funct_2(B,k5_numbers,u1_struct_0(A)) & m2_relset_1(B,k5_numbers,u1_struct_0(A)) ) => ! [C] : ( ( v1_funct_1(C) & v1_funct_2(C,k5_numbers,k1_numbers) & m2_relset_1(C,k5_numbers,k1_numbers) ) => ! [D] : ( ( v1_funct_1(D) & v1_funct_2(D,k5_numbers,k1_numbers) & m2_relset_1(D,k5_numbers,k1_numbers) ) => k7_bhsp_4(A,B,k9_seq_1(C,D)) = k8_bhsp_1(A,k7_bhsp_4(A,B,C),k7_bhsp_4(A,B,D)) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d9_bhsp_4,t11_seq_1,d9_rlvect_1,d9_bhsp_4,d9_bhsp_4,d5_normsp_1,t113_funct_2]), [file(bhsp_4,t46_bhsp_4),interesting(0.00)]). fof(t12_seq_1,theorem,( ! [A] : ( ( v1_funct_1(A) & v1_funct_2(A,k5_numbers,k1_numbers) & m2_relset_1(A,k5_numbers,k1_numbers) ) => ! [B] : ( ( v1_funct_1(B) & v1_funct_2(B,k5_numbers,k1_numbers) & m2_relset_1(B,k5_numbers,k1_numbers) ) => ! [C] : ( ( v1_funct_1(C) & v1_funct_2(C,k5_numbers,k1_numbers) & m2_relset_1(C,k5_numbers,k1_numbers) ) => ( A = k8_seq_1(k5_numbers,k1_numbers,B,C) <=> ! [D] : ( m2_subset_1(D,k1_numbers,k5_numbers) => k2_seq_1(k5_numbers,k1_numbers,A,D) = k4_real_1(k2_seq_1(k5_numbers,k1_numbers,B,D),k2_seq_1(k5_numbers,k1_numbers,C,D)) ) ) ) ) ) ), file(seq_1,t12_seq_1), [interesting(0.00)]). fof(t47_bhsp_4,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) & v2_bhsp_1(A) & l1_bhsp_1(A) ) => ! [B] : ( ( v1_funct_1(B) & v1_funct_2(B,k5_numbers,u1_struct_0(A)) & m2_relset_1(B,k5_numbers,u1_struct_0(A)) ) => ! [C] : ( ( v1_funct_1(C) & v1_funct_2(C,k5_numbers,k1_numbers) & m2_relset_1(C,k5_numbers,k1_numbers) ) => ! [D] : ( ( v1_funct_1(D) & v1_funct_2(D,k5_numbers,k1_numbers) & m2_relset_1(D,k5_numbers,k1_numbers) ) => k7_bhsp_4(A,B,k11_seq_1(C,D)) = k7_bhsp_4(A,k7_bhsp_4(A,B,D),C) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d9_bhsp_4,t12_seq_1,d9_rlvect_1,d9_bhsp_4,d9_bhsp_4,t113_funct_2]), [file(bhsp_4,t47_bhsp_4),interesting(0.00)]). fof(d10_bhsp_1,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) & v2_bhsp_1(A) & l1_bhsp_1(A) ) => ! [B] : ( ( v1_funct_1(B) & v1_funct_2(B,k5_numbers,u1_struct_0(A)) & m2_relset_1(B,k5_numbers,u1_struct_0(A)) ) => ! [C] : ( ( v1_funct_1(C) & v1_funct_2(C,k5_numbers,u1_struct_0(A)) & m2_relset_1(C,k5_numbers,u1_struct_0(A)) ) => ( C = k6_bhsp_1(A,B) <=> ! [D] : ( m2_subset_1(D,k1_numbers,k5_numbers) => k2_normsp_1(A,C,D) = k5_rlvect_1(A,k2_normsp_1(A,B,D)) ) ) ) ) ) ), file(bhsp_1,d10_bhsp_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(t14_seq_1,theorem,( ! [A] : ( ( v1_funct_1(A) & v1_funct_2(A,k5_numbers,k1_numbers) & m2_relset_1(A,k5_numbers,k1_numbers) ) => ! [B] : ( ( v1_funct_1(B) & v1_funct_2(B,k5_numbers,k1_numbers) & m2_relset_1(B,k5_numbers,k1_numbers) ) => ( A = k17_seq_1(B) <=> ! [C] : ( m2_subset_1(C,k1_numbers,k5_numbers) => k2_seq_1(k5_numbers,k1_numbers,A,C) = k1_real_1(k2_seq_1(k5_numbers,k1_numbers,B,C)) ) ) ) ) ), file(seq_1,t14_seq_1), [interesting(0.00)]). fof(t49_bhsp_4,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) & v2_bhsp_1(A) & l1_bhsp_1(A) ) => ! [B] : ( ( v1_funct_1(B) & v1_funct_2(B,k5_numbers,u1_struct_0(A)) & m2_relset_1(B,k5_numbers,u1_struct_0(A)) ) => ! [C] : ( ( v1_funct_1(C) & v1_funct_2(C,k5_numbers,k1_numbers) & m2_relset_1(C,k5_numbers,k1_numbers) ) => k7_bhsp_4(A,k6_bhsp_1(A,B),C) = k7_bhsp_4(A,B,k17_seq_1(C)) ) ) ) ), inference(mizar_proof,[status(thm)],[d9_bhsp_4,d10_bhsp_1,t38_rlvect_1,t14_seq_1,d9_bhsp_4,t113_funct_2]), [file(bhsp_4,t49_bhsp_4),interesting(0.00)]). fof(t3_bhsp_4,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) & v2_bhsp_1(A) & l1_bhsp_1(A) ) => ! [B] : ( m1_subset_1(B,k1_numbers) => ! [C] : ( ( v1_funct_1(C) & v1_funct_2(C,k5_numbers,u1_struct_0(A)) & m2_relset_1(C,k5_numbers,u1_struct_0(A)) ) => k1_bhsp_4(A,k6_normsp_1(A,C,B)) = k6_normsp_1(A,k1_bhsp_4(A,C),B) ) ) ) ), inference(mizar_proof,[status(thm)],[d8_normsp_1,d1_bhsp_4,d8_normsp_1,d8_normsp_1,d1_bhsp_4,d9_rlvect_1,d8_normsp_1,d8_normsp_1,d1_bhsp_4]), [file(bhsp_4,t3_bhsp_4),interesting(0.00)]). fof(t77_bhsp_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) & v2_bhsp_1(A) & l1_bhsp_1(A) ) => ! [B] : ( ( v1_funct_1(B) & v1_funct_2(B,k5_numbers,u1_struct_0(A)) & m2_relset_1(B,k5_numbers,u1_struct_0(A)) ) => k6_normsp_1(A,B,k1_real_1(1)) = k6_bhsp_1(A,B) ) ) ), file(bhsp_1,t77_bhsp_1), [interesting(0.00)]). fof(t4_bhsp_4,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) & v2_bhsp_1(A) & l1_bhsp_1(A) ) => ! [B] : ( ( v1_funct_1(B) & v1_funct_2(B,k5_numbers,u1_struct_0(A)) & m2_relset_1(B,k5_numbers,u1_struct_0(A)) ) => k1_bhsp_4(A,k6_bhsp_1(A,B)) = k6_bhsp_1(A,k1_bhsp_4(A,B)) ) ) ), inference(mizar_proof,[status(thm)],[t3_bhsp_4,t77_bhsp_1,t77_bhsp_1]), [file(bhsp_4,t4_bhsp_4),interesting(0.00)]). fof(t15_seq_2,theorem,( ! [A] : ( ( v1_funct_1(A) & v1_funct_2(A,k5_numbers,k1_numbers) & m2_relset_1(A,k5_numbers,k1_numbers) ) => ( v3_seq_2(A) <=> ? [B] : ( v1_xreal_0(B) & ~ r1_xreal_0(B,0) & ! [C] : ( m2_subset_1(C,k1_numbers,k5_numbers) => ~ r1_xreal_0(B,k18_complex1(k2_seq_1(k5_numbers,k1_numbers,A,C))) ) ) ) ) ), file(seq_2,t15_seq_2), [interesting(0.00)]). fof(d3_bhsp_3,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) & v2_bhsp_1(A) & l1_bhsp_1(A) ) => ! [B] : ( ( v1_funct_1(B) & v1_funct_2(B,k5_numbers,u1_struct_0(A)) & m2_relset_1(B,k5_numbers,u1_struct_0(A)) ) => ( v2_bhsp_3(B,A) <=> ? [C] : ( m1_subset_1(C,k1_numbers) & ~ r1_xreal_0(C,0) & ! [D] : ( m2_subset_1(D,k1_numbers,k5_numbers) => r1_xreal_0(k3_bhsp_1(A,k2_normsp_1(A,B,D)),C) ) ) ) ) ) ), file(bhsp_3,d3_bhsp_3), [interesting(0.00)]). fof(d1_xreal_0,definition,( ! [A] : ( v1_xreal_0(A) <=> r2_hidden(A,k1_numbers) ) ), file(xreal_0,d1_xreal_0), [interesting(0.00)]). fof(t66_xreal_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ! [C] : ( v1_xreal_0(C) => ( ( r1_xreal_0(A,B) & r1_xreal_0(0,C) ) => r1_xreal_0(k3_xcmplx_0(A,C),k3_xcmplx_0(B,C)) ) ) ) ) ), file(xreal_1,t66_xreal_1), [interesting(0.00)]). fof(t122_real_2,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ~ ( ( ( ~ r1_xreal_0(0,A) & ~ r1_xreal_0(0,B) ) | ( ~ r1_xreal_0(A,0) & ~ r1_xreal_0(B,0) ) ) & r1_xreal_0(k3_xcmplx_0(A,B),0) ) ) ) ), file(real_2,t122_real_2), [interesting(0.00)]). fof(t51_bhsp_4,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) & v2_bhsp_1(A) & l1_bhsp_1(A) ) => ! [B] : ( ( v1_funct_1(B) & v1_funct_2(B,k5_numbers,u1_struct_0(A)) & m2_relset_1(B,k5_numbers,u1_struct_0(A)) ) => ! [C] : ( ( v1_funct_1(C) & v1_funct_2(C,k5_numbers,k1_numbers) & m2_relset_1(C,k5_numbers,k1_numbers) ) => ( ( v3_seq_2(C) & v2_bhsp_3(B,A) ) => v2_bhsp_3(k7_bhsp_4(A,B,C),A) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t15_seq_2,d3_bhsp_3,d1_xreal_0,t132_complex1,t66_xreal_1,t66_xreal_1,d9_bhsp_4,t33_bhsp_1,t2_xreal_1,t122_real_2,d3_bhsp_3]), [file(bhsp_4,t51_bhsp_4),interesting(0.00)]). fof(d6_seq_2,definition,( ! [A] : ( ( v1_funct_1(A) & v1_funct_2(A,k5_numbers,k1_numbers) & m2_relset_1(A,k5_numbers,k1_numbers) ) => ( v4_seq_2(A) <=> ? [B] : ( v1_xreal_0(B) & ! [C] : ( v1_xreal_0(C) => ~ ( ~ r1_xreal_0(C,0) & ! [D] : ( m2_subset_1(D,k1_numbers,k5_numbers) => ? [E] : ( m2_subset_1(E,k1_numbers,k5_numbers) & r1_xreal_0(D,E) & r1_xreal_0(C,k18_complex1(k6_xcmplx_0(k2_seq_1(k5_numbers,k1_numbers,A,E),B))) ) ) ) ) ) ) ) ), file(seq_2,d6_seq_2), [interesting(0.00)]). fof(t9_bhsp_2,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) & v2_bhsp_1(A) & l1_bhsp_1(A) ) => ! [B] : ( ( v1_funct_1(B) & v1_funct_2(B,k5_numbers,u1_struct_0(A)) & m2_relset_1(B,k5_numbers,u1_struct_0(A)) ) => ( v1_bhsp_2(B,A) <=> ? [C] : ( m1_subset_1(C,u1_struct_0(A)) & ! [D] : ( m1_subset_1(D,k1_numbers) => ~ ( ~ r1_xreal_0(D,0) & ! [E] : ( m2_subset_1(E,k1_numbers,k5_numbers) => ? [F] : ( m2_subset_1(F,k1_numbers,k5_numbers) & r1_xreal_0(E,F) & r1_xreal_0(D,k3_bhsp_1(A,k6_rlvect_1(A,k2_normsp_1(A,B,F),C))) ) ) ) ) ) ) ) ) ), file(bhsp_2,t9_bhsp_2), [interesting(0.00)]). fof(t27_seq_2,theorem,( ! [A] : ( ( v1_funct_1(A) & v1_funct_2(A,k5_numbers,k1_numbers) & m2_relset_1(A,k5_numbers,k1_numbers) ) => ( v4_seq_2(A) => v3_seq_2(A) ) ) ), file(seq_2,t27_seq_2), [interesting(0.00)]). fof(t127_real_2,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ~ ( ( ( ~ r1_xreal_0(A,0) & ~ r1_xreal_0(B,0) ) | ( ~ r1_xreal_0(0,A) & ~ r1_xreal_0(0,B) ) ) & r1_xreal_0(k7_xcmplx_0(A,B),0) ) ) ) ), file(real_2,t127_real_2), [interesting(0.00)]). fof(t37_nat_1,theorem,( ! [A] : ( v4_ordinal2(A) => ! [B] : ( v4_ordinal2(B) => ! [C] : ( v4_ordinal2(C) => ( r1_xreal_0(A,B) => r1_xreal_0(A,k2_xcmplx_0(B,C)) ) ) ) ) ), file(nat_1,t37_nat_1), [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(t47_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)) => k5_rlvect_1(A,k6_rlvect_1(A,B,C)) = k2_rlvect_1(A,C,k5_rlvect_1(A,B)) ) ) ) ), file(rlvect_1,t47_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(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(t98_xreal_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ! [C] : ( v1_xreal_0(C) => ! [D] : ( v1_xreal_0(D) => ~ ( r1_xreal_0(0,A) & r1_xreal_0(0,B) & ~ r1_xreal_0(C,A) & ~ r1_xreal_0(D,B) & r1_xreal_0(k3_xcmplx_0(C,D),k3_xcmplx_0(A,B)) ) ) ) ) ) ), file(xreal_1,t98_xreal_1), [interesting(0.00)]). fof(t75_xcmplx_1,theorem,( ! [A] : ( v1_xcmplx_0(A) => ! [B] : ( v1_xcmplx_0(B) => ! [C] : ( v1_xcmplx_0(C) => k3_xcmplx_0(A,k7_xcmplx_0(B,C)) = k7_xcmplx_0(k3_xcmplx_0(A,B),C) ) ) ) ), file(xcmplx_1,t75_xcmplx_1), [interesting(0.00)]). fof(t63_xcmplx_1,theorem,( ! [A] : ( v1_xcmplx_0(A) => ! [B] : ( v1_xcmplx_0(B) => ! [C] : ( v1_xcmplx_0(C) => k2_xcmplx_0(k7_xcmplx_0(A,B),k7_xcmplx_0(C,B)) = k7_xcmplx_0(k2_xcmplx_0(A,C),B) ) ) ) ), file(xcmplx_1,t63_xcmplx_1), [interesting(0.00)]). fof(t90_xcmplx_1,theorem,( ! [A] : ( v1_xcmplx_0(A) => ! [B] : ( v1_xcmplx_0(B) => ( A != 0 => B = k7_xcmplx_0(k3_xcmplx_0(B,A),A) ) ) ) ), file(xcmplx_1,t90_xcmplx_1), [interesting(0.00)]). fof(t50_bhsp_4,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) & v2_bhsp_1(A) & l1_bhsp_1(A) ) => ! [B] : ( ( v1_funct_1(B) & v1_funct_2(B,k5_numbers,u1_struct_0(A)) & m2_relset_1(B,k5_numbers,u1_struct_0(A)) ) => ! [C] : ( ( v1_funct_1(C) & v1_funct_2(C,k5_numbers,k1_numbers) & m2_relset_1(C,k5_numbers,k1_numbers) ) => ( ( v4_seq_2(C) & v1_bhsp_2(B,A) ) => v1_bhsp_2(k7_bhsp_4(A,B,C),A) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d6_seq_2,d1_xreal_0,t9_bhsp_2,t27_seq_2,t15_seq_2,d1_xreal_0,t34_bhsp_1,t10_xreal_1,t127_real_2,t37_nat_1,t2_xreal_1,t37_nat_1,t2_xreal_1,d9_bhsp_4,t10_rlvect_1,t28_rlvect_1,t43_rlvect_1,t43_rlvect_1,t41_rlvect_1,t47_rlvect_1,t36_bhsp_1,t48_rlvect_1,t49_rlvect_1,t33_bhsp_1,t33_bhsp_1,t132_complex1,t34_bhsp_1,t98_xreal_1,t66_xreal_1,t10_xreal_1,t75_xcmplx_1,t75_xcmplx_1,t63_xcmplx_1,t90_xcmplx_1,t2_xreal_1,t9_bhsp_2]), [file(bhsp_4,t50_bhsp_4),interesting(0.00)]). fof(d2_bhsp_2,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) & v2_bhsp_1(A) & l1_bhsp_1(A) ) => ! [B] : ( ( v1_funct_1(B) & v1_funct_2(B,k5_numbers,u1_struct_0(A)) & m2_relset_1(B,k5_numbers,u1_struct_0(A)) ) => ( v1_bhsp_2(B,A) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ( C = k1_bhsp_2(A,B) <=> ! [D] : ( m1_subset_1(D,k1_numbers) => ~ ( ~ r1_xreal_0(D,0) & ! [E] : ( m2_subset_1(E,k1_numbers,k5_numbers) => ? [F] : ( m2_subset_1(F,k1_numbers,k5_numbers) & r1_xreal_0(E,F) & r1_xreal_0(D,k5_bhsp_1(A,k2_normsp_1(A,B,F),C)) ) ) ) ) ) ) ) ) ) ), file(bhsp_2,d2_bhsp_2), [interesting(0.00)]). fof(d5_bhsp_1,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) & v2_bhsp_1(A) & l1_bhsp_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => k4_bhsp_1(A,B,C) = k3_bhsp_1(A,k6_rlvect_1(A,B,C)) ) ) ) ), file(bhsp_1,d5_bhsp_1), [interesting(0.00)]). fof(d10_bhsp_4,definition,( ! [A] : ( ( v1_funct_1(A) & v1_funct_2(A,k5_numbers,k1_numbers) & m2_relset_1(A,k5_numbers,k1_numbers) ) => ( v3_bhsp_4(A) <=> ! [B] : ( m1_subset_1(B,k1_numbers) => ~ ( ~ r1_xreal_0(B,0) & ! [C] : ( m2_subset_1(C,k1_numbers,k5_numbers) => ? [D] : ( m2_subset_1(D,k1_numbers,k5_numbers) & ? [E] : ( m2_subset_1(E,k1_numbers,k5_numbers) & r1_xreal_0(C,D) & r1_xreal_0(C,E) & r1_xreal_0(B,k18_complex1(k5_real_1(k2_seq_1(k5_numbers,k1_numbers,A,D),k2_seq_1(k5_numbers,k1_numbers,A,E)))) ) ) ) ) ) ) ) ), file(bhsp_4,d10_bhsp_4), [interesting(0.00)]). fof(t58_seq_4,theorem,( ! [A] : ( ( v1_funct_1(A) & v1_funct_2(A,k5_numbers,k1_numbers) & m2_relset_1(A,k5_numbers,k1_numbers) ) => ( v4_seq_2(A) <=> ! [B] : ( v1_xreal_0(B) => ~ ( ~ r1_xreal_0(B,0) & ! [C] : ( m2_subset_1(C,k1_numbers,k5_numbers) => ? [D] : ( m2_subset_1(D,k1_numbers,k5_numbers) & r1_xreal_0(C,D) & r1_xreal_0(B,k18_complex1(k5_real_1(k8_funct_2(k5_numbers,k1_numbers,A,D),k8_funct_2(k5_numbers,k1_numbers,A,C)))) ) ) ) ) ) ) ), file(seq_4,t58_seq_4), [interesting(0.00)]). fof(t15_seq_1,theorem,( ! [A] : ( ( v1_funct_1(A) & v1_funct_2(A,k5_numbers,k1_numbers) & m2_relset_1(A,k5_numbers,k1_numbers) ) => ! [B] : ( ( v1_funct_1(B) & v1_funct_2(B,k5_numbers,k1_numbers) & m2_relset_1(B,k5_numbers,k1_numbers) ) => k10_seq_1(A,B) = k9_seq_1(A,k17_seq_1(B)) ) ) ), file(seq_1,t15_seq_1), [interesting(0.00)]). fof(d9_seqm_3,definition,( ! [A] : ( ( v1_funct_1(A) & v1_funct_2(A,k5_numbers,k1_numbers) & m2_relset_1(A,k5_numbers,k1_numbers) ) => ! [B] : ( m2_subset_1(B,k1_numbers,k5_numbers) => ! [C] : ( ( v1_funct_1(C) & v1_funct_2(C,k5_numbers,k1_numbers) & m2_relset_1(C,k5_numbers,k1_numbers) ) => ( C = k1_seqm_3(A,B) <=> ! [D] : ( m2_subset_1(D,k1_numbers,k5_numbers) => k2_seq_1(k5_numbers,k1_numbers,C,D) = k2_seq_1(k5_numbers,k1_numbers,A,k1_nat_1(D,B)) ) ) ) ) ) ), file(seqm_3,d9_seqm_3), [interesting(0.00)]). fof(t37_seq_1,theorem,( ! [A] : ( ( v1_funct_1(A) & v1_funct_2(A,k5_numbers,k1_numbers) & m2_relset_1(A,k5_numbers,k1_numbers) ) => ! [B] : ( ( v1_funct_1(B) & v1_funct_2(B,k5_numbers,k1_numbers) & m2_relset_1(B,k5_numbers,k1_numbers) ) => k10_seq_1(A,k17_seq_1(B)) = k9_seq_1(A,B) ) ) ), file(seq_1,t37_seq_1), [interesting(0.00)]). fof(t25_seq_1,theorem,( ! [A] : ( ( v1_funct_1(A) & v1_funct_2(A,k5_numbers,k1_numbers) & m2_relset_1(A,k5_numbers,k1_numbers) ) => k17_seq_1(A) = k14_seq_1(A,k1_real_1(1)) ) ), file(seq_1,t25_seq_1), [interesting(0.00)]). fof(t32_seq_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( ( v1_funct_1(B) & v1_funct_2(B,k5_numbers,k1_numbers) & m2_relset_1(B,k5_numbers,k1_numbers) ) => ! [C] : ( ( v1_funct_1(C) & v1_funct_2(C,k5_numbers,k1_numbers) & m2_relset_1(C,k5_numbers,k1_numbers) ) => k14_seq_1(k10_seq_1(B,C),A) = k10_seq_1(k14_seq_1(B,A),k14_seq_1(C,A)) ) ) ) ), file(seq_1,t32_seq_1), [interesting(0.00)]). fof(t48_bhsp_4,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) & v2_bhsp_1(A) & l1_bhsp_1(A) ) => ! [B] : ( m1_subset_1(B,k1_numbers) => ! [C] : ( ( v1_funct_1(C) & v1_funct_2(C,k5_numbers,u1_struct_0(A)) & m2_relset_1(C,k5_numbers,u1_struct_0(A)) ) => ! [D] : ( ( v1_funct_1(D) & v1_funct_2(D,k5_numbers,k1_numbers) & m2_relset_1(D,k5_numbers,k1_numbers) ) => k7_bhsp_4(A,C,k14_seq_1(D,B)) = k6_normsp_1(A,k7_bhsp_4(A,C,D),B) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d9_bhsp_4,t13_seq_1,d9_rlvect_1,d9_bhsp_4,d8_normsp_1,t113_funct_2]), [file(bhsp_4,t48_bhsp_4),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(t1_bhsp_4,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) & v2_bhsp_1(A) & l1_bhsp_1(A) ) => ! [B] : ( ( v1_funct_1(B) & v1_funct_2(B,k5_numbers,u1_struct_0(A)) & m2_relset_1(B,k5_numbers,u1_struct_0(A)) ) => ! [C] : ( ( v1_funct_1(C) & v1_funct_2(C,k5_numbers,u1_struct_0(A)) & m2_relset_1(C,k5_numbers,u1_struct_0(A)) ) => k8_bhsp_1(A,k1_bhsp_4(A,B),k1_bhsp_4(A,C)) = k1_bhsp_4(A,k8_bhsp_1(A,B,C)) ) ) ) ), inference(mizar_proof,[status(thm)],[d5_normsp_1,d1_bhsp_4,d1_bhsp_4,d5_normsp_1,d5_normsp_1,d1_bhsp_4,d1_bhsp_4,d6_rlvect_1,d6_rlvect_1,d5_normsp_1,d6_rlvect_1,d5_normsp_1,d1_bhsp_4]), [file(bhsp_4,t1_bhsp_4),interesting(0.00)]). fof(t5_bhsp_4,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) & v2_bhsp_1(A) & l1_bhsp_1(A) ) => ! [B] : ( m1_subset_1(B,k1_numbers) => ! [C] : ( m1_subset_1(C,k1_numbers) => ! [D] : ( ( v1_funct_1(D) & v1_funct_2(D,k5_numbers,u1_struct_0(A)) & m2_relset_1(D,k5_numbers,u1_struct_0(A)) ) => ! [E] : ( ( v1_funct_1(E) & v1_funct_2(E,k5_numbers,u1_struct_0(A)) & m2_relset_1(E,k5_numbers,u1_struct_0(A)) ) => k8_bhsp_1(A,k6_normsp_1(A,k1_bhsp_4(A,D),B),k6_normsp_1(A,k1_bhsp_4(A,E),C)) = k1_bhsp_4(A,k8_bhsp_1(A,k6_normsp_1(A,D,B),k6_normsp_1(A,E,C))) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t3_bhsp_4,t3_bhsp_4,t1_bhsp_4]), [file(bhsp_4,t5_bhsp_4),interesting(0.00)]). fof(t13_bhsp_2,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) & v2_bhsp_1(A) & l1_bhsp_1(A) ) => ! [B] : ( ( v1_funct_1(B) & v1_funct_2(B,k5_numbers,u1_struct_0(A)) & m2_relset_1(B,k5_numbers,u1_struct_0(A)) ) => ! [C] : ( ( v1_funct_1(C) & v1_funct_2(C,k5_numbers,u1_struct_0(A)) & m2_relset_1(C,k5_numbers,u1_struct_0(A)) ) => ( ( v1_bhsp_2(B,A) & v1_bhsp_2(C,A) ) => k1_bhsp_2(A,k3_normsp_1(A,B,C)) = k4_rlvect_1(A,k1_bhsp_2(A,B),k1_bhsp_2(A,C)) ) ) ) ) ), file(bhsp_2,t13_bhsp_2), [interesting(0.00)]). fof(t6_bhsp_4,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) & v2_bhsp_1(A) & l1_bhsp_1(A) ) => ! [B] : ( ( v1_funct_1(B) & v1_funct_2(B,k5_numbers,u1_struct_0(A)) & m2_relset_1(B,k5_numbers,u1_struct_0(A)) ) => ! [C] : ( ( v1_funct_1(C) & v1_funct_2(C,k5_numbers,u1_struct_0(A)) & m2_relset_1(C,k5_numbers,u1_struct_0(A)) ) => ( ( v1_bhsp_4(B,A) & v1_bhsp_4(C,A) ) => ( v1_bhsp_4(k8_bhsp_1(A,B,C),A) & k2_bhsp_4(A,k8_bhsp_1(A,B,C)) = k4_rlvect_1(A,k2_bhsp_4(A,B),k2_bhsp_4(A,C)) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d2_bhsp_4,d2_bhsp_4,t3_bhsp_2,t1_bhsp_4,d2_bhsp_4,t1_bhsp_4,t13_bhsp_2]), [file(bhsp_4,t6_bhsp_4),interesting(0.00)]). fof(t2_bhsp_4,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) & v2_bhsp_1(A) & l1_bhsp_1(A) ) => ! [B] : ( ( v1_funct_1(B) & v1_funct_2(B,k5_numbers,u1_struct_0(A)) & m2_relset_1(B,k5_numbers,u1_struct_0(A)) ) => ! [C] : ( ( v1_funct_1(C) & v1_funct_2(C,k5_numbers,u1_struct_0(A)) & m2_relset_1(C,k5_numbers,u1_struct_0(A)) ) => k4_normsp_1(A,k1_bhsp_4(A,B),k1_bhsp_4(A,C)) = k1_bhsp_4(A,k4_normsp_1(A,B,C)) ) ) ) ), inference(mizar_proof,[status(thm)],[d6_normsp_1,d1_bhsp_4,d1_bhsp_4,d6_normsp_1,d6_normsp_1,d1_bhsp_4,d1_bhsp_4,t41_rlvect_1,d6_rlvect_1,d6_rlvect_1,d6_rlvect_1,d6_normsp_1,d6_normsp_1,d1_bhsp_4]), [file(bhsp_4,t2_bhsp_4),interesting(0.00)]). fof(t7_bhsp_4,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) & v2_bhsp_1(A) & l1_bhsp_1(A) ) => ! [B] : ( ( v1_funct_1(B) & v1_funct_2(B,k5_numbers,u1_struct_0(A)) & m2_relset_1(B,k5_numbers,u1_struct_0(A)) ) => ! [C] : ( ( v1_funct_1(C) & v1_funct_2(C,k5_numbers,u1_struct_0(A)) & m2_relset_1(C,k5_numbers,u1_struct_0(A)) ) => ( ( v1_bhsp_4(B,A) & v1_bhsp_4(C,A) ) => ( v1_bhsp_4(k4_normsp_1(A,B,C),A) & k2_bhsp_4(A,k4_normsp_1(A,B,C)) = k6_rlvect_1(A,k2_bhsp_4(A,B),k2_bhsp_4(A,C)) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d2_bhsp_4,d2_bhsp_4,t4_bhsp_2,t2_bhsp_4,d2_bhsp_4,t2_bhsp_4,t14_bhsp_2]), [file(bhsp_4,t7_bhsp_4),interesting(0.00)]). fof(t5_bhsp_2,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) & v2_bhsp_1(A) & l1_bhsp_1(A) ) => ! [B] : ( m1_subset_1(B,k1_numbers) => ! [C] : ( ( v1_funct_1(C) & v1_funct_2(C,k5_numbers,u1_struct_0(A)) & m2_relset_1(C,k5_numbers,u1_struct_0(A)) ) => ( v1_bhsp_2(C,A) => v1_bhsp_2(k6_normsp_1(A,C,B),A) ) ) ) ) ), file(bhsp_2,t5_bhsp_2), [interesting(0.00)]). fof(t15_bhsp_2,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) & v2_bhsp_1(A) & l1_bhsp_1(A) ) => ! [B] : ( m1_subset_1(B,k1_numbers) => ! [C] : ( ( v1_funct_1(C) & v1_funct_2(C,k5_numbers,u1_struct_0(A)) & m2_relset_1(C,k5_numbers,u1_struct_0(A)) ) => ( v1_bhsp_2(C,A) => k1_bhsp_2(A,k6_normsp_1(A,C,B)) = k3_rlvect_1(A,k1_bhsp_2(A,C),B) ) ) ) ) ), file(bhsp_2,t15_bhsp_2), [interesting(0.00)]). fof(t8_bhsp_4,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) & v2_bhsp_1(A) & l1_bhsp_1(A) ) => ! [B] : ( m1_subset_1(B,k1_numbers) => ! [C] : ( ( v1_funct_1(C) & v1_funct_2(C,k5_numbers,u1_struct_0(A)) & m2_relset_1(C,k5_numbers,u1_struct_0(A)) ) => ( v1_bhsp_4(C,A) => ( v1_bhsp_4(k6_normsp_1(A,C,B),A) & k2_bhsp_4(A,k6_normsp_1(A,C,B)) = k3_rlvect_1(A,k2_bhsp_4(A,C),B) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d2_bhsp_4,t5_bhsp_2,t3_bhsp_4,d2_bhsp_4,t3_bhsp_4,t15_bhsp_2]), [file(bhsp_4,t8_bhsp_4),interesting(0.00)]).