:: BHSP_2 semantic presentation begin definitionlet "X" be ($#l1_bhsp_1 :::"RealUnitarySpace":::); let "seq" be ($#m1_subset_1 :::"sequence":::) "of" (Set (Const "X")); attr "seq" is :::"convergent"::: means :: BHSP_2:def 1 (Bool "ex" (Set (Var "g")) "being" ($#m1_subset_1 :::"Point":::) "of" "X" "st" (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "r")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool "ex" (Set (Var "m")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "n")) ($#r1_xxreal_0 :::">="::: ) (Set (Var "m")))) "holds" (Bool (Set ($#k4_bhsp_1 :::"dist"::: ) "(" (Set "(" "seq" ($#k1_normsp_1 :::"."::: ) (Set (Var "n")) ")" ) "," (Set (Var "g")) ")" ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "r"))))))); end; :: deftheorem defines :::"convergent"::: BHSP_2:def 1 : (Bool "for" (Set (Var "X")) "being" ($#l1_bhsp_1 :::"RealUnitarySpace":::) (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "seq")) "is" ($#v1_bhsp_2 :::"convergent"::: ) ) "iff" (Bool "ex" (Set (Var "g")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) "st" (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "r")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool "ex" (Set (Var "m")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "n")) ($#r1_xxreal_0 :::">="::: ) (Set (Var "m")))) "holds" (Bool (Set ($#k4_bhsp_1 :::"dist"::: ) "(" (Set "(" (Set (Var "seq")) ($#k1_normsp_1 :::"."::: ) (Set (Var "n")) ")" ) "," (Set (Var "g")) ")" ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "r"))))))) ")" ))); theorem :: BHSP_2:1 (Bool "for" (Set (Var "X")) "being" ($#l1_bhsp_1 :::"RealUnitarySpace":::) (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "seq")) "is" ($#v3_funct_1 :::"constant"::: ) )) "holds" (Bool (Set (Var "seq")) "is" ($#v1_bhsp_2 :::"convergent"::: ) ))) ; theorem :: BHSP_2:2 (Bool "for" (Set (Var "X")) "being" ($#l1_bhsp_1 :::"RealUnitarySpace":::) (Bool "for" (Set (Var "seq")) "," (Set (Var "seq9")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "seq")) "is" ($#v1_bhsp_2 :::"convergent"::: ) ) & (Bool "ex" (Set (Var "k")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "k")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n")))) "holds" (Bool (Set (Set (Var "seq9")) ($#k1_normsp_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "seq")) ($#k1_normsp_1 :::"."::: ) (Set (Var "n"))))))) "holds" (Bool (Set (Var "seq9")) "is" ($#v1_bhsp_2 :::"convergent"::: ) ))) ; theorem :: BHSP_2:3 (Bool "for" (Set (Var "X")) "being" ($#l1_bhsp_1 :::"RealUnitarySpace":::) (Bool "for" (Set (Var "seq1")) "," (Set (Var "seq2")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "seq1")) "is" ($#v1_bhsp_2 :::"convergent"::: ) ) & (Bool (Set (Var "seq2")) "is" ($#v1_bhsp_2 :::"convergent"::: ) )) "holds" (Bool (Set (Set (Var "seq1")) ($#k2_normsp_1 :::"+"::: ) (Set (Var "seq2"))) "is" ($#v1_bhsp_2 :::"convergent"::: ) ))) ; theorem :: BHSP_2:4 (Bool "for" (Set (Var "X")) "being" ($#l1_bhsp_1 :::"RealUnitarySpace":::) (Bool "for" (Set (Var "seq1")) "," (Set (Var "seq2")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "seq1")) "is" ($#v1_bhsp_2 :::"convergent"::: ) ) & (Bool (Set (Var "seq2")) "is" ($#v1_bhsp_2 :::"convergent"::: ) )) "holds" (Bool (Set (Set (Var "seq1")) ($#k3_normsp_1 :::"-"::: ) (Set (Var "seq2"))) "is" ($#v1_bhsp_2 :::"convergent"::: ) ))) ; theorem :: BHSP_2:5 (Bool "for" (Set (Var "X")) "being" ($#l1_bhsp_1 :::"RealUnitarySpace":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "seq")) "is" ($#v1_bhsp_2 :::"convergent"::: ) )) "holds" (Bool (Set (Set (Var "a")) ($#k5_normsp_1 :::"*"::: ) (Set (Var "seq"))) "is" ($#v1_bhsp_2 :::"convergent"::: ) )))) ; theorem :: BHSP_2:6 (Bool "for" (Set (Var "X")) "being" ($#l1_bhsp_1 :::"RealUnitarySpace":::) (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "seq")) "is" ($#v1_bhsp_2 :::"convergent"::: ) )) "holds" (Bool (Set ($#k5_vfunct_1 :::"-"::: ) (Set (Var "seq"))) "is" ($#v1_bhsp_2 :::"convergent"::: ) ))) ; theorem :: BHSP_2:7 (Bool "for" (Set (Var "X")) "being" ($#l1_bhsp_1 :::"RealUnitarySpace":::) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "seq")) "is" ($#v1_bhsp_2 :::"convergent"::: ) )) "holds" (Bool (Set (Set (Var "seq")) ($#k5_bhsp_1 :::"+"::: ) (Set (Var "x"))) "is" ($#v1_bhsp_2 :::"convergent"::: ) )))) ; theorem :: BHSP_2:8 (Bool "for" (Set (Var "X")) "being" ($#l1_bhsp_1 :::"RealUnitarySpace":::) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "seq")) "is" ($#v1_bhsp_2 :::"convergent"::: ) )) "holds" (Bool (Set (Set (Var "seq")) ($#k4_normsp_1 :::"-"::: ) (Set (Var "x"))) "is" ($#v1_bhsp_2 :::"convergent"::: ) )))) ; theorem :: BHSP_2:9 (Bool "for" (Set (Var "X")) "being" ($#l1_bhsp_1 :::"RealUnitarySpace":::) (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "seq")) "is" ($#v1_bhsp_2 :::"convergent"::: ) ) "iff" (Bool "ex" (Set (Var "g")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) "st" (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "r")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool "ex" (Set (Var "m")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "n")) ($#r1_xxreal_0 :::">="::: ) (Set (Var "m")))) "holds" (Bool (Set ($#k3_bhsp_1 :::"||."::: ) (Set "(" (Set "(" (Set (Var "seq")) ($#k1_normsp_1 :::"."::: ) (Set (Var "n")) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set (Var "g")) ")" ) ($#k3_bhsp_1 :::".||"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "r"))))))) ")" ))) ; definitionlet "X" be ($#l1_bhsp_1 :::"RealUnitarySpace":::); let "seq" be ($#m1_subset_1 :::"sequence":::) "of" (Set (Const "X")); assume (Bool (Set (Const "seq")) "is" ($#v1_bhsp_2 :::"convergent"::: ) ) ; func :::"lim"::: "seq" -> ($#m1_subset_1 :::"Point":::) "of" "X" means :: BHSP_2:def 2 (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "r")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool "ex" (Set (Var "m")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "n")) ($#r1_xxreal_0 :::">="::: ) (Set (Var "m")))) "holds" (Bool (Set ($#k4_bhsp_1 :::"dist"::: ) "(" (Set "(" "seq" ($#k1_normsp_1 :::"."::: ) (Set (Var "n")) ")" ) "," it ")" ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "r")))))); end; :: deftheorem defines :::"lim"::: BHSP_2:def 2 : (Bool "for" (Set (Var "X")) "being" ($#l1_bhsp_1 :::"RealUnitarySpace":::) (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "seq")) "is" ($#v1_bhsp_2 :::"convergent"::: ) )) "holds" (Bool "for" (Set (Var "b3")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k1_bhsp_2 :::"lim"::: ) (Set (Var "seq")))) "iff" (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "r")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool "ex" (Set (Var "m")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "n")) ($#r1_xxreal_0 :::">="::: ) (Set (Var "m")))) "holds" (Bool (Set ($#k4_bhsp_1 :::"dist"::: ) "(" (Set "(" (Set (Var "seq")) ($#k1_normsp_1 :::"."::: ) (Set (Var "n")) ")" ) "," (Set (Var "b3")) ")" ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "r")))))) ")" )))); theorem :: BHSP_2:10 (Bool "for" (Set (Var "X")) "being" ($#l1_bhsp_1 :::"RealUnitarySpace":::) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "seq")) "is" ($#v3_funct_1 :::"constant"::: ) ) & (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "seq"))))) "holds" (Bool (Set ($#k1_bhsp_2 :::"lim"::: ) (Set (Var "seq"))) ($#r1_hidden :::"="::: ) (Set (Var "x")))))) ; theorem :: BHSP_2:11 (Bool "for" (Set (Var "X")) "being" ($#l1_bhsp_1 :::"RealUnitarySpace":::) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "seq")) "is" ($#v3_funct_1 :::"constant"::: ) ) & (Bool "ex" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Set (Set (Var "seq")) ($#k1_normsp_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Var "x"))))) "holds" (Bool (Set ($#k1_bhsp_2 :::"lim"::: ) (Set (Var "seq"))) ($#r1_hidden :::"="::: ) (Set (Var "x")))))) ; theorem :: BHSP_2:12 (Bool "for" (Set (Var "X")) "being" ($#l1_bhsp_1 :::"RealUnitarySpace":::) (Bool "for" (Set (Var "seq")) "," (Set (Var "seq9")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "seq")) "is" ($#v1_bhsp_2 :::"convergent"::: ) ) & (Bool "ex" (Set (Var "k")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "n")) ($#r1_xxreal_0 :::">="::: ) (Set (Var "k")))) "holds" (Bool (Set (Set (Var "seq9")) ($#k1_normsp_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "seq")) ($#k1_normsp_1 :::"."::: ) (Set (Var "n"))))))) "holds" (Bool (Set ($#k1_bhsp_2 :::"lim"::: ) (Set (Var "seq"))) ($#r1_hidden :::"="::: ) (Set ($#k1_bhsp_2 :::"lim"::: ) (Set (Var "seq9")))))) ; theorem :: BHSP_2:13 (Bool "for" (Set (Var "X")) "being" ($#l1_bhsp_1 :::"RealUnitarySpace":::) (Bool "for" (Set (Var "seq1")) "," (Set (Var "seq2")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "seq1")) "is" ($#v1_bhsp_2 :::"convergent"::: ) ) & (Bool (Set (Var "seq2")) "is" ($#v1_bhsp_2 :::"convergent"::: ) )) "holds" (Bool (Set ($#k1_bhsp_2 :::"lim"::: ) (Set "(" (Set (Var "seq1")) ($#k2_normsp_1 :::"+"::: ) (Set (Var "seq2")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_bhsp_2 :::"lim"::: ) (Set (Var "seq1")) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" ($#k1_bhsp_2 :::"lim"::: ) (Set (Var "seq2")) ")" ))))) ; theorem :: BHSP_2:14 (Bool "for" (Set (Var "X")) "being" ($#l1_bhsp_1 :::"RealUnitarySpace":::) (Bool "for" (Set (Var "seq1")) "," (Set (Var "seq2")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "seq1")) "is" ($#v1_bhsp_2 :::"convergent"::: ) ) & (Bool (Set (Var "seq2")) "is" ($#v1_bhsp_2 :::"convergent"::: ) )) "holds" (Bool (Set ($#k1_bhsp_2 :::"lim"::: ) (Set "(" (Set (Var "seq1")) ($#k3_normsp_1 :::"-"::: ) (Set (Var "seq2")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_bhsp_2 :::"lim"::: ) (Set (Var "seq1")) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set "(" ($#k1_bhsp_2 :::"lim"::: ) (Set (Var "seq2")) ")" ))))) ; theorem :: BHSP_2:15 (Bool "for" (Set (Var "X")) "being" ($#l1_bhsp_1 :::"RealUnitarySpace":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "seq")) "is" ($#v1_bhsp_2 :::"convergent"::: ) )) "holds" (Bool (Set ($#k1_bhsp_2 :::"lim"::: ) (Set "(" (Set (Var "a")) ($#k5_normsp_1 :::"*"::: ) (Set (Var "seq")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k1_rlvect_1 :::"*"::: ) (Set "(" ($#k1_bhsp_2 :::"lim"::: ) (Set (Var "seq")) ")" )))))) ; theorem :: BHSP_2:16 (Bool "for" (Set (Var "X")) "being" ($#l1_bhsp_1 :::"RealUnitarySpace":::) (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "seq")) "is" ($#v1_bhsp_2 :::"convergent"::: ) )) "holds" (Bool (Set ($#k1_bhsp_2 :::"lim"::: ) (Set "(" ($#k5_vfunct_1 :::"-"::: ) (Set (Var "seq")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_algstr_0 :::"-"::: ) (Set "(" ($#k1_bhsp_2 :::"lim"::: ) (Set (Var "seq")) ")" ))))) ; theorem :: BHSP_2:17 (Bool "for" (Set (Var "X")) "being" ($#l1_bhsp_1 :::"RealUnitarySpace":::) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "seq")) "is" ($#v1_bhsp_2 :::"convergent"::: ) )) "holds" (Bool (Set ($#k1_bhsp_2 :::"lim"::: ) (Set "(" (Set (Var "seq")) ($#k5_bhsp_1 :::"+"::: ) (Set (Var "x")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_bhsp_2 :::"lim"::: ) (Set (Var "seq")) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "x"))))))) ; theorem :: BHSP_2:18 (Bool "for" (Set (Var "X")) "being" ($#l1_bhsp_1 :::"RealUnitarySpace":::) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "seq")) "is" ($#v1_bhsp_2 :::"convergent"::: ) )) "holds" (Bool (Set ($#k1_bhsp_2 :::"lim"::: ) (Set "(" (Set (Var "seq")) ($#k4_normsp_1 :::"-"::: ) (Set (Var "x")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_bhsp_2 :::"lim"::: ) (Set (Var "seq")) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set (Var "x"))))))) ; theorem :: BHSP_2:19 (Bool "for" (Set (Var "X")) "being" ($#l1_bhsp_1 :::"RealUnitarySpace":::) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "seq")) "is" ($#v1_bhsp_2 :::"convergent"::: ) )) "holds" (Bool "(" (Bool (Set ($#k1_bhsp_2 :::"lim"::: ) (Set (Var "seq"))) ($#r1_hidden :::"="::: ) (Set (Var "g"))) "iff" (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "r")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool "ex" (Set (Var "m")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "n")) ($#r1_xxreal_0 :::">="::: ) (Set (Var "m")))) "holds" (Bool (Set ($#k3_bhsp_1 :::"||."::: ) (Set "(" (Set "(" (Set (Var "seq")) ($#k1_normsp_1 :::"."::: ) (Set (Var "n")) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set (Var "g")) ")" ) ($#k3_bhsp_1 :::".||"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "r")))))) ")" )))) ; definitionlet "X" be ($#l1_bhsp_1 :::"RealUnitarySpace":::); let "seq" be ($#m1_subset_1 :::"sequence":::) "of" (Set (Const "X")); func :::"||.":::"seq":::".||"::: -> ($#m1_subset_1 :::"Real_Sequence":::) means :: BHSP_2:def 3 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set it ($#k8_nat_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set ($#k3_bhsp_1 :::"||."::: ) (Set "(" "seq" ($#k1_normsp_1 :::"."::: ) (Set (Var "n")) ")" ) ($#k3_bhsp_1 :::".||"::: ) ))); end; :: deftheorem defines :::"||."::: BHSP_2:def 3 : (Bool "for" (Set (Var "X")) "being" ($#l1_bhsp_1 :::"RealUnitarySpace":::) (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "b3")) "being" ($#m1_subset_1 :::"Real_Sequence":::) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k2_bhsp_2 :::"||."::: ) (Set (Var "seq")) ($#k2_bhsp_2 :::".||"::: ) )) "iff" (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set (Var "b3")) ($#k8_nat_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set ($#k3_bhsp_1 :::"||."::: ) (Set "(" (Set (Var "seq")) ($#k1_normsp_1 :::"."::: ) (Set (Var "n")) ")" ) ($#k3_bhsp_1 :::".||"::: ) ))) ")" )))); theorem :: BHSP_2:20 (Bool "for" (Set (Var "X")) "being" ($#l1_bhsp_1 :::"RealUnitarySpace":::) (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "seq")) "is" ($#v1_bhsp_2 :::"convergent"::: ) )) "holds" (Bool (Set ($#k2_bhsp_2 :::"||."::: ) (Set (Var "seq")) ($#k2_bhsp_2 :::".||"::: ) ) "is" ($#v2_comseq_2 :::"convergent"::: ) ))) ; theorem :: BHSP_2:21 (Bool "for" (Set (Var "X")) "being" ($#l1_bhsp_1 :::"RealUnitarySpace":::) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "seq")) "is" ($#v1_bhsp_2 :::"convergent"::: ) ) & (Bool (Set ($#k1_bhsp_2 :::"lim"::: ) (Set (Var "seq"))) ($#r1_hidden :::"="::: ) (Set (Var "g")))) "holds" (Bool "(" (Bool (Set ($#k2_bhsp_2 :::"||."::: ) (Set (Var "seq")) ($#k2_bhsp_2 :::".||"::: ) ) "is" ($#v2_comseq_2 :::"convergent"::: ) ) & (Bool (Set ($#k2_seq_2 :::"lim"::: ) (Set ($#k2_bhsp_2 :::"||."::: ) (Set (Var "seq")) ($#k2_bhsp_2 :::".||"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k3_bhsp_1 :::"||."::: ) (Set (Var "g")) ($#k3_bhsp_1 :::".||"::: ) )) ")" )))) ; theorem :: BHSP_2:22 (Bool "for" (Set (Var "X")) "being" ($#l1_bhsp_1 :::"RealUnitarySpace":::) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "seq")) "is" ($#v1_bhsp_2 :::"convergent"::: ) ) & (Bool (Set ($#k1_bhsp_2 :::"lim"::: ) (Set (Var "seq"))) ($#r1_hidden :::"="::: ) (Set (Var "g")))) "holds" (Bool "(" (Bool (Set ($#k2_bhsp_2 :::"||."::: ) (Set "(" (Set (Var "seq")) ($#k4_normsp_1 :::"-"::: ) (Set (Var "g")) ")" ) ($#k2_bhsp_2 :::".||"::: ) ) "is" ($#v2_comseq_2 :::"convergent"::: ) ) & (Bool (Set ($#k2_seq_2 :::"lim"::: ) (Set ($#k2_bhsp_2 :::"||."::: ) (Set "(" (Set (Var "seq")) ($#k4_normsp_1 :::"-"::: ) (Set (Var "g")) ")" ) ($#k2_bhsp_2 :::".||"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" )))) ; definitionlet "X" be ($#l1_bhsp_1 :::"RealUnitarySpace":::); let "seq" be ($#m1_subset_1 :::"sequence":::) "of" (Set (Const "X")); let "x" be ($#m1_subset_1 :::"Point":::) "of" (Set (Const "X")); func :::"dist"::: "(" "seq" "," "x" ")" -> ($#m1_subset_1 :::"Real_Sequence":::) means :: BHSP_2:def 4 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set it ($#k8_nat_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set ($#k4_bhsp_1 :::"dist"::: ) "(" (Set "(" "seq" ($#k1_normsp_1 :::"."::: ) (Set (Var "n")) ")" ) "," "x" ")" ))); end; :: deftheorem defines :::"dist"::: BHSP_2:def 4 : (Bool "for" (Set (Var "X")) "being" ($#l1_bhsp_1 :::"RealUnitarySpace":::) (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "b4")) "being" ($#m1_subset_1 :::"Real_Sequence":::) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set ($#k3_bhsp_2 :::"dist"::: ) "(" (Set (Var "seq")) "," (Set (Var "x")) ")" )) "iff" (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set (Var "b4")) ($#k8_nat_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set ($#k4_bhsp_1 :::"dist"::: ) "(" (Set "(" (Set (Var "seq")) ($#k1_normsp_1 :::"."::: ) (Set (Var "n")) ")" ) "," (Set (Var "x")) ")" ))) ")" ))))); theorem :: BHSP_2:23 (Bool "for" (Set (Var "X")) "being" ($#l1_bhsp_1 :::"RealUnitarySpace":::) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "seq")) "is" ($#v1_bhsp_2 :::"convergent"::: ) ) & (Bool (Set ($#k1_bhsp_2 :::"lim"::: ) (Set (Var "seq"))) ($#r1_hidden :::"="::: ) (Set (Var "g")))) "holds" (Bool (Set ($#k3_bhsp_2 :::"dist"::: ) "(" (Set (Var "seq")) "," (Set (Var "g")) ")" ) "is" ($#v2_comseq_2 :::"convergent"::: ) )))) ; theorem :: BHSP_2:24 (Bool "for" (Set (Var "X")) "being" ($#l1_bhsp_1 :::"RealUnitarySpace":::) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "seq")) "is" ($#v1_bhsp_2 :::"convergent"::: ) ) & (Bool (Set ($#k1_bhsp_2 :::"lim"::: ) (Set (Var "seq"))) ($#r1_hidden :::"="::: ) (Set (Var "g")))) "holds" (Bool "(" (Bool (Set ($#k3_bhsp_2 :::"dist"::: ) "(" (Set (Var "seq")) "," (Set (Var "g")) ")" ) "is" ($#v2_comseq_2 :::"convergent"::: ) ) & (Bool (Set ($#k2_seq_2 :::"lim"::: ) (Set "(" ($#k3_bhsp_2 :::"dist"::: ) "(" (Set (Var "seq")) "," (Set (Var "g")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" )))) ; theorem :: BHSP_2:25 (Bool "for" (Set (Var "X")) "being" ($#l1_bhsp_1 :::"RealUnitarySpace":::) (Bool "for" (Set (Var "g1")) "," (Set (Var "g2")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "seq1")) "," (Set (Var "seq2")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "seq1")) "is" ($#v1_bhsp_2 :::"convergent"::: ) ) & (Bool (Set ($#k1_bhsp_2 :::"lim"::: ) (Set (Var "seq1"))) ($#r1_hidden :::"="::: ) (Set (Var "g1"))) & (Bool (Set (Var "seq2")) "is" ($#v1_bhsp_2 :::"convergent"::: ) ) & (Bool (Set ($#k1_bhsp_2 :::"lim"::: ) (Set (Var "seq2"))) ($#r1_hidden :::"="::: ) (Set (Var "g2")))) "holds" (Bool "(" (Bool (Set ($#k2_bhsp_2 :::"||."::: ) (Set "(" (Set (Var "seq1")) ($#k2_normsp_1 :::"+"::: ) (Set (Var "seq2")) ")" ) ($#k2_bhsp_2 :::".||"::: ) ) "is" ($#v2_comseq_2 :::"convergent"::: ) ) & (Bool (Set ($#k2_seq_2 :::"lim"::: ) (Set ($#k2_bhsp_2 :::"||."::: ) (Set "(" (Set (Var "seq1")) ($#k2_normsp_1 :::"+"::: ) (Set (Var "seq2")) ")" ) ($#k2_bhsp_2 :::".||"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k3_bhsp_1 :::"||."::: ) (Set "(" (Set (Var "g1")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "g2")) ")" ) ($#k3_bhsp_1 :::".||"::: ) )) ")" )))) ; theorem :: BHSP_2:26 (Bool "for" (Set (Var "X")) "being" ($#l1_bhsp_1 :::"RealUnitarySpace":::) (Bool "for" (Set (Var "g1")) "," (Set (Var "g2")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "seq1")) "," (Set (Var "seq2")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "seq1")) "is" ($#v1_bhsp_2 :::"convergent"::: ) ) & (Bool (Set ($#k1_bhsp_2 :::"lim"::: ) (Set (Var "seq1"))) ($#r1_hidden :::"="::: ) (Set (Var "g1"))) & (Bool (Set (Var "seq2")) "is" ($#v1_bhsp_2 :::"convergent"::: ) ) & (Bool (Set ($#k1_bhsp_2 :::"lim"::: ) (Set (Var "seq2"))) ($#r1_hidden :::"="::: ) (Set (Var "g2")))) "holds" (Bool "(" (Bool (Set ($#k2_bhsp_2 :::"||."::: ) (Set "(" (Set "(" (Set (Var "seq1")) ($#k2_normsp_1 :::"+"::: ) (Set (Var "seq2")) ")" ) ($#k4_normsp_1 :::"-"::: ) (Set "(" (Set (Var "g1")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "g2")) ")" ) ")" ) ($#k2_bhsp_2 :::".||"::: ) ) "is" ($#v2_comseq_2 :::"convergent"::: ) ) & (Bool (Set ($#k2_seq_2 :::"lim"::: ) (Set ($#k2_bhsp_2 :::"||."::: ) (Set "(" (Set "(" (Set (Var "seq1")) ($#k2_normsp_1 :::"+"::: ) (Set (Var "seq2")) ")" ) ($#k4_normsp_1 :::"-"::: ) (Set "(" (Set (Var "g1")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "g2")) ")" ) ")" ) ($#k2_bhsp_2 :::".||"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" )))) ; theorem :: BHSP_2:27 (Bool "for" (Set (Var "X")) "being" ($#l1_bhsp_1 :::"RealUnitarySpace":::) (Bool "for" (Set (Var "g1")) "," (Set (Var "g2")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "seq1")) "," (Set (Var "seq2")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "seq1")) "is" ($#v1_bhsp_2 :::"convergent"::: ) ) & (Bool (Set ($#k1_bhsp_2 :::"lim"::: ) (Set (Var "seq1"))) ($#r1_hidden :::"="::: ) (Set (Var "g1"))) & (Bool (Set (Var "seq2")) "is" ($#v1_bhsp_2 :::"convergent"::: ) ) & (Bool (Set ($#k1_bhsp_2 :::"lim"::: ) (Set (Var "seq2"))) ($#r1_hidden :::"="::: ) (Set (Var "g2")))) "holds" (Bool "(" (Bool (Set ($#k2_bhsp_2 :::"||."::: ) (Set "(" (Set (Var "seq1")) ($#k3_normsp_1 :::"-"::: ) (Set (Var "seq2")) ")" ) ($#k2_bhsp_2 :::".||"::: ) ) "is" ($#v2_comseq_2 :::"convergent"::: ) ) & (Bool (Set ($#k2_seq_2 :::"lim"::: ) (Set ($#k2_bhsp_2 :::"||."::: ) (Set "(" (Set (Var "seq1")) ($#k3_normsp_1 :::"-"::: ) (Set (Var "seq2")) ")" ) ($#k2_bhsp_2 :::".||"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k3_bhsp_1 :::"||."::: ) (Set "(" (Set (Var "g1")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "g2")) ")" ) ($#k3_bhsp_1 :::".||"::: ) )) ")" )))) ; theorem :: BHSP_2:28 (Bool "for" (Set (Var "X")) "being" ($#l1_bhsp_1 :::"RealUnitarySpace":::) (Bool "for" (Set (Var "g1")) "," (Set (Var "g2")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "seq1")) "," (Set (Var "seq2")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "seq1")) "is" ($#v1_bhsp_2 :::"convergent"::: ) ) & (Bool (Set ($#k1_bhsp_2 :::"lim"::: ) (Set (Var "seq1"))) ($#r1_hidden :::"="::: ) (Set (Var "g1"))) & (Bool (Set (Var "seq2")) "is" ($#v1_bhsp_2 :::"convergent"::: ) ) & (Bool (Set ($#k1_bhsp_2 :::"lim"::: ) (Set (Var "seq2"))) ($#r1_hidden :::"="::: ) (Set (Var "g2")))) "holds" (Bool "(" (Bool (Set ($#k2_bhsp_2 :::"||."::: ) (Set "(" (Set "(" (Set (Var "seq1")) ($#k3_normsp_1 :::"-"::: ) (Set (Var "seq2")) ")" ) ($#k4_normsp_1 :::"-"::: ) (Set "(" (Set (Var "g1")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "g2")) ")" ) ")" ) ($#k2_bhsp_2 :::".||"::: ) ) "is" ($#v2_comseq_2 :::"convergent"::: ) ) & (Bool (Set ($#k2_seq_2 :::"lim"::: ) (Set ($#k2_bhsp_2 :::"||."::: ) (Set "(" (Set "(" (Set (Var "seq1")) ($#k3_normsp_1 :::"-"::: ) (Set (Var "seq2")) ")" ) ($#k4_normsp_1 :::"-"::: ) (Set "(" (Set (Var "g1")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "g2")) ")" ) ")" ) ($#k2_bhsp_2 :::".||"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" )))) ; theorem :: BHSP_2:29 (Bool "for" (Set (Var "X")) "being" ($#l1_bhsp_1 :::"RealUnitarySpace":::) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "seq")) "is" ($#v1_bhsp_2 :::"convergent"::: ) ) & (Bool (Set ($#k1_bhsp_2 :::"lim"::: ) (Set (Var "seq"))) ($#r1_hidden :::"="::: ) (Set (Var "g")))) "holds" (Bool "(" (Bool (Set ($#k2_bhsp_2 :::"||."::: ) (Set "(" (Set (Var "a")) ($#k5_normsp_1 :::"*"::: ) (Set (Var "seq")) ")" ) ($#k2_bhsp_2 :::".||"::: ) ) "is" ($#v2_comseq_2 :::"convergent"::: ) ) & (Bool (Set ($#k2_seq_2 :::"lim"::: ) (Set ($#k2_bhsp_2 :::"||."::: ) (Set "(" (Set (Var "a")) ($#k5_normsp_1 :::"*"::: ) (Set (Var "seq")) ")" ) ($#k2_bhsp_2 :::".||"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k3_bhsp_1 :::"||."::: ) (Set "(" (Set (Var "a")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "g")) ")" ) ($#k3_bhsp_1 :::".||"::: ) )) ")" ))))) ; theorem :: BHSP_2:30 (Bool "for" (Set (Var "X")) "being" ($#l1_bhsp_1 :::"RealUnitarySpace":::) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "seq")) "is" ($#v1_bhsp_2 :::"convergent"::: ) ) & (Bool (Set ($#k1_bhsp_2 :::"lim"::: ) (Set (Var "seq"))) ($#r1_hidden :::"="::: ) (Set (Var "g")))) "holds" (Bool "(" (Bool (Set ($#k2_bhsp_2 :::"||."::: ) (Set "(" (Set "(" (Set (Var "a")) ($#k5_normsp_1 :::"*"::: ) (Set (Var "seq")) ")" ) ($#k4_normsp_1 :::"-"::: ) (Set "(" (Set (Var "a")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "g")) ")" ) ")" ) ($#k2_bhsp_2 :::".||"::: ) ) "is" ($#v2_comseq_2 :::"convergent"::: ) ) & (Bool (Set ($#k2_seq_2 :::"lim"::: ) (Set ($#k2_bhsp_2 :::"||."::: ) (Set "(" (Set "(" (Set (Var "a")) ($#k5_normsp_1 :::"*"::: ) (Set (Var "seq")) ")" ) ($#k4_normsp_1 :::"-"::: ) (Set "(" (Set (Var "a")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "g")) ")" ) ")" ) ($#k2_bhsp_2 :::".||"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" ))))) ; theorem :: BHSP_2:31 (Bool "for" (Set (Var "X")) "being" ($#l1_bhsp_1 :::"RealUnitarySpace":::) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "seq")) "is" ($#v1_bhsp_2 :::"convergent"::: ) ) & (Bool (Set ($#k1_bhsp_2 :::"lim"::: ) (Set (Var "seq"))) ($#r1_hidden :::"="::: ) (Set (Var "g")))) "holds" (Bool "(" (Bool (Set ($#k2_bhsp_2 :::"||."::: ) (Set "(" ($#k5_vfunct_1 :::"-"::: ) (Set (Var "seq")) ")" ) ($#k2_bhsp_2 :::".||"::: ) ) "is" ($#v2_comseq_2 :::"convergent"::: ) ) & (Bool (Set ($#k2_seq_2 :::"lim"::: ) (Set ($#k2_bhsp_2 :::"||."::: ) (Set "(" ($#k5_vfunct_1 :::"-"::: ) (Set (Var "seq")) ")" ) ($#k2_bhsp_2 :::".||"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k3_bhsp_1 :::"||."::: ) (Set "(" ($#k4_algstr_0 :::"-"::: ) (Set (Var "g")) ")" ) ($#k3_bhsp_1 :::".||"::: ) )) ")" )))) ; theorem :: BHSP_2:32 (Bool "for" (Set (Var "X")) "being" ($#l1_bhsp_1 :::"RealUnitarySpace":::) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "seq")) "is" ($#v1_bhsp_2 :::"convergent"::: ) ) & (Bool (Set ($#k1_bhsp_2 :::"lim"::: ) (Set (Var "seq"))) ($#r1_hidden :::"="::: ) (Set (Var "g")))) "holds" (Bool "(" (Bool (Set ($#k2_bhsp_2 :::"||."::: ) (Set "(" (Set "(" ($#k5_vfunct_1 :::"-"::: ) (Set (Var "seq")) ")" ) ($#k4_normsp_1 :::"-"::: ) (Set "(" ($#k4_algstr_0 :::"-"::: ) (Set (Var "g")) ")" ) ")" ) ($#k2_bhsp_2 :::".||"::: ) ) "is" ($#v2_comseq_2 :::"convergent"::: ) ) & (Bool (Set ($#k2_seq_2 :::"lim"::: ) (Set ($#k2_bhsp_2 :::"||."::: ) (Set "(" (Set "(" ($#k5_vfunct_1 :::"-"::: ) (Set (Var "seq")) ")" ) ($#k4_normsp_1 :::"-"::: ) (Set "(" ($#k4_algstr_0 :::"-"::: ) (Set (Var "g")) ")" ) ")" ) ($#k2_bhsp_2 :::".||"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" )))) ; theorem :: BHSP_2:33 (Bool "for" (Set (Var "X")) "being" ($#l1_bhsp_1 :::"RealUnitarySpace":::) (Bool "for" (Set (Var "g")) "," (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "seq")) "is" ($#v1_bhsp_2 :::"convergent"::: ) ) & (Bool (Set ($#k1_bhsp_2 :::"lim"::: ) (Set (Var "seq"))) ($#r1_hidden :::"="::: ) (Set (Var "g")))) "holds" (Bool "(" (Bool (Set ($#k2_bhsp_2 :::"||."::: ) (Set "(" (Set "(" (Set (Var "seq")) ($#k5_bhsp_1 :::"+"::: ) (Set (Var "x")) ")" ) ($#k4_normsp_1 :::"-"::: ) (Set "(" (Set (Var "g")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "x")) ")" ) ")" ) ($#k2_bhsp_2 :::".||"::: ) ) "is" ($#v2_comseq_2 :::"convergent"::: ) ) & (Bool (Set ($#k2_seq_2 :::"lim"::: ) (Set ($#k2_bhsp_2 :::"||."::: ) (Set "(" (Set "(" (Set (Var "seq")) ($#k5_bhsp_1 :::"+"::: ) (Set (Var "x")) ")" ) ($#k4_normsp_1 :::"-"::: ) (Set "(" (Set (Var "g")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "x")) ")" ) ")" ) ($#k2_bhsp_2 :::".||"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" )))) ; theorem :: BHSP_2:34 (Bool "for" (Set (Var "X")) "being" ($#l1_bhsp_1 :::"RealUnitarySpace":::) (Bool "for" (Set (Var "g")) "," (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "seq")) "is" ($#v1_bhsp_2 :::"convergent"::: ) ) & (Bool (Set ($#k1_bhsp_2 :::"lim"::: ) (Set (Var "seq"))) ($#r1_hidden :::"="::: ) (Set (Var "g")))) "holds" (Bool "(" (Bool (Set ($#k2_bhsp_2 :::"||."::: ) (Set "(" (Set (Var "seq")) ($#k4_normsp_1 :::"-"::: ) (Set (Var "x")) ")" ) ($#k2_bhsp_2 :::".||"::: ) ) "is" ($#v2_comseq_2 :::"convergent"::: ) ) & (Bool (Set ($#k2_seq_2 :::"lim"::: ) (Set ($#k2_bhsp_2 :::"||."::: ) (Set "(" (Set (Var "seq")) ($#k4_normsp_1 :::"-"::: ) (Set (Var "x")) ")" ) ($#k2_bhsp_2 :::".||"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k3_bhsp_1 :::"||."::: ) (Set "(" (Set (Var "g")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "x")) ")" ) ($#k3_bhsp_1 :::".||"::: ) )) ")" )))) ; theorem :: BHSP_2:35 (Bool "for" (Set (Var "X")) "being" ($#l1_bhsp_1 :::"RealUnitarySpace":::) (Bool "for" (Set (Var "g")) "," (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "seq")) "is" ($#v1_bhsp_2 :::"convergent"::: ) ) & (Bool (Set ($#k1_bhsp_2 :::"lim"::: ) (Set (Var "seq"))) ($#r1_hidden :::"="::: ) (Set (Var "g")))) "holds" (Bool "(" (Bool (Set ($#k2_bhsp_2 :::"||."::: ) (Set "(" (Set "(" (Set (Var "seq")) ($#k4_normsp_1 :::"-"::: ) (Set (Var "x")) ")" ) ($#k4_normsp_1 :::"-"::: ) (Set "(" (Set (Var "g")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "x")) ")" ) ")" ) ($#k2_bhsp_2 :::".||"::: ) ) "is" ($#v2_comseq_2 :::"convergent"::: ) ) & (Bool (Set ($#k2_seq_2 :::"lim"::: ) (Set ($#k2_bhsp_2 :::"||."::: ) (Set "(" (Set "(" (Set (Var "seq")) ($#k4_normsp_1 :::"-"::: ) (Set (Var "x")) ")" ) ($#k4_normsp_1 :::"-"::: ) (Set "(" (Set (Var "g")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "x")) ")" ) ")" ) ($#k2_bhsp_2 :::".||"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" )))) ; theorem :: BHSP_2:36 (Bool "for" (Set (Var "X")) "being" ($#l1_bhsp_1 :::"RealUnitarySpace":::) (Bool "for" (Set (Var "g1")) "," (Set (Var "g2")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "seq1")) "," (Set (Var "seq2")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "seq1")) "is" ($#v1_bhsp_2 :::"convergent"::: ) ) & (Bool (Set ($#k1_bhsp_2 :::"lim"::: ) (Set (Var "seq1"))) ($#r1_hidden :::"="::: ) (Set (Var "g1"))) & (Bool (Set (Var "seq2")) "is" ($#v1_bhsp_2 :::"convergent"::: ) ) & (Bool (Set ($#k1_bhsp_2 :::"lim"::: ) (Set (Var "seq2"))) ($#r1_hidden :::"="::: ) (Set (Var "g2")))) "holds" (Bool "(" (Bool (Set ($#k3_bhsp_2 :::"dist"::: ) "(" (Set "(" (Set (Var "seq1")) ($#k2_normsp_1 :::"+"::: ) (Set (Var "seq2")) ")" ) "," (Set "(" (Set (Var "g1")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "g2")) ")" ) ")" ) "is" ($#v2_comseq_2 :::"convergent"::: ) ) & (Bool (Set ($#k2_seq_2 :::"lim"::: ) (Set "(" ($#k3_bhsp_2 :::"dist"::: ) "(" (Set "(" (Set (Var "seq1")) ($#k2_normsp_1 :::"+"::: ) (Set (Var "seq2")) ")" ) "," (Set "(" (Set (Var "g1")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "g2")) ")" ) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" )))) ; theorem :: BHSP_2:37 (Bool "for" (Set (Var "X")) "being" ($#l1_bhsp_1 :::"RealUnitarySpace":::) (Bool "for" (Set (Var "g1")) "," (Set (Var "g2")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "seq1")) "," (Set (Var "seq2")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "seq1")) "is" ($#v1_bhsp_2 :::"convergent"::: ) ) & (Bool (Set ($#k1_bhsp_2 :::"lim"::: ) (Set (Var "seq1"))) ($#r1_hidden :::"="::: ) (Set (Var "g1"))) & (Bool (Set (Var "seq2")) "is" ($#v1_bhsp_2 :::"convergent"::: ) ) & (Bool (Set ($#k1_bhsp_2 :::"lim"::: ) (Set (Var "seq2"))) ($#r1_hidden :::"="::: ) (Set (Var "g2")))) "holds" (Bool "(" (Bool (Set ($#k3_bhsp_2 :::"dist"::: ) "(" (Set "(" (Set (Var "seq1")) ($#k3_normsp_1 :::"-"::: ) (Set (Var "seq2")) ")" ) "," (Set "(" (Set (Var "g1")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "g2")) ")" ) ")" ) "is" ($#v2_comseq_2 :::"convergent"::: ) ) & (Bool (Set ($#k2_seq_2 :::"lim"::: ) (Set "(" ($#k3_bhsp_2 :::"dist"::: ) "(" (Set "(" (Set (Var "seq1")) ($#k3_normsp_1 :::"-"::: ) (Set (Var "seq2")) ")" ) "," (Set "(" (Set (Var "g1")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "g2")) ")" ) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" )))) ; theorem :: BHSP_2:38 (Bool "for" (Set (Var "X")) "being" ($#l1_bhsp_1 :::"RealUnitarySpace":::) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "seq")) "is" ($#v1_bhsp_2 :::"convergent"::: ) ) & (Bool (Set ($#k1_bhsp_2 :::"lim"::: ) (Set (Var "seq"))) ($#r1_hidden :::"="::: ) (Set (Var "g")))) "holds" (Bool "(" (Bool (Set ($#k3_bhsp_2 :::"dist"::: ) "(" (Set "(" (Set (Var "a")) ($#k5_normsp_1 :::"*"::: ) (Set (Var "seq")) ")" ) "," (Set "(" (Set (Var "a")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "g")) ")" ) ")" ) "is" ($#v2_comseq_2 :::"convergent"::: ) ) & (Bool (Set ($#k2_seq_2 :::"lim"::: ) (Set "(" ($#k3_bhsp_2 :::"dist"::: ) "(" (Set "(" (Set (Var "a")) ($#k5_normsp_1 :::"*"::: ) (Set (Var "seq")) ")" ) "," (Set "(" (Set (Var "a")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "g")) ")" ) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" ))))) ; theorem :: BHSP_2:39 (Bool "for" (Set (Var "X")) "being" ($#l1_bhsp_1 :::"RealUnitarySpace":::) (Bool "for" (Set (Var "g")) "," (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "seq")) "is" ($#v1_bhsp_2 :::"convergent"::: ) ) & (Bool (Set ($#k1_bhsp_2 :::"lim"::: ) (Set (Var "seq"))) ($#r1_hidden :::"="::: ) (Set (Var "g")))) "holds" (Bool "(" (Bool (Set ($#k3_bhsp_2 :::"dist"::: ) "(" (Set "(" (Set (Var "seq")) ($#k5_bhsp_1 :::"+"::: ) (Set (Var "x")) ")" ) "," (Set "(" (Set (Var "g")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "x")) ")" ) ")" ) "is" ($#v2_comseq_2 :::"convergent"::: ) ) & (Bool (Set ($#k2_seq_2 :::"lim"::: ) (Set "(" ($#k3_bhsp_2 :::"dist"::: ) "(" (Set "(" (Set (Var "seq")) ($#k5_bhsp_1 :::"+"::: ) (Set (Var "x")) ")" ) "," (Set "(" (Set (Var "g")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "x")) ")" ) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" )))) ; definitionlet "X" be ($#l1_bhsp_1 :::"RealUnitarySpace":::); let "x" be ($#m1_subset_1 :::"Point":::) "of" (Set (Const "X")); let "r" be ($#m1_subset_1 :::"Real":::); func :::"Ball"::: "(" "x" "," "r" ")" -> ($#m1_subset_1 :::"Subset":::) "of" "X" equals :: BHSP_2:def 5 "{" (Set (Var "y")) where y "is" ($#m1_subset_1 :::"Point":::) "of" "X" : (Bool (Set ($#k3_bhsp_1 :::"||."::: ) (Set "(" "x" ($#k5_algstr_0 :::"-"::: ) (Set (Var "y")) ")" ) ($#k3_bhsp_1 :::".||"::: ) ) ($#r1_xxreal_0 :::"<"::: ) "r") "}" ; func :::"cl_Ball"::: "(" "x" "," "r" ")" -> ($#m1_subset_1 :::"Subset":::) "of" "X" equals :: BHSP_2:def 6 "{" (Set (Var "y")) where y "is" ($#m1_subset_1 :::"Point":::) "of" "X" : (Bool (Set ($#k3_bhsp_1 :::"||."::: ) (Set "(" "x" ($#k5_algstr_0 :::"-"::: ) (Set (Var "y")) ")" ) ($#k3_bhsp_1 :::".||"::: ) ) ($#r1_xxreal_0 :::"<="::: ) "r") "}" ; func :::"Sphere"::: "(" "x" "," "r" ")" -> ($#m1_subset_1 :::"Subset":::) "of" "X" equals :: BHSP_2:def 7 "{" (Set (Var "y")) where y "is" ($#m1_subset_1 :::"Point":::) "of" "X" : (Bool (Set ($#k3_bhsp_1 :::"||."::: ) (Set "(" "x" ($#k5_algstr_0 :::"-"::: ) (Set (Var "y")) ")" ) ($#k3_bhsp_1 :::".||"::: ) ) ($#r1_hidden :::"="::: ) "r") "}" ; end; :: deftheorem defines :::"Ball"::: BHSP_2:def 5 : (Bool "for" (Set (Var "X")) "being" ($#l1_bhsp_1 :::"RealUnitarySpace":::) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "holds" (Bool (Set ($#k4_bhsp_2 :::"Ball"::: ) "(" (Set (Var "x")) "," (Set (Var "r")) ")" ) ($#r1_hidden :::"="::: ) "{" (Set (Var "y")) where y "is" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) : (Bool (Set ($#k3_bhsp_1 :::"||."::: ) (Set "(" (Set (Var "x")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "y")) ")" ) ($#k3_bhsp_1 :::".||"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "r"))) "}" )))); :: deftheorem defines :::"cl_Ball"::: BHSP_2:def 6 : (Bool "for" (Set (Var "X")) "being" ($#l1_bhsp_1 :::"RealUnitarySpace":::) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "holds" (Bool (Set ($#k5_bhsp_2 :::"cl_Ball"::: ) "(" (Set (Var "x")) "," (Set (Var "r")) ")" ) ($#r1_hidden :::"="::: ) "{" (Set (Var "y")) where y "is" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) : (Bool (Set ($#k3_bhsp_1 :::"||."::: ) (Set "(" (Set (Var "x")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "y")) ")" ) ($#k3_bhsp_1 :::".||"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "r"))) "}" )))); :: deftheorem defines :::"Sphere"::: BHSP_2:def 7 : (Bool "for" (Set (Var "X")) "being" ($#l1_bhsp_1 :::"RealUnitarySpace":::) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "holds" (Bool (Set ($#k6_bhsp_2 :::"Sphere"::: ) "(" (Set (Var "x")) "," (Set (Var "r")) ")" ) ($#r1_hidden :::"="::: ) "{" (Set (Var "y")) where y "is" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) : (Bool (Set ($#k3_bhsp_1 :::"||."::: ) (Set "(" (Set (Var "x")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "y")) ")" ) ($#k3_bhsp_1 :::".||"::: ) ) ($#r1_hidden :::"="::: ) (Set (Var "r"))) "}" )))); theorem :: BHSP_2:40 (Bool "for" (Set (Var "X")) "being" ($#l1_bhsp_1 :::"RealUnitarySpace":::) (Bool "for" (Set (Var "z")) "," (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "holds" (Bool "(" (Bool (Set (Var "z")) ($#r2_hidden :::"in"::: ) (Set ($#k4_bhsp_2 :::"Ball"::: ) "(" (Set (Var "x")) "," (Set (Var "r")) ")" )) "iff" (Bool (Set ($#k3_bhsp_1 :::"||."::: ) (Set "(" (Set (Var "x")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "z")) ")" ) ($#k3_bhsp_1 :::".||"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "r"))) ")" )))) ; theorem :: BHSP_2:41 (Bool "for" (Set (Var "X")) "being" ($#l1_bhsp_1 :::"RealUnitarySpace":::) (Bool "for" (Set (Var "z")) "," (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "holds" (Bool "(" (Bool (Set (Var "z")) ($#r2_hidden :::"in"::: ) (Set ($#k4_bhsp_2 :::"Ball"::: ) "(" (Set (Var "x")) "," (Set (Var "r")) ")" )) "iff" (Bool (Set ($#k4_bhsp_1 :::"dist"::: ) "(" (Set (Var "x")) "," (Set (Var "z")) ")" ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "r"))) ")" )))) ; theorem :: BHSP_2:42 (Bool "for" (Set (Var "X")) "being" ($#l1_bhsp_1 :::"RealUnitarySpace":::) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "r")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k4_bhsp_2 :::"Ball"::: ) "(" (Set (Var "x")) "," (Set (Var "r")) ")" ))))) ; theorem :: BHSP_2:43 (Bool "for" (Set (Var "X")) "being" ($#l1_bhsp_1 :::"RealUnitarySpace":::) (Bool "for" (Set (Var "y")) "," (Set (Var "x")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set ($#k4_bhsp_2 :::"Ball"::: ) "(" (Set (Var "x")) "," (Set (Var "r")) ")" )) & (Bool (Set (Var "z")) ($#r2_hidden :::"in"::: ) (Set ($#k4_bhsp_2 :::"Ball"::: ) "(" (Set (Var "x")) "," (Set (Var "r")) ")" ))) "holds" (Bool (Set ($#k4_bhsp_1 :::"dist"::: ) "(" (Set (Var "y")) "," (Set (Var "z")) ")" ) ($#r1_xxreal_0 :::"<"::: ) (Set (Num 2) ($#k8_real_1 :::"*"::: ) (Set (Var "r"))))))) ; theorem :: BHSP_2:44 (Bool "for" (Set (Var "X")) "being" ($#l1_bhsp_1 :::"RealUnitarySpace":::) (Bool "for" (Set (Var "y")) "," (Set (Var "x")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set ($#k4_bhsp_2 :::"Ball"::: ) "(" (Set (Var "x")) "," (Set (Var "r")) ")" ))) "holds" (Bool (Set (Set (Var "y")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "z"))) ($#r2_hidden :::"in"::: ) (Set ($#k4_bhsp_2 :::"Ball"::: ) "(" (Set "(" (Set (Var "x")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "z")) ")" ) "," (Set (Var "r")) ")" ))))) ; theorem :: BHSP_2:45 (Bool "for" (Set (Var "X")) "being" ($#l1_bhsp_1 :::"RealUnitarySpace":::) (Bool "for" (Set (Var "y")) "," (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set ($#k4_bhsp_2 :::"Ball"::: ) "(" (Set (Var "x")) "," (Set (Var "r")) ")" ))) "holds" (Bool (Set (Set (Var "y")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "x"))) ($#r2_hidden :::"in"::: ) (Set ($#k4_bhsp_2 :::"Ball"::: ) "(" (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "X")) ")" ) "," (Set (Var "r")) ")" ))))) ; theorem :: BHSP_2:46 (Bool "for" (Set (Var "X")) "being" ($#l1_bhsp_1 :::"RealUnitarySpace":::) (Bool "for" (Set (Var "y")) "," (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "r")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set ($#k4_bhsp_2 :::"Ball"::: ) "(" (Set (Var "x")) "," (Set (Var "r")) ")" )) & (Bool (Set (Var "r")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "q")))) "holds" (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set ($#k4_bhsp_2 :::"Ball"::: ) "(" (Set (Var "x")) "," (Set (Var "q")) ")" ))))) ; theorem :: BHSP_2:47 (Bool "for" (Set (Var "X")) "being" ($#l1_bhsp_1 :::"RealUnitarySpace":::) (Bool "for" (Set (Var "z")) "," (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "holds" (Bool "(" (Bool (Set (Var "z")) ($#r2_hidden :::"in"::: ) (Set ($#k5_bhsp_2 :::"cl_Ball"::: ) "(" (Set (Var "x")) "," (Set (Var "r")) ")" )) "iff" (Bool (Set ($#k3_bhsp_1 :::"||."::: ) (Set "(" (Set (Var "x")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "z")) ")" ) ($#k3_bhsp_1 :::".||"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "r"))) ")" )))) ; theorem :: BHSP_2:48 (Bool "for" (Set (Var "X")) "being" ($#l1_bhsp_1 :::"RealUnitarySpace":::) (Bool "for" (Set (Var "z")) "," (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "holds" (Bool "(" (Bool (Set (Var "z")) ($#r2_hidden :::"in"::: ) (Set ($#k5_bhsp_2 :::"cl_Ball"::: ) "(" (Set (Var "x")) "," (Set (Var "r")) ")" )) "iff" (Bool (Set ($#k4_bhsp_1 :::"dist"::: ) "(" (Set (Var "x")) "," (Set (Var "z")) ")" ) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "r"))) ")" )))) ; theorem :: BHSP_2:49 (Bool "for" (Set (Var "X")) "being" ($#l1_bhsp_1 :::"RealUnitarySpace":::) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "r")) ($#r1_xxreal_0 :::">="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k5_bhsp_2 :::"cl_Ball"::: ) "(" (Set (Var "x")) "," (Set (Var "r")) ")" ))))) ; theorem :: BHSP_2:50 (Bool "for" (Set (Var "X")) "being" ($#l1_bhsp_1 :::"RealUnitarySpace":::) (Bool "for" (Set (Var "y")) "," (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set ($#k4_bhsp_2 :::"Ball"::: ) "(" (Set (Var "x")) "," (Set (Var "r")) ")" ))) "holds" (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set ($#k5_bhsp_2 :::"cl_Ball"::: ) "(" (Set (Var "x")) "," (Set (Var "r")) ")" ))))) ; theorem :: BHSP_2:51 (Bool "for" (Set (Var "X")) "being" ($#l1_bhsp_1 :::"RealUnitarySpace":::) (Bool "for" (Set (Var "z")) "," (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "holds" (Bool "(" (Bool (Set (Var "z")) ($#r2_hidden :::"in"::: ) (Set ($#k6_bhsp_2 :::"Sphere"::: ) "(" (Set (Var "x")) "," (Set (Var "r")) ")" )) "iff" (Bool (Set ($#k3_bhsp_1 :::"||."::: ) (Set "(" (Set (Var "x")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "z")) ")" ) ($#k3_bhsp_1 :::".||"::: ) ) ($#r1_hidden :::"="::: ) (Set (Var "r"))) ")" )))) ; theorem :: BHSP_2:52 (Bool "for" (Set (Var "X")) "being" ($#l1_bhsp_1 :::"RealUnitarySpace":::) (Bool "for" (Set (Var "z")) "," (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "holds" (Bool "(" (Bool (Set (Var "z")) ($#r2_hidden :::"in"::: ) (Set ($#k6_bhsp_2 :::"Sphere"::: ) "(" (Set (Var "x")) "," (Set (Var "r")) ")" )) "iff" (Bool (Set ($#k4_bhsp_1 :::"dist"::: ) "(" (Set (Var "x")) "," (Set (Var "z")) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "r"))) ")" )))) ; theorem :: BHSP_2:53 (Bool "for" (Set (Var "X")) "being" ($#l1_bhsp_1 :::"RealUnitarySpace":::) (Bool "for" (Set (Var "y")) "," (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set ($#k6_bhsp_2 :::"Sphere"::: ) "(" (Set (Var "x")) "," (Set (Var "r")) ")" ))) "holds" (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set ($#k5_bhsp_2 :::"cl_Ball"::: ) "(" (Set (Var "x")) "," (Set (Var "r")) ")" ))))) ; theorem :: BHSP_2:54 (Bool "for" (Set (Var "X")) "being" ($#l1_bhsp_1 :::"RealUnitarySpace":::) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "holds" (Bool (Set ($#k4_bhsp_2 :::"Ball"::: ) "(" (Set (Var "x")) "," (Set (Var "r")) ")" ) ($#r1_tarski :::"c="::: ) (Set ($#k5_bhsp_2 :::"cl_Ball"::: ) "(" (Set (Var "x")) "," (Set (Var "r")) ")" ))))) ; theorem :: BHSP_2:55 (Bool "for" (Set (Var "X")) "being" ($#l1_bhsp_1 :::"RealUnitarySpace":::) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "holds" (Bool (Set ($#k6_bhsp_2 :::"Sphere"::: ) "(" (Set (Var "x")) "," (Set (Var "r")) ")" ) ($#r1_tarski :::"c="::: ) (Set ($#k5_bhsp_2 :::"cl_Ball"::: ) "(" (Set (Var "x")) "," (Set (Var "r")) ")" ))))) ; theorem :: BHSP_2:56 (Bool "for" (Set (Var "X")) "being" ($#l1_bhsp_1 :::"RealUnitarySpace":::) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "holds" (Bool (Set (Set "(" ($#k4_bhsp_2 :::"Ball"::: ) "(" (Set (Var "x")) "," (Set (Var "r")) ")" ")" ) ($#k4_subset_1 :::"\/"::: ) (Set "(" ($#k6_bhsp_2 :::"Sphere"::: ) "(" (Set (Var "x")) "," (Set (Var "r")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k5_bhsp_2 :::"cl_Ball"::: ) "(" (Set (Var "x")) "," (Set (Var "r")) ")" ))))) ;