:: CLVECT_2 semantic presentation begin definitionlet "X" be ($#l1_csspace :::"ComplexUnitarySpace":::); let "seq" be ($#m1_subset_1 :::"sequence":::) "of" (Set (Const "X")); attr "seq" is :::"convergent"::: means :: CLVECT_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" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "n")) ($#r1_xxreal_0 :::">="::: ) (Set (Var "m")))) "holds" (Bool (Set ($#k15_csspace :::"dist"::: ) "(" (Set "(" "seq" ($#k1_normsp_1 :::"."::: ) (Set (Var "n")) ")" ) "," (Set (Var "g")) ")" ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "r"))))))); end; :: deftheorem defines :::"convergent"::: CLVECT_2:def 1 : (Bool "for" (Set (Var "X")) "being" ($#l1_csspace :::"ComplexUnitarySpace":::) (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "seq")) "is" ($#v1_clvect_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" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "n")) ($#r1_xxreal_0 :::">="::: ) (Set (Var "m")))) "holds" (Bool (Set ($#k15_csspace :::"dist"::: ) "(" (Set "(" (Set (Var "seq")) ($#k1_normsp_1 :::"."::: ) (Set (Var "n")) ")" ) "," (Set (Var "g")) ")" ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "r"))))))) ")" ))); theorem :: CLVECT_2:1 (Bool "for" (Set (Var "X")) "being" ($#l1_csspace :::"ComplexUnitarySpace":::) (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_clvect_2 :::"convergent"::: ) ))) ; theorem :: CLVECT_2:2 (Bool "for" (Set (Var "X")) "being" ($#l1_csspace :::"ComplexUnitarySpace":::) (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_clvect_2 :::"convergent"::: ) ) & (Bool "ex" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "for" (Set (Var "n")) "being" ($#m2_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 "seq2")) ($#k1_normsp_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "seq1")) ($#k1_normsp_1 :::"."::: ) (Set (Var "n"))))))) "holds" (Bool (Set (Var "seq2")) "is" ($#v1_clvect_2 :::"convergent"::: ) ))) ; theorem :: CLVECT_2:3 (Bool "for" (Set (Var "X")) "being" ($#l1_csspace :::"ComplexUnitarySpace":::) (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_clvect_2 :::"convergent"::: ) ) & (Bool (Set (Var "seq2")) "is" ($#v1_clvect_2 :::"convergent"::: ) )) "holds" (Bool (Set (Set (Var "seq1")) ($#k16_csspace :::"+"::: ) (Set (Var "seq2"))) "is" ($#v1_clvect_2 :::"convergent"::: ) ))) ; theorem :: CLVECT_2:4 (Bool "for" (Set (Var "X")) "being" ($#l1_csspace :::"ComplexUnitarySpace":::) (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_clvect_2 :::"convergent"::: ) ) & (Bool (Set (Var "seq2")) "is" ($#v1_clvect_2 :::"convergent"::: ) )) "holds" (Bool (Set (Set (Var "seq1")) ($#k3_normsp_1 :::"-"::: ) (Set (Var "seq2"))) "is" ($#v1_clvect_2 :::"convergent"::: ) ))) ; theorem :: CLVECT_2:5 (Bool "for" (Set (Var "X")) "being" ($#l1_csspace :::"ComplexUnitarySpace":::) (Bool "for" (Set (Var "z")) "being" ($#m1_hidden :::"Complex":::) (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "seq")) "is" ($#v1_clvect_2 :::"convergent"::: ) )) "holds" (Bool (Set (Set (Var "z")) ($#k6_clvect_1 :::"*"::: ) (Set (Var "seq"))) "is" ($#v1_clvect_2 :::"convergent"::: ) )))) ; theorem :: CLVECT_2:6 (Bool "for" (Set (Var "X")) "being" ($#l1_csspace :::"ComplexUnitarySpace":::) (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "seq")) "is" ($#v1_clvect_2 :::"convergent"::: ) )) "holds" (Bool (Set ($#k5_vfunct_1 :::"-"::: ) (Set (Var "seq"))) "is" ($#v1_clvect_2 :::"convergent"::: ) ))) ; theorem :: CLVECT_2:7 (Bool "for" (Set (Var "X")) "being" ($#l1_csspace :::"ComplexUnitarySpace":::) (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_clvect_2 :::"convergent"::: ) )) "holds" (Bool (Set (Set (Var "seq")) ($#k5_bhsp_1 :::"+"::: ) (Set (Var "x"))) "is" ($#v1_clvect_2 :::"convergent"::: ) )))) ; theorem :: CLVECT_2:8 (Bool "for" (Set (Var "X")) "being" ($#l1_csspace :::"ComplexUnitarySpace":::) (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_clvect_2 :::"convergent"::: ) )) "holds" (Bool (Set (Set (Var "seq")) ($#k4_normsp_1 :::"-"::: ) (Set (Var "x"))) "is" ($#v1_clvect_2 :::"convergent"::: ) )))) ; theorem :: CLVECT_2:9 (Bool "for" (Set (Var "X")) "being" ($#l1_csspace :::"ComplexUnitarySpace":::) (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "seq")) "is" ($#v1_clvect_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" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "n")) ($#r1_xxreal_0 :::">="::: ) (Set (Var "m")))) "holds" (Bool (Set ($#k13_csspace :::"||."::: ) (Set "(" (Set "(" (Set (Var "seq")) ($#k1_normsp_1 :::"."::: ) (Set (Var "n")) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set (Var "g")) ")" ) ($#k13_csspace :::".||"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "r"))))))) ")" ))) ; definitionlet "X" be ($#l1_csspace :::"ComplexUnitarySpace":::); let "seq" be ($#m1_subset_1 :::"sequence":::) "of" (Set (Const "X")); assume (Bool (Set (Const "seq")) "is" ($#v1_clvect_2 :::"convergent"::: ) ) ; func :::"lim"::: "seq" -> ($#m1_subset_1 :::"Point":::) "of" "X" means :: CLVECT_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" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "n")) ($#r1_xxreal_0 :::">="::: ) (Set (Var "m")))) "holds" (Bool (Set ($#k15_csspace :::"dist"::: ) "(" (Set "(" "seq" ($#k1_normsp_1 :::"."::: ) (Set (Var "n")) ")" ) "," it ")" ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "r")))))); end; :: deftheorem defines :::"lim"::: CLVECT_2:def 2 : (Bool "for" (Set (Var "X")) "being" ($#l1_csspace :::"ComplexUnitarySpace":::) (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "seq")) "is" ($#v1_clvect_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_clvect_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" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "n")) ($#r1_xxreal_0 :::">="::: ) (Set (Var "m")))) "holds" (Bool (Set ($#k15_csspace :::"dist"::: ) "(" (Set "(" (Set (Var "seq")) ($#k1_normsp_1 :::"."::: ) (Set (Var "n")) ")" ) "," (Set (Var "b3")) ")" ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "r")))))) ")" )))); theorem :: CLVECT_2:10 (Bool "for" (Set (Var "X")) "being" ($#l1_csspace :::"ComplexUnitarySpace":::) (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_clvect_2 :::"lim"::: ) (Set (Var "seq"))) ($#r1_hidden :::"="::: ) (Set (Var "x")))))) ; theorem :: CLVECT_2:11 (Bool "for" (Set (Var "X")) "being" ($#l1_csspace :::"ComplexUnitarySpace":::) (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" ($#m2_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_clvect_2 :::"lim"::: ) (Set (Var "seq"))) ($#r1_hidden :::"="::: ) (Set (Var "x")))))) ; theorem :: CLVECT_2:12 (Bool "for" (Set (Var "X")) "being" ($#l1_csspace :::"ComplexUnitarySpace":::) (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_clvect_2 :::"convergent"::: ) ) & (Bool "ex" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "for" (Set (Var "n")) "being" ($#m2_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 "seq2")) ($#k1_normsp_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "seq1")) ($#k1_normsp_1 :::"."::: ) (Set (Var "n"))))))) "holds" (Bool (Set ($#k1_clvect_2 :::"lim"::: ) (Set (Var "seq1"))) ($#r1_hidden :::"="::: ) (Set ($#k1_clvect_2 :::"lim"::: ) (Set (Var "seq2")))))) ; theorem :: CLVECT_2:13 (Bool "for" (Set (Var "X")) "being" ($#l1_csspace :::"ComplexUnitarySpace":::) (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_clvect_2 :::"convergent"::: ) ) & (Bool (Set (Var "seq2")) "is" ($#v1_clvect_2 :::"convergent"::: ) )) "holds" (Bool (Set ($#k1_clvect_2 :::"lim"::: ) (Set "(" (Set (Var "seq1")) ($#k16_csspace :::"+"::: ) (Set (Var "seq2")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_clvect_2 :::"lim"::: ) (Set (Var "seq1")) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" ($#k1_clvect_2 :::"lim"::: ) (Set (Var "seq2")) ")" ))))) ; theorem :: CLVECT_2:14 (Bool "for" (Set (Var "X")) "being" ($#l1_csspace :::"ComplexUnitarySpace":::) (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_clvect_2 :::"convergent"::: ) ) & (Bool (Set (Var "seq2")) "is" ($#v1_clvect_2 :::"convergent"::: ) )) "holds" (Bool (Set ($#k1_clvect_2 :::"lim"::: ) (Set "(" (Set (Var "seq1")) ($#k3_normsp_1 :::"-"::: ) (Set (Var "seq2")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_clvect_2 :::"lim"::: ) (Set (Var "seq1")) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set "(" ($#k1_clvect_2 :::"lim"::: ) (Set (Var "seq2")) ")" ))))) ; theorem :: CLVECT_2:15 (Bool "for" (Set (Var "X")) "being" ($#l1_csspace :::"ComplexUnitarySpace":::) (Bool "for" (Set (Var "z")) "being" ($#m1_hidden :::"Complex":::) (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "seq")) "is" ($#v1_clvect_2 :::"convergent"::: ) )) "holds" (Bool (Set ($#k1_clvect_2 :::"lim"::: ) (Set "(" (Set (Var "z")) ($#k6_clvect_1 :::"*"::: ) (Set (Var "seq")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "z")) ($#k1_clvect_1 :::"*"::: ) (Set "(" ($#k1_clvect_2 :::"lim"::: ) (Set (Var "seq")) ")" )))))) ; theorem :: CLVECT_2:16 (Bool "for" (Set (Var "X")) "being" ($#l1_csspace :::"ComplexUnitarySpace":::) (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "seq")) "is" ($#v1_clvect_2 :::"convergent"::: ) )) "holds" (Bool (Set ($#k1_clvect_2 :::"lim"::: ) (Set "(" ($#k5_vfunct_1 :::"-"::: ) (Set (Var "seq")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_algstr_0 :::"-"::: ) (Set "(" ($#k1_clvect_2 :::"lim"::: ) (Set (Var "seq")) ")" ))))) ; theorem :: CLVECT_2:17 (Bool "for" (Set (Var "X")) "being" ($#l1_csspace :::"ComplexUnitarySpace":::) (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_clvect_2 :::"convergent"::: ) )) "holds" (Bool (Set ($#k1_clvect_2 :::"lim"::: ) (Set "(" (Set (Var "seq")) ($#k5_bhsp_1 :::"+"::: ) (Set (Var "x")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_clvect_2 :::"lim"::: ) (Set (Var "seq")) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "x"))))))) ; theorem :: CLVECT_2:18 (Bool "for" (Set (Var "X")) "being" ($#l1_csspace :::"ComplexUnitarySpace":::) (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_clvect_2 :::"convergent"::: ) )) "holds" (Bool (Set ($#k1_clvect_2 :::"lim"::: ) (Set "(" (Set (Var "seq")) ($#k4_normsp_1 :::"-"::: ) (Set (Var "x")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_clvect_2 :::"lim"::: ) (Set (Var "seq")) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set (Var "x"))))))) ; theorem :: CLVECT_2:19 (Bool "for" (Set (Var "X")) "being" ($#l1_csspace :::"ComplexUnitarySpace":::) (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_clvect_2 :::"convergent"::: ) )) "holds" (Bool "(" (Bool (Set ($#k1_clvect_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" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "n")) ($#r1_xxreal_0 :::">="::: ) (Set (Var "m")))) "holds" (Bool (Set ($#k13_csspace :::"||."::: ) (Set "(" (Set "(" (Set (Var "seq")) ($#k1_normsp_1 :::"."::: ) (Set (Var "n")) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set (Var "g")) ")" ) ($#k13_csspace :::".||"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "r")))))) ")" )))) ; definitionlet "X" be ($#l1_csspace :::"ComplexUnitarySpace":::); let "seq" be ($#m1_subset_1 :::"sequence":::) "of" (Set (Const "X")); func :::"||.":::"seq":::".||"::: -> ($#m1_subset_1 :::"Real_Sequence":::) means :: CLVECT_2:def 3 (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set it ($#k1_seq_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set ($#k13_csspace :::"||."::: ) (Set "(" "seq" ($#k1_normsp_1 :::"."::: ) (Set (Var "n")) ")" ) ($#k13_csspace :::".||"::: ) ))); end; :: deftheorem defines :::"||."::: CLVECT_2:def 3 : (Bool "for" (Set (Var "X")) "being" ($#l1_csspace :::"ComplexUnitarySpace":::) (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_clvect_2 :::"||."::: ) (Set (Var "seq")) ($#k2_clvect_2 :::".||"::: ) )) "iff" (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set (Var "b3")) ($#k1_seq_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set ($#k13_csspace :::"||."::: ) (Set "(" (Set (Var "seq")) ($#k1_normsp_1 :::"."::: ) (Set (Var "n")) ")" ) ($#k13_csspace :::".||"::: ) ))) ")" )))); theorem :: CLVECT_2:20 (Bool "for" (Set (Var "X")) "being" ($#l1_csspace :::"ComplexUnitarySpace":::) (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "seq")) "is" ($#v1_clvect_2 :::"convergent"::: ) )) "holds" (Bool (Set ($#k2_clvect_2 :::"||."::: ) (Set (Var "seq")) ($#k2_clvect_2 :::".||"::: ) ) "is" ($#v2_comseq_2 :::"convergent"::: ) ))) ; theorem :: CLVECT_2:21 (Bool "for" (Set (Var "X")) "being" ($#l1_csspace :::"ComplexUnitarySpace":::) (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_clvect_2 :::"convergent"::: ) ) & (Bool (Set ($#k1_clvect_2 :::"lim"::: ) (Set (Var "seq"))) ($#r1_hidden :::"="::: ) (Set (Var "g")))) "holds" (Bool "(" (Bool (Set ($#k2_clvect_2 :::"||."::: ) (Set (Var "seq")) ($#k2_clvect_2 :::".||"::: ) ) "is" ($#v2_comseq_2 :::"convergent"::: ) ) & (Bool (Set ($#k2_seq_2 :::"lim"::: ) (Set ($#k2_clvect_2 :::"||."::: ) (Set (Var "seq")) ($#k2_clvect_2 :::".||"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k13_csspace :::"||."::: ) (Set (Var "g")) ($#k13_csspace :::".||"::: ) )) ")" )))) ; theorem :: CLVECT_2:22 (Bool "for" (Set (Var "X")) "being" ($#l1_csspace :::"ComplexUnitarySpace":::) (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_clvect_2 :::"convergent"::: ) ) & (Bool (Set ($#k1_clvect_2 :::"lim"::: ) (Set (Var "seq"))) ($#r1_hidden :::"="::: ) (Set (Var "g")))) "holds" (Bool "(" (Bool (Set ($#k2_clvect_2 :::"||."::: ) (Set "(" (Set (Var "seq")) ($#k4_normsp_1 :::"-"::: ) (Set (Var "g")) ")" ) ($#k2_clvect_2 :::".||"::: ) ) "is" ($#v2_comseq_2 :::"convergent"::: ) ) & (Bool (Set ($#k2_seq_2 :::"lim"::: ) (Set ($#k2_clvect_2 :::"||."::: ) (Set "(" (Set (Var "seq")) ($#k4_normsp_1 :::"-"::: ) (Set (Var "g")) ")" ) ($#k2_clvect_2 :::".||"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" )))) ; definitionlet "X" be ($#l1_csspace :::"ComplexUnitarySpace":::); 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 :: CLVECT_2:def 4 (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set it ($#k1_seq_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set ($#k15_csspace :::"dist"::: ) "(" (Set "(" "seq" ($#k1_normsp_1 :::"."::: ) (Set (Var "n")) ")" ) "," "x" ")" ))); end; :: deftheorem defines :::"dist"::: CLVECT_2:def 4 : (Bool "for" (Set (Var "X")) "being" ($#l1_csspace :::"ComplexUnitarySpace":::) (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_clvect_2 :::"dist"::: ) "(" (Set (Var "seq")) "," (Set (Var "x")) ")" )) "iff" (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set (Var "b4")) ($#k1_seq_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set ($#k15_csspace :::"dist"::: ) "(" (Set "(" (Set (Var "seq")) ($#k1_normsp_1 :::"."::: ) (Set (Var "n")) ")" ) "," (Set (Var "x")) ")" ))) ")" ))))); theorem :: CLVECT_2:23 (Bool "for" (Set (Var "X")) "being" ($#l1_csspace :::"ComplexUnitarySpace":::) (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_clvect_2 :::"convergent"::: ) ) & (Bool (Set ($#k1_clvect_2 :::"lim"::: ) (Set (Var "seq"))) ($#r1_hidden :::"="::: ) (Set (Var "g")))) "holds" (Bool (Set ($#k3_clvect_2 :::"dist"::: ) "(" (Set (Var "seq")) "," (Set (Var "g")) ")" ) "is" ($#v2_comseq_2 :::"convergent"::: ) )))) ; theorem :: CLVECT_2:24 (Bool "for" (Set (Var "X")) "being" ($#l1_csspace :::"ComplexUnitarySpace":::) (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_clvect_2 :::"convergent"::: ) ) & (Bool (Set ($#k1_clvect_2 :::"lim"::: ) (Set (Var "seq"))) ($#r1_hidden :::"="::: ) (Set (Var "g")))) "holds" (Bool "(" (Bool (Set ($#k3_clvect_2 :::"dist"::: ) "(" (Set (Var "seq")) "," (Set (Var "g")) ")" ) "is" ($#v2_comseq_2 :::"convergent"::: ) ) & (Bool (Set ($#k2_seq_2 :::"lim"::: ) (Set "(" ($#k3_clvect_2 :::"dist"::: ) "(" (Set (Var "seq")) "," (Set (Var "g")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" )))) ; theorem :: CLVECT_2:25 (Bool "for" (Set (Var "X")) "being" ($#l1_csspace :::"ComplexUnitarySpace":::) (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_clvect_2 :::"convergent"::: ) ) & (Bool (Set ($#k1_clvect_2 :::"lim"::: ) (Set (Var "seq1"))) ($#r1_hidden :::"="::: ) (Set (Var "g1"))) & (Bool (Set (Var "seq2")) "is" ($#v1_clvect_2 :::"convergent"::: ) ) & (Bool (Set ($#k1_clvect_2 :::"lim"::: ) (Set (Var "seq2"))) ($#r1_hidden :::"="::: ) (Set (Var "g2")))) "holds" (Bool "(" (Bool (Set ($#k2_clvect_2 :::"||."::: ) (Set "(" (Set (Var "seq1")) ($#k16_csspace :::"+"::: ) (Set (Var "seq2")) ")" ) ($#k2_clvect_2 :::".||"::: ) ) "is" ($#v2_comseq_2 :::"convergent"::: ) ) & (Bool (Set ($#k2_seq_2 :::"lim"::: ) (Set ($#k2_clvect_2 :::"||."::: ) (Set "(" (Set (Var "seq1")) ($#k16_csspace :::"+"::: ) (Set (Var "seq2")) ")" ) ($#k2_clvect_2 :::".||"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k13_csspace :::"||."::: ) (Set "(" (Set (Var "g1")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "g2")) ")" ) ($#k13_csspace :::".||"::: ) )) ")" )))) ; theorem :: CLVECT_2:26 (Bool "for" (Set (Var "X")) "being" ($#l1_csspace :::"ComplexUnitarySpace":::) (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_clvect_2 :::"convergent"::: ) ) & (Bool (Set ($#k1_clvect_2 :::"lim"::: ) (Set (Var "seq1"))) ($#r1_hidden :::"="::: ) (Set (Var "g1"))) & (Bool (Set (Var "seq2")) "is" ($#v1_clvect_2 :::"convergent"::: ) ) & (Bool (Set ($#k1_clvect_2 :::"lim"::: ) (Set (Var "seq2"))) ($#r1_hidden :::"="::: ) (Set (Var "g2")))) "holds" (Bool "(" (Bool (Set ($#k2_clvect_2 :::"||."::: ) (Set "(" (Set "(" (Set (Var "seq1")) ($#k16_csspace :::"+"::: ) (Set (Var "seq2")) ")" ) ($#k4_normsp_1 :::"-"::: ) (Set "(" (Set (Var "g1")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "g2")) ")" ) ")" ) ($#k2_clvect_2 :::".||"::: ) ) "is" ($#v2_comseq_2 :::"convergent"::: ) ) & (Bool (Set ($#k2_seq_2 :::"lim"::: ) (Set ($#k2_clvect_2 :::"||."::: ) (Set "(" (Set "(" (Set (Var "seq1")) ($#k16_csspace :::"+"::: ) (Set (Var "seq2")) ")" ) ($#k4_normsp_1 :::"-"::: ) (Set "(" (Set (Var "g1")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "g2")) ")" ) ")" ) ($#k2_clvect_2 :::".||"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" )))) ; theorem :: CLVECT_2:27 (Bool "for" (Set (Var "X")) "being" ($#l1_csspace :::"ComplexUnitarySpace":::) (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_clvect_2 :::"convergent"::: ) ) & (Bool (Set ($#k1_clvect_2 :::"lim"::: ) (Set (Var "seq1"))) ($#r1_hidden :::"="::: ) (Set (Var "g1"))) & (Bool (Set (Var "seq2")) "is" ($#v1_clvect_2 :::"convergent"::: ) ) & (Bool (Set ($#k1_clvect_2 :::"lim"::: ) (Set (Var "seq2"))) ($#r1_hidden :::"="::: ) (Set (Var "g2")))) "holds" (Bool "(" (Bool (Set ($#k2_clvect_2 :::"||."::: ) (Set "(" (Set (Var "seq1")) ($#k3_normsp_1 :::"-"::: ) (Set (Var "seq2")) ")" ) ($#k2_clvect_2 :::".||"::: ) ) "is" ($#v2_comseq_2 :::"convergent"::: ) ) & (Bool (Set ($#k2_seq_2 :::"lim"::: ) (Set ($#k2_clvect_2 :::"||."::: ) (Set "(" (Set (Var "seq1")) ($#k3_normsp_1 :::"-"::: ) (Set (Var "seq2")) ")" ) ($#k2_clvect_2 :::".||"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k13_csspace :::"||."::: ) (Set "(" (Set (Var "g1")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "g2")) ")" ) ($#k13_csspace :::".||"::: ) )) ")" )))) ; theorem :: CLVECT_2:28 (Bool "for" (Set (Var "X")) "being" ($#l1_csspace :::"ComplexUnitarySpace":::) (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_clvect_2 :::"convergent"::: ) ) & (Bool (Set ($#k1_clvect_2 :::"lim"::: ) (Set (Var "seq1"))) ($#r1_hidden :::"="::: ) (Set (Var "g1"))) & (Bool (Set (Var "seq2")) "is" ($#v1_clvect_2 :::"convergent"::: ) ) & (Bool (Set ($#k1_clvect_2 :::"lim"::: ) (Set (Var "seq2"))) ($#r1_hidden :::"="::: ) (Set (Var "g2")))) "holds" (Bool "(" (Bool (Set ($#k2_clvect_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_clvect_2 :::".||"::: ) ) "is" ($#v2_comseq_2 :::"convergent"::: ) ) & (Bool (Set ($#k2_seq_2 :::"lim"::: ) (Set ($#k2_clvect_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_clvect_2 :::".||"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" )))) ; theorem :: CLVECT_2:29 (Bool "for" (Set (Var "X")) "being" ($#l1_csspace :::"ComplexUnitarySpace":::) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "z")) "being" ($#m1_hidden :::"Complex":::) (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "seq")) "is" ($#v1_clvect_2 :::"convergent"::: ) ) & (Bool (Set ($#k1_clvect_2 :::"lim"::: ) (Set (Var "seq"))) ($#r1_hidden :::"="::: ) (Set (Var "g")))) "holds" (Bool "(" (Bool (Set ($#k2_clvect_2 :::"||."::: ) (Set "(" (Set (Var "z")) ($#k6_clvect_1 :::"*"::: ) (Set (Var "seq")) ")" ) ($#k2_clvect_2 :::".||"::: ) ) "is" ($#v2_comseq_2 :::"convergent"::: ) ) & (Bool (Set ($#k2_seq_2 :::"lim"::: ) (Set ($#k2_clvect_2 :::"||."::: ) (Set "(" (Set (Var "z")) ($#k6_clvect_1 :::"*"::: ) (Set (Var "seq")) ")" ) ($#k2_clvect_2 :::".||"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k13_csspace :::"||."::: ) (Set "(" (Set (Var "z")) ($#k1_clvect_1 :::"*"::: ) (Set (Var "g")) ")" ) ($#k13_csspace :::".||"::: ) )) ")" ))))) ; theorem :: CLVECT_2:30 (Bool "for" (Set (Var "X")) "being" ($#l1_csspace :::"ComplexUnitarySpace":::) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "z")) "being" ($#m1_hidden :::"Complex":::) (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "seq")) "is" ($#v1_clvect_2 :::"convergent"::: ) ) & (Bool (Set ($#k1_clvect_2 :::"lim"::: ) (Set (Var "seq"))) ($#r1_hidden :::"="::: ) (Set (Var "g")))) "holds" (Bool "(" (Bool (Set ($#k2_clvect_2 :::"||."::: ) (Set "(" (Set "(" (Set (Var "z")) ($#k6_clvect_1 :::"*"::: ) (Set (Var "seq")) ")" ) ($#k4_normsp_1 :::"-"::: ) (Set "(" (Set (Var "z")) ($#k1_clvect_1 :::"*"::: ) (Set (Var "g")) ")" ) ")" ) ($#k2_clvect_2 :::".||"::: ) ) "is" ($#v2_comseq_2 :::"convergent"::: ) ) & (Bool (Set ($#k2_seq_2 :::"lim"::: ) (Set ($#k2_clvect_2 :::"||."::: ) (Set "(" (Set "(" (Set (Var "z")) ($#k6_clvect_1 :::"*"::: ) (Set (Var "seq")) ")" ) ($#k4_normsp_1 :::"-"::: ) (Set "(" (Set (Var "z")) ($#k1_clvect_1 :::"*"::: ) (Set (Var "g")) ")" ) ")" ) ($#k2_clvect_2 :::".||"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" ))))) ; theorem :: CLVECT_2:31 (Bool "for" (Set (Var "X")) "being" ($#l1_csspace :::"ComplexUnitarySpace":::) (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_clvect_2 :::"convergent"::: ) ) & (Bool (Set ($#k1_clvect_2 :::"lim"::: ) (Set (Var "seq"))) ($#r1_hidden :::"="::: ) (Set (Var "g")))) "holds" (Bool "(" (Bool (Set ($#k2_clvect_2 :::"||."::: ) (Set "(" ($#k5_vfunct_1 :::"-"::: ) (Set (Var "seq")) ")" ) ($#k2_clvect_2 :::".||"::: ) ) "is" ($#v2_comseq_2 :::"convergent"::: ) ) & (Bool (Set ($#k2_seq_2 :::"lim"::: ) (Set ($#k2_clvect_2 :::"||."::: ) (Set "(" ($#k5_vfunct_1 :::"-"::: ) (Set (Var "seq")) ")" ) ($#k2_clvect_2 :::".||"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k13_csspace :::"||."::: ) (Set "(" ($#k4_algstr_0 :::"-"::: ) (Set (Var "g")) ")" ) ($#k13_csspace :::".||"::: ) )) ")" )))) ; theorem :: CLVECT_2:32 (Bool "for" (Set (Var "X")) "being" ($#l1_csspace :::"ComplexUnitarySpace":::) (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_clvect_2 :::"convergent"::: ) ) & (Bool (Set ($#k1_clvect_2 :::"lim"::: ) (Set (Var "seq"))) ($#r1_hidden :::"="::: ) (Set (Var "g")))) "holds" (Bool "(" (Bool (Set ($#k2_clvect_2 :::"||."::: ) (Set "(" (Set "(" ($#k5_vfunct_1 :::"-"::: ) (Set (Var "seq")) ")" ) ($#k4_normsp_1 :::"-"::: ) (Set "(" ($#k4_algstr_0 :::"-"::: ) (Set (Var "g")) ")" ) ")" ) ($#k2_clvect_2 :::".||"::: ) ) "is" ($#v2_comseq_2 :::"convergent"::: ) ) & (Bool (Set ($#k2_seq_2 :::"lim"::: ) (Set ($#k2_clvect_2 :::"||."::: ) (Set "(" (Set "(" ($#k5_vfunct_1 :::"-"::: ) (Set (Var "seq")) ")" ) ($#k4_normsp_1 :::"-"::: ) (Set "(" ($#k4_algstr_0 :::"-"::: ) (Set (Var "g")) ")" ) ")" ) ($#k2_clvect_2 :::".||"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" )))) ; theorem :: CLVECT_2:33 (Bool "for" (Set (Var "X")) "being" ($#l1_csspace :::"ComplexUnitarySpace":::) (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_clvect_2 :::"convergent"::: ) ) & (Bool (Set ($#k1_clvect_2 :::"lim"::: ) (Set (Var "seq"))) ($#r1_hidden :::"="::: ) (Set (Var "g")))) "holds" (Bool "(" (Bool (Set ($#k2_clvect_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_clvect_2 :::".||"::: ) ) "is" ($#v2_comseq_2 :::"convergent"::: ) ) & (Bool (Set ($#k2_seq_2 :::"lim"::: ) (Set ($#k2_clvect_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_clvect_2 :::".||"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" )))) ; theorem :: CLVECT_2:34 (Bool "for" (Set (Var "X")) "being" ($#l1_csspace :::"ComplexUnitarySpace":::) (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_clvect_2 :::"convergent"::: ) ) & (Bool (Set ($#k1_clvect_2 :::"lim"::: ) (Set (Var "seq"))) ($#r1_hidden :::"="::: ) (Set (Var "g")))) "holds" (Bool "(" (Bool (Set ($#k2_clvect_2 :::"||."::: ) (Set "(" (Set (Var "seq")) ($#k4_normsp_1 :::"-"::: ) (Set (Var "x")) ")" ) ($#k2_clvect_2 :::".||"::: ) ) "is" ($#v2_comseq_2 :::"convergent"::: ) ) & (Bool (Set ($#k2_seq_2 :::"lim"::: ) (Set ($#k2_clvect_2 :::"||."::: ) (Set "(" (Set (Var "seq")) ($#k4_normsp_1 :::"-"::: ) (Set (Var "x")) ")" ) ($#k2_clvect_2 :::".||"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k13_csspace :::"||."::: ) (Set "(" (Set (Var "g")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "x")) ")" ) ($#k13_csspace :::".||"::: ) )) ")" )))) ; theorem :: CLVECT_2:35 (Bool "for" (Set (Var "X")) "being" ($#l1_csspace :::"ComplexUnitarySpace":::) (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_clvect_2 :::"convergent"::: ) ) & (Bool (Set ($#k1_clvect_2 :::"lim"::: ) (Set (Var "seq"))) ($#r1_hidden :::"="::: ) (Set (Var "g")))) "holds" (Bool "(" (Bool (Set ($#k2_clvect_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_clvect_2 :::".||"::: ) ) "is" ($#v2_comseq_2 :::"convergent"::: ) ) & (Bool (Set ($#k2_seq_2 :::"lim"::: ) (Set ($#k2_clvect_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_clvect_2 :::".||"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" )))) ; theorem :: CLVECT_2:36 (Bool "for" (Set (Var "X")) "being" ($#l1_csspace :::"ComplexUnitarySpace":::) (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_clvect_2 :::"convergent"::: ) ) & (Bool (Set ($#k1_clvect_2 :::"lim"::: ) (Set (Var "seq1"))) ($#r1_hidden :::"="::: ) (Set (Var "g1"))) & (Bool (Set (Var "seq2")) "is" ($#v1_clvect_2 :::"convergent"::: ) ) & (Bool (Set ($#k1_clvect_2 :::"lim"::: ) (Set (Var "seq2"))) ($#r1_hidden :::"="::: ) (Set (Var "g2")))) "holds" (Bool "(" (Bool (Set ($#k3_clvect_2 :::"dist"::: ) "(" (Set "(" (Set (Var "seq1")) ($#k16_csspace :::"+"::: ) (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_clvect_2 :::"dist"::: ) "(" (Set "(" (Set (Var "seq1")) ($#k16_csspace :::"+"::: ) (Set (Var "seq2")) ")" ) "," (Set "(" (Set (Var "g1")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "g2")) ")" ) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" )))) ; theorem :: CLVECT_2:37 (Bool "for" (Set (Var "X")) "being" ($#l1_csspace :::"ComplexUnitarySpace":::) (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_clvect_2 :::"convergent"::: ) ) & (Bool (Set ($#k1_clvect_2 :::"lim"::: ) (Set (Var "seq1"))) ($#r1_hidden :::"="::: ) (Set (Var "g1"))) & (Bool (Set (Var "seq2")) "is" ($#v1_clvect_2 :::"convergent"::: ) ) & (Bool (Set ($#k1_clvect_2 :::"lim"::: ) (Set (Var "seq2"))) ($#r1_hidden :::"="::: ) (Set (Var "g2")))) "holds" (Bool "(" (Bool (Set ($#k3_clvect_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_clvect_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 :: CLVECT_2:38 (Bool "for" (Set (Var "X")) "being" ($#l1_csspace :::"ComplexUnitarySpace":::) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "z")) "being" ($#m1_hidden :::"Complex":::) (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "seq")) "is" ($#v1_clvect_2 :::"convergent"::: ) ) & (Bool (Set ($#k1_clvect_2 :::"lim"::: ) (Set (Var "seq"))) ($#r1_hidden :::"="::: ) (Set (Var "g")))) "holds" (Bool "(" (Bool (Set ($#k3_clvect_2 :::"dist"::: ) "(" (Set "(" (Set (Var "z")) ($#k6_clvect_1 :::"*"::: ) (Set (Var "seq")) ")" ) "," (Set "(" (Set (Var "z")) ($#k1_clvect_1 :::"*"::: ) (Set (Var "g")) ")" ) ")" ) "is" ($#v2_comseq_2 :::"convergent"::: ) ) & (Bool (Set ($#k2_seq_2 :::"lim"::: ) (Set "(" ($#k3_clvect_2 :::"dist"::: ) "(" (Set "(" (Set (Var "z")) ($#k6_clvect_1 :::"*"::: ) (Set (Var "seq")) ")" ) "," (Set "(" (Set (Var "z")) ($#k1_clvect_1 :::"*"::: ) (Set (Var "g")) ")" ) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" ))))) ; theorem :: CLVECT_2:39 (Bool "for" (Set (Var "X")) "being" ($#l1_csspace :::"ComplexUnitarySpace":::) (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_clvect_2 :::"convergent"::: ) ) & (Bool (Set ($#k1_clvect_2 :::"lim"::: ) (Set (Var "seq"))) ($#r1_hidden :::"="::: ) (Set (Var "g")))) "holds" (Bool "(" (Bool (Set ($#k3_clvect_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_clvect_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_csspace :::"ComplexUnitarySpace":::); 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 :: CLVECT_2:def 5 "{" (Set (Var "y")) where y "is" ($#m1_subset_1 :::"Point":::) "of" "X" : (Bool (Set ($#k13_csspace :::"||."::: ) (Set "(" "x" ($#k5_algstr_0 :::"-"::: ) (Set (Var "y")) ")" ) ($#k13_csspace :::".||"::: ) ) ($#r1_xxreal_0 :::"<"::: ) "r") "}" ; func :::"cl_Ball"::: "(" "x" "," "r" ")" -> ($#m1_subset_1 :::"Subset":::) "of" "X" equals :: CLVECT_2:def 6 "{" (Set (Var "y")) where y "is" ($#m1_subset_1 :::"Point":::) "of" "X" : (Bool (Set ($#k13_csspace :::"||."::: ) (Set "(" "x" ($#k5_algstr_0 :::"-"::: ) (Set (Var "y")) ")" ) ($#k13_csspace :::".||"::: ) ) ($#r1_xxreal_0 :::"<="::: ) "r") "}" ; func :::"Sphere"::: "(" "x" "," "r" ")" -> ($#m1_subset_1 :::"Subset":::) "of" "X" equals :: CLVECT_2:def 7 "{" (Set (Var "y")) where y "is" ($#m1_subset_1 :::"Point":::) "of" "X" : (Bool (Set ($#k13_csspace :::"||."::: ) (Set "(" "x" ($#k5_algstr_0 :::"-"::: ) (Set (Var "y")) ")" ) ($#k13_csspace :::".||"::: ) ) ($#r1_hidden :::"="::: ) "r") "}" ; end; :: deftheorem defines :::"Ball"::: CLVECT_2:def 5 : (Bool "for" (Set (Var "X")) "being" ($#l1_csspace :::"ComplexUnitarySpace":::) (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_clvect_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 ($#k13_csspace :::"||."::: ) (Set "(" (Set (Var "x")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "y")) ")" ) ($#k13_csspace :::".||"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "r"))) "}" )))); :: deftheorem defines :::"cl_Ball"::: CLVECT_2:def 6 : (Bool "for" (Set (Var "X")) "being" ($#l1_csspace :::"ComplexUnitarySpace":::) (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_clvect_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 ($#k13_csspace :::"||."::: ) (Set "(" (Set (Var "x")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "y")) ")" ) ($#k13_csspace :::".||"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "r"))) "}" )))); :: deftheorem defines :::"Sphere"::: CLVECT_2:def 7 : (Bool "for" (Set (Var "X")) "being" ($#l1_csspace :::"ComplexUnitarySpace":::) (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_clvect_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 ($#k13_csspace :::"||."::: ) (Set "(" (Set (Var "x")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "y")) ")" ) ($#k13_csspace :::".||"::: ) ) ($#r1_hidden :::"="::: ) (Set (Var "r"))) "}" )))); theorem :: CLVECT_2:40 (Bool "for" (Set (Var "X")) "being" ($#l1_csspace :::"ComplexUnitarySpace":::) (Bool "for" (Set (Var "w")) "," (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 "w")) ($#r2_hidden :::"in"::: ) (Set ($#k4_clvect_2 :::"Ball"::: ) "(" (Set (Var "x")) "," (Set (Var "r")) ")" )) "iff" (Bool (Set ($#k13_csspace :::"||."::: ) (Set "(" (Set (Var "x")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "w")) ")" ) ($#k13_csspace :::".||"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "r"))) ")" )))) ; theorem :: CLVECT_2:41 (Bool "for" (Set (Var "X")) "being" ($#l1_csspace :::"ComplexUnitarySpace":::) (Bool "for" (Set (Var "w")) "," (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 "w")) ($#r2_hidden :::"in"::: ) (Set ($#k4_clvect_2 :::"Ball"::: ) "(" (Set (Var "x")) "," (Set (Var "r")) ")" )) "iff" (Bool (Set ($#k15_csspace :::"dist"::: ) "(" (Set (Var "x")) "," (Set (Var "w")) ")" ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "r"))) ")" )))) ; theorem :: CLVECT_2:42 (Bool "for" (Set (Var "X")) "being" ($#l1_csspace :::"ComplexUnitarySpace":::) (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_clvect_2 :::"Ball"::: ) "(" (Set (Var "x")) "," (Set (Var "r")) ")" ))))) ; theorem :: CLVECT_2:43 (Bool "for" (Set (Var "X")) "being" ($#l1_csspace :::"ComplexUnitarySpace":::) (Bool "for" (Set (Var "y")) "," (Set (Var "x")) "," (Set (Var "w")) "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_clvect_2 :::"Ball"::: ) "(" (Set (Var "x")) "," (Set (Var "r")) ")" )) & (Bool (Set (Var "w")) ($#r2_hidden :::"in"::: ) (Set ($#k4_clvect_2 :::"Ball"::: ) "(" (Set (Var "x")) "," (Set (Var "r")) ")" ))) "holds" (Bool (Set ($#k15_csspace :::"dist"::: ) "(" (Set (Var "y")) "," (Set (Var "w")) ")" ) ($#r1_xxreal_0 :::"<"::: ) (Set (Num 2) ($#k8_real_1 :::"*"::: ) (Set (Var "r"))))))) ; theorem :: CLVECT_2:44 (Bool "for" (Set (Var "X")) "being" ($#l1_csspace :::"ComplexUnitarySpace":::) (Bool "for" (Set (Var "y")) "," (Set (Var "x")) "," (Set (Var "w")) "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_clvect_2 :::"Ball"::: ) "(" (Set (Var "x")) "," (Set (Var "r")) ")" ))) "holds" (Bool (Set (Set (Var "y")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "w"))) ($#r2_hidden :::"in"::: ) (Set ($#k4_clvect_2 :::"Ball"::: ) "(" (Set "(" (Set (Var "x")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "w")) ")" ) "," (Set (Var "r")) ")" ))))) ; theorem :: CLVECT_2:45 (Bool "for" (Set (Var "X")) "being" ($#l1_csspace :::"ComplexUnitarySpace":::) (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_clvect_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_clvect_2 :::"Ball"::: ) "(" (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "X")) ")" ) "," (Set (Var "r")) ")" ))))) ; theorem :: CLVECT_2:46 (Bool "for" (Set (Var "X")) "being" ($#l1_csspace :::"ComplexUnitarySpace":::) (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_clvect_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_clvect_2 :::"Ball"::: ) "(" (Set (Var "x")) "," (Set (Var "q")) ")" ))))) ; theorem :: CLVECT_2:47 (Bool "for" (Set (Var "X")) "being" ($#l1_csspace :::"ComplexUnitarySpace":::) (Bool "for" (Set (Var "w")) "," (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 "w")) ($#r2_hidden :::"in"::: ) (Set ($#k5_clvect_2 :::"cl_Ball"::: ) "(" (Set (Var "x")) "," (Set (Var "r")) ")" )) "iff" (Bool (Set ($#k13_csspace :::"||."::: ) (Set "(" (Set (Var "x")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "w")) ")" ) ($#k13_csspace :::".||"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "r"))) ")" )))) ; theorem :: CLVECT_2:48 (Bool "for" (Set (Var "X")) "being" ($#l1_csspace :::"ComplexUnitarySpace":::) (Bool "for" (Set (Var "w")) "," (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 "w")) ($#r2_hidden :::"in"::: ) (Set ($#k5_clvect_2 :::"cl_Ball"::: ) "(" (Set (Var "x")) "," (Set (Var "r")) ")" )) "iff" (Bool (Set ($#k15_csspace :::"dist"::: ) "(" (Set (Var "x")) "," (Set (Var "w")) ")" ) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "r"))) ")" )))) ; theorem :: CLVECT_2:49 (Bool "for" (Set (Var "X")) "being" ($#l1_csspace :::"ComplexUnitarySpace":::) (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_clvect_2 :::"cl_Ball"::: ) "(" (Set (Var "x")) "," (Set (Var "r")) ")" ))))) ; theorem :: CLVECT_2:50 (Bool "for" (Set (Var "X")) "being" ($#l1_csspace :::"ComplexUnitarySpace":::) (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_clvect_2 :::"Ball"::: ) "(" (Set (Var "x")) "," (Set (Var "r")) ")" ))) "holds" (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set ($#k5_clvect_2 :::"cl_Ball"::: ) "(" (Set (Var "x")) "," (Set (Var "r")) ")" ))))) ; theorem :: CLVECT_2:51 (Bool "for" (Set (Var "X")) "being" ($#l1_csspace :::"ComplexUnitarySpace":::) (Bool "for" (Set (Var "w")) "," (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 "w")) ($#r2_hidden :::"in"::: ) (Set ($#k6_clvect_2 :::"Sphere"::: ) "(" (Set (Var "x")) "," (Set (Var "r")) ")" )) "iff" (Bool (Set ($#k13_csspace :::"||."::: ) (Set "(" (Set (Var "x")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "w")) ")" ) ($#k13_csspace :::".||"::: ) ) ($#r1_hidden :::"="::: ) (Set (Var "r"))) ")" )))) ; theorem :: CLVECT_2:52 (Bool "for" (Set (Var "X")) "being" ($#l1_csspace :::"ComplexUnitarySpace":::) (Bool "for" (Set (Var "w")) "," (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 "w")) ($#r2_hidden :::"in"::: ) (Set ($#k6_clvect_2 :::"Sphere"::: ) "(" (Set (Var "x")) "," (Set (Var "r")) ")" )) "iff" (Bool (Set ($#k15_csspace :::"dist"::: ) "(" (Set (Var "x")) "," (Set (Var "w")) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "r"))) ")" )))) ; theorem :: CLVECT_2:53 (Bool "for" (Set (Var "X")) "being" ($#l1_csspace :::"ComplexUnitarySpace":::) (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_clvect_2 :::"Sphere"::: ) "(" (Set (Var "x")) "," (Set (Var "r")) ")" ))) "holds" (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set ($#k5_clvect_2 :::"cl_Ball"::: ) "(" (Set (Var "x")) "," (Set (Var "r")) ")" ))))) ; theorem :: CLVECT_2:54 (Bool "for" (Set (Var "X")) "being" ($#l1_csspace :::"ComplexUnitarySpace":::) (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_clvect_2 :::"Ball"::: ) "(" (Set (Var "x")) "," (Set (Var "r")) ")" ) ($#r1_tarski :::"c="::: ) (Set ($#k5_clvect_2 :::"cl_Ball"::: ) "(" (Set (Var "x")) "," (Set (Var "r")) ")" ))))) ; theorem :: CLVECT_2:55 (Bool "for" (Set (Var "X")) "being" ($#l1_csspace :::"ComplexUnitarySpace":::) (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_clvect_2 :::"Sphere"::: ) "(" (Set (Var "x")) "," (Set (Var "r")) ")" ) ($#r1_tarski :::"c="::: ) (Set ($#k5_clvect_2 :::"cl_Ball"::: ) "(" (Set (Var "x")) "," (Set (Var "r")) ")" ))))) ; theorem :: CLVECT_2:56 (Bool "for" (Set (Var "X")) "being" ($#l1_csspace :::"ComplexUnitarySpace":::) (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_clvect_2 :::"Ball"::: ) "(" (Set (Var "x")) "," (Set (Var "r")) ")" ")" ) ($#k4_subset_1 :::"\/"::: ) (Set "(" ($#k6_clvect_2 :::"Sphere"::: ) "(" (Set (Var "x")) "," (Set (Var "r")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k5_clvect_2 :::"cl_Ball"::: ) "(" (Set (Var "x")) "," (Set (Var "r")) ")" ))))) ; begin definitionlet "X" be ($#l1_csspace :::"ComplexUnitarySpace":::); let "seq" be ($#m1_subset_1 :::"sequence":::) "of" (Set (Const "X")); attr "seq" is :::"Cauchy"::: means :: CLVECT_2:def 8 (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 "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "for" (Set (Var "n")) "," (Set (Var "m")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "n")) ($#r1_xxreal_0 :::">="::: ) (Set (Var "k"))) & (Bool (Set (Var "m")) ($#r1_xxreal_0 :::">="::: ) (Set (Var "k")))) "holds" (Bool (Set ($#k15_csspace :::"dist"::: ) "(" (Set "(" "seq" ($#k1_normsp_1 :::"."::: ) (Set (Var "n")) ")" ) "," (Set "(" "seq" ($#k1_normsp_1 :::"."::: ) (Set (Var "m")) ")" ) ")" ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "r")))))); end; :: deftheorem defines :::"Cauchy"::: CLVECT_2:def 8 : (Bool "for" (Set (Var "X")) "being" ($#l1_csspace :::"ComplexUnitarySpace":::) (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "seq")) "is" ($#v2_clvect_2 :::"Cauchy"::: ) ) "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 "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "for" (Set (Var "n")) "," (Set (Var "m")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "n")) ($#r1_xxreal_0 :::">="::: ) (Set (Var "k"))) & (Bool (Set (Var "m")) ($#r1_xxreal_0 :::">="::: ) (Set (Var "k")))) "holds" (Bool (Set ($#k15_csspace :::"dist"::: ) "(" (Set "(" (Set (Var "seq")) ($#k1_normsp_1 :::"."::: ) (Set (Var "n")) ")" ) "," (Set "(" (Set (Var "seq")) ($#k1_normsp_1 :::"."::: ) (Set (Var "m")) ")" ) ")" ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "r")))))) ")" ))); theorem :: CLVECT_2:57 (Bool "for" (Set (Var "X")) "being" ($#l1_csspace :::"ComplexUnitarySpace":::) (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" ($#v2_clvect_2 :::"Cauchy"::: ) ))) ; theorem :: CLVECT_2:58 (Bool "for" (Set (Var "X")) "being" ($#l1_csspace :::"ComplexUnitarySpace":::) (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "seq")) "is" ($#v2_clvect_2 :::"Cauchy"::: ) ) "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 "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "for" (Set (Var "n")) "," (Set (Var "m")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "n")) ($#r1_xxreal_0 :::">="::: ) (Set (Var "k"))) & (Bool (Set (Var "m")) ($#r1_xxreal_0 :::">="::: ) (Set (Var "k")))) "holds" (Bool (Set ($#k13_csspace :::"||."::: ) (Set "(" (Set "(" (Set (Var "seq")) ($#k1_normsp_1 :::"."::: ) (Set (Var "n")) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set "(" (Set (Var "seq")) ($#k1_normsp_1 :::"."::: ) (Set (Var "m")) ")" ) ")" ) ($#k13_csspace :::".||"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "r")))))) ")" ))) ; theorem :: CLVECT_2:59 (Bool "for" (Set (Var "X")) "being" ($#l1_csspace :::"ComplexUnitarySpace":::) (Bool "for" (Set (Var "seq1")) "," (Set (Var "seq2")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "seq1")) "is" ($#v2_clvect_2 :::"Cauchy"::: ) ) & (Bool (Set (Var "seq2")) "is" ($#v2_clvect_2 :::"Cauchy"::: ) )) "holds" (Bool (Set (Set (Var "seq1")) ($#k16_csspace :::"+"::: ) (Set (Var "seq2"))) "is" ($#v2_clvect_2 :::"Cauchy"::: ) ))) ; theorem :: CLVECT_2:60 (Bool "for" (Set (Var "X")) "being" ($#l1_csspace :::"ComplexUnitarySpace":::) (Bool "for" (Set (Var "seq1")) "," (Set (Var "seq2")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "seq1")) "is" ($#v2_clvect_2 :::"Cauchy"::: ) ) & (Bool (Set (Var "seq2")) "is" ($#v2_clvect_2 :::"Cauchy"::: ) )) "holds" (Bool (Set (Set (Var "seq1")) ($#k3_normsp_1 :::"-"::: ) (Set (Var "seq2"))) "is" ($#v2_clvect_2 :::"Cauchy"::: ) ))) ; theorem :: CLVECT_2:61 (Bool "for" (Set (Var "X")) "being" ($#l1_csspace :::"ComplexUnitarySpace":::) (Bool "for" (Set (Var "z")) "being" ($#m1_hidden :::"Complex":::) (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "seq")) "is" ($#v2_clvect_2 :::"Cauchy"::: ) )) "holds" (Bool (Set (Set (Var "z")) ($#k6_clvect_1 :::"*"::: ) (Set (Var "seq"))) "is" ($#v2_clvect_2 :::"Cauchy"::: ) )))) ; theorem :: CLVECT_2:62 (Bool "for" (Set (Var "X")) "being" ($#l1_csspace :::"ComplexUnitarySpace":::) (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "seq")) "is" ($#v2_clvect_2 :::"Cauchy"::: ) )) "holds" (Bool (Set ($#k5_vfunct_1 :::"-"::: ) (Set (Var "seq"))) "is" ($#v2_clvect_2 :::"Cauchy"::: ) ))) ; theorem :: CLVECT_2:63 (Bool "for" (Set (Var "X")) "being" ($#l1_csspace :::"ComplexUnitarySpace":::) (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" ($#v2_clvect_2 :::"Cauchy"::: ) )) "holds" (Bool (Set (Set (Var "seq")) ($#k5_bhsp_1 :::"+"::: ) (Set (Var "x"))) "is" ($#v2_clvect_2 :::"Cauchy"::: ) )))) ; theorem :: CLVECT_2:64 (Bool "for" (Set (Var "X")) "being" ($#l1_csspace :::"ComplexUnitarySpace":::) (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" ($#v2_clvect_2 :::"Cauchy"::: ) )) "holds" (Bool (Set (Set (Var "seq")) ($#k4_normsp_1 :::"-"::: ) (Set (Var "x"))) "is" ($#v2_clvect_2 :::"Cauchy"::: ) )))) ; theorem :: CLVECT_2:65 (Bool "for" (Set (Var "X")) "being" ($#l1_csspace :::"ComplexUnitarySpace":::) (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "seq")) "is" ($#v1_clvect_2 :::"convergent"::: ) )) "holds" (Bool (Set (Var "seq")) "is" ($#v2_clvect_2 :::"Cauchy"::: ) ))) ; definitionlet "X" be ($#l1_csspace :::"ComplexUnitarySpace":::); let "seq1", "seq2" be ($#m1_subset_1 :::"sequence":::) "of" (Set (Const "X")); pred "seq1" :::"is_compared_to"::: "seq2" means :: CLVECT_2:def 9 (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" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "n")) ($#r1_xxreal_0 :::">="::: ) (Set (Var "m")))) "holds" (Bool (Set ($#k15_csspace :::"dist"::: ) "(" (Set "(" "seq1" ($#k1_normsp_1 :::"."::: ) (Set (Var "n")) ")" ) "," (Set "(" "seq2" ($#k1_normsp_1 :::"."::: ) (Set (Var "n")) ")" ) ")" ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "r")))))); end; :: deftheorem defines :::"is_compared_to"::: CLVECT_2:def 9 : (Bool "for" (Set (Var "X")) "being" ($#l1_csspace :::"ComplexUnitarySpace":::) (Bool "for" (Set (Var "seq1")) "," (Set (Var "seq2")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "seq1")) ($#r1_clvect_2 :::"is_compared_to"::: ) (Set (Var "seq2"))) "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" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "n")) ($#r1_xxreal_0 :::">="::: ) (Set (Var "m")))) "holds" (Bool (Set ($#k15_csspace :::"dist"::: ) "(" (Set "(" (Set (Var "seq1")) ($#k1_normsp_1 :::"."::: ) (Set (Var "n")) ")" ) "," (Set "(" (Set (Var "seq2")) ($#k1_normsp_1 :::"."::: ) (Set (Var "n")) ")" ) ")" ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "r")))))) ")" ))); theorem :: CLVECT_2:66 (Bool "for" (Set (Var "X")) "being" ($#l1_csspace :::"ComplexUnitarySpace":::) (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X")) "holds" (Bool (Set (Var "seq")) ($#r1_clvect_2 :::"is_compared_to"::: ) (Set (Var "seq"))))) ; theorem :: CLVECT_2:67 (Bool "for" (Set (Var "X")) "being" ($#l1_csspace :::"ComplexUnitarySpace":::) (Bool "for" (Set (Var "seq1")) "," (Set (Var "seq2")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "seq1")) ($#r1_clvect_2 :::"is_compared_to"::: ) (Set (Var "seq2")))) "holds" (Bool (Set (Var "seq2")) ($#r1_clvect_2 :::"is_compared_to"::: ) (Set (Var "seq1"))))) ; definitionlet "X" be ($#l1_csspace :::"ComplexUnitarySpace":::); let "seq1", "seq2" be ($#m1_subset_1 :::"sequence":::) "of" (Set (Const "X")); :: original: :::"is_compared_to"::: redefine pred "seq1" :::"is_compared_to"::: "seq2"; reflexivity (Bool "for" (Set (Var "seq1")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Const "X")) "holds" (Bool ((Set (Const "X")) "," (Set (Var "b1")) "," (Set (Var "b1"))))) ; symmetry (Bool "for" (Set (Var "seq1")) "," (Set (Var "seq2")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Const "X")) "st" (Bool (Bool ((Set (Const "X")) "," (Set (Var "b1")) "," (Set (Var "b2"))))) "holds" (Bool ((Set (Const "X")) "," (Set (Var "b2")) "," (Set (Var "b1"))))) ; end; theorem :: CLVECT_2:68 (Bool "for" (Set (Var "X")) "being" ($#l1_csspace :::"ComplexUnitarySpace":::) (Bool "for" (Set (Var "seq1")) "," (Set (Var "seq2")) "," (Set (Var "seq3")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "seq1")) ($#r2_clvect_2 :::"is_compared_to"::: ) (Set (Var "seq2"))) & (Bool (Set (Var "seq2")) ($#r2_clvect_2 :::"is_compared_to"::: ) (Set (Var "seq3")))) "holds" (Bool (Set (Var "seq1")) ($#r2_clvect_2 :::"is_compared_to"::: ) (Set (Var "seq3"))))) ; theorem :: CLVECT_2:69 (Bool "for" (Set (Var "X")) "being" ($#l1_csspace :::"ComplexUnitarySpace":::) (Bool "for" (Set (Var "seq1")) "," (Set (Var "seq2")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "seq1")) ($#r2_clvect_2 :::"is_compared_to"::: ) (Set (Var "seq2"))) "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" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "n")) ($#r1_xxreal_0 :::">="::: ) (Set (Var "m")))) "holds" (Bool (Set ($#k13_csspace :::"||."::: ) (Set "(" (Set "(" (Set (Var "seq1")) ($#k1_normsp_1 :::"."::: ) (Set (Var "n")) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set "(" (Set (Var "seq2")) ($#k1_normsp_1 :::"."::: ) (Set (Var "n")) ")" ) ")" ) ($#k13_csspace :::".||"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "r")))))) ")" ))) ; theorem :: CLVECT_2:70 (Bool "for" (Set (Var "X")) "being" ($#l1_csspace :::"ComplexUnitarySpace":::) (Bool "for" (Set (Var "seq1")) "," (Set (Var "seq2")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X")) "st" (Bool (Bool "ex" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "for" (Set (Var "n")) "being" ($#m2_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 "seq1")) ($#k1_normsp_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "seq2")) ($#k1_normsp_1 :::"."::: ) (Set (Var "n"))))))) "holds" (Bool (Set (Var "seq1")) ($#r2_clvect_2 :::"is_compared_to"::: ) (Set (Var "seq2"))))) ; theorem :: CLVECT_2:71 (Bool "for" (Set (Var "X")) "being" ($#l1_csspace :::"ComplexUnitarySpace":::) (Bool "for" (Set (Var "seq1")) "," (Set (Var "seq2")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "seq1")) "is" ($#v2_clvect_2 :::"Cauchy"::: ) ) & (Bool (Set (Var "seq1")) ($#r2_clvect_2 :::"is_compared_to"::: ) (Set (Var "seq2")))) "holds" (Bool (Set (Var "seq2")) "is" ($#v2_clvect_2 :::"Cauchy"::: ) ))) ; theorem :: CLVECT_2:72 (Bool "for" (Set (Var "X")) "being" ($#l1_csspace :::"ComplexUnitarySpace":::) (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_clvect_2 :::"convergent"::: ) ) & (Bool (Set (Var "seq1")) ($#r2_clvect_2 :::"is_compared_to"::: ) (Set (Var "seq2")))) "holds" (Bool (Set (Var "seq2")) "is" ($#v1_clvect_2 :::"convergent"::: ) ))) ; theorem :: CLVECT_2:73 (Bool "for" (Set (Var "X")) "being" ($#l1_csspace :::"ComplexUnitarySpace":::) (Bool "for" (Set (Var "g")) "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_clvect_2 :::"convergent"::: ) ) & (Bool (Set ($#k1_clvect_2 :::"lim"::: ) (Set (Var "seq1"))) ($#r1_hidden :::"="::: ) (Set (Var "g"))) & (Bool (Set (Var "seq1")) ($#r2_clvect_2 :::"is_compared_to"::: ) (Set (Var "seq2")))) "holds" (Bool "(" (Bool (Set (Var "seq2")) "is" ($#v1_clvect_2 :::"convergent"::: ) ) & (Bool (Set ($#k1_clvect_2 :::"lim"::: ) (Set (Var "seq2"))) ($#r1_hidden :::"="::: ) (Set (Var "g"))) ")" )))) ; definitionlet "X" be ($#l1_csspace :::"ComplexUnitarySpace":::); let "seq" be ($#m1_subset_1 :::"sequence":::) "of" (Set (Const "X")); attr "seq" is :::"bounded"::: means :: CLVECT_2:def 10 (Bool "ex" (Set (Var "M")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool "(" (Bool (Set (Var "M")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool "(" "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set ($#k13_csspace :::"||."::: ) (Set "(" "seq" ($#k1_normsp_1 :::"."::: ) (Set (Var "n")) ")" ) ($#k13_csspace :::".||"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "M"))) ")" ) ")" )); end; :: deftheorem defines :::"bounded"::: CLVECT_2:def 10 : (Bool "for" (Set (Var "X")) "being" ($#l1_csspace :::"ComplexUnitarySpace":::) (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "seq")) "is" ($#v3_clvect_2 :::"bounded"::: ) ) "iff" (Bool "ex" (Set (Var "M")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool "(" (Bool (Set (Var "M")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool "(" "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set ($#k13_csspace :::"||."::: ) (Set "(" (Set (Var "seq")) ($#k1_normsp_1 :::"."::: ) (Set (Var "n")) ")" ) ($#k13_csspace :::".||"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "M"))) ")" ) ")" )) ")" ))); theorem :: CLVECT_2:74 (Bool "for" (Set (Var "X")) "being" ($#l1_csspace :::"ComplexUnitarySpace":::) (Bool "for" (Set (Var "seq1")) "," (Set (Var "seq2")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "seq1")) "is" ($#v3_clvect_2 :::"bounded"::: ) ) & (Bool (Set (Var "seq2")) "is" ($#v3_clvect_2 :::"bounded"::: ) )) "holds" (Bool (Set (Set (Var "seq1")) ($#k16_csspace :::"+"::: ) (Set (Var "seq2"))) "is" ($#v3_clvect_2 :::"bounded"::: ) ))) ; theorem :: CLVECT_2:75 (Bool "for" (Set (Var "X")) "being" ($#l1_csspace :::"ComplexUnitarySpace":::) (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "seq")) "is" ($#v3_clvect_2 :::"bounded"::: ) )) "holds" (Bool (Set ($#k5_vfunct_1 :::"-"::: ) (Set (Var "seq"))) "is" ($#v3_clvect_2 :::"bounded"::: ) ))) ; theorem :: CLVECT_2:76 (Bool "for" (Set (Var "X")) "being" ($#l1_csspace :::"ComplexUnitarySpace":::) (Bool "for" (Set (Var "seq1")) "," (Set (Var "seq2")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "seq1")) "is" ($#v3_clvect_2 :::"bounded"::: ) ) & (Bool (Set (Var "seq2")) "is" ($#v3_clvect_2 :::"bounded"::: ) )) "holds" (Bool (Set (Set (Var "seq1")) ($#k3_normsp_1 :::"-"::: ) (Set (Var "seq2"))) "is" ($#v3_clvect_2 :::"bounded"::: ) ))) ; theorem :: CLVECT_2:77 (Bool "for" (Set (Var "X")) "being" ($#l1_csspace :::"ComplexUnitarySpace":::) (Bool "for" (Set (Var "z")) "being" ($#m1_hidden :::"Complex":::) (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "seq")) "is" ($#v3_clvect_2 :::"bounded"::: ) )) "holds" (Bool (Set (Set (Var "z")) ($#k6_clvect_1 :::"*"::: ) (Set (Var "seq"))) "is" ($#v3_clvect_2 :::"bounded"::: ) )))) ; theorem :: CLVECT_2:78 (Bool "for" (Set (Var "X")) "being" ($#l1_csspace :::"ComplexUnitarySpace":::) (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" ($#v3_clvect_2 :::"bounded"::: ) ))) ; theorem :: CLVECT_2:79 (Bool "for" (Set (Var "X")) "being" ($#l1_csspace :::"ComplexUnitarySpace":::) (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "m")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "ex" (Set (Var "M")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool "(" (Bool (Set (Var "M")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool "(" "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "m")))) "holds" (Bool (Set ($#k13_csspace :::"||."::: ) (Set "(" (Set (Var "seq")) ($#k1_normsp_1 :::"."::: ) (Set (Var "n")) ")" ) ($#k13_csspace :::".||"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "M"))) ")" ) ")" ))))) ; theorem :: CLVECT_2:80 (Bool "for" (Set (Var "X")) "being" ($#l1_csspace :::"ComplexUnitarySpace":::) (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "seq")) "is" ($#v1_clvect_2 :::"convergent"::: ) )) "holds" (Bool (Set (Var "seq")) "is" ($#v3_clvect_2 :::"bounded"::: ) ))) ; theorem :: CLVECT_2:81 (Bool "for" (Set (Var "X")) "being" ($#l1_csspace :::"ComplexUnitarySpace":::) (Bool "for" (Set (Var "seq1")) "," (Set (Var "seq2")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "seq1")) "is" ($#v3_clvect_2 :::"bounded"::: ) ) & (Bool (Set (Var "seq1")) ($#r2_clvect_2 :::"is_compared_to"::: ) (Set (Var "seq2")))) "holds" (Bool (Set (Var "seq2")) "is" ($#v3_clvect_2 :::"bounded"::: ) ))) ; theorem :: CLVECT_2:82 (Bool "for" (Set (Var "X")) "being" ($#l1_csspace :::"ComplexUnitarySpace":::) (Bool "for" (Set (Var "seq")) "," (Set (Var "seq1")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "seq")) "is" ($#v3_clvect_2 :::"bounded"::: ) ) & (Bool (Set (Var "seq1")) "is" ($#m2_valued_0 :::"subsequence"::: ) "of" (Set (Var "seq")))) "holds" (Bool (Set (Var "seq1")) "is" ($#v3_clvect_2 :::"bounded"::: ) ))) ; theorem :: CLVECT_2:83 (Bool "for" (Set (Var "X")) "being" ($#l1_csspace :::"ComplexUnitarySpace":::) (Bool "for" (Set (Var "seq")) "," (Set (Var "seq1")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "seq")) "is" ($#v1_clvect_2 :::"convergent"::: ) ) & (Bool (Set (Var "seq1")) "is" ($#m2_valued_0 :::"subsequence"::: ) "of" (Set (Var "seq")))) "holds" (Bool (Set (Var "seq1")) "is" ($#v1_clvect_2 :::"convergent"::: ) ))) ; theorem :: CLVECT_2:84 (Bool "for" (Set (Var "X")) "being" ($#l1_csspace :::"ComplexUnitarySpace":::) (Bool "for" (Set (Var "seq1")) "," (Set (Var "seq")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "seq1")) "is" ($#m2_valued_0 :::"subsequence"::: ) "of" (Set (Var "seq"))) & (Bool (Set (Var "seq")) "is" ($#v1_clvect_2 :::"convergent"::: ) )) "holds" (Bool (Set ($#k1_clvect_2 :::"lim"::: ) (Set (Var "seq1"))) ($#r1_hidden :::"="::: ) (Set ($#k1_clvect_2 :::"lim"::: ) (Set (Var "seq")))))) ; theorem :: CLVECT_2:85 (Bool "for" (Set (Var "X")) "being" ($#l1_csspace :::"ComplexUnitarySpace":::) (Bool "for" (Set (Var "seq")) "," (Set (Var "seq1")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "seq")) "is" ($#v2_clvect_2 :::"Cauchy"::: ) ) & (Bool (Set (Var "seq1")) "is" ($#m2_valued_0 :::"subsequence"::: ) "of" (Set (Var "seq")))) "holds" (Bool (Set (Var "seq1")) "is" ($#v2_clvect_2 :::"Cauchy"::: ) ))) ; theorem :: CLVECT_2:86 (Bool "for" (Set (Var "X")) "being" ($#l1_csspace :::"ComplexUnitarySpace":::) (Bool "for" (Set (Var "seq1")) "," (Set (Var "seq2")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set "(" (Set (Var "seq1")) ($#k16_csspace :::"+"::: ) (Set (Var "seq2")) ")" ) ($#k1_valued_0 :::"^\"::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "seq1")) ($#k1_valued_0 :::"^\"::: ) (Set (Var "k")) ")" ) ($#k16_csspace :::"+"::: ) (Set "(" (Set (Var "seq2")) ($#k1_valued_0 :::"^\"::: ) (Set (Var "k")) ")" )))))) ; theorem :: CLVECT_2:87 (Bool "for" (Set (Var "X")) "being" ($#l1_csspace :::"ComplexUnitarySpace":::) (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set "(" ($#k5_vfunct_1 :::"-"::: ) (Set (Var "seq")) ")" ) ($#k1_valued_0 :::"^\"::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set ($#k5_vfunct_1 :::"-"::: ) (Set "(" (Set (Var "seq")) ($#k1_valued_0 :::"^\"::: ) (Set (Var "k")) ")" )))))) ; theorem :: CLVECT_2:88 (Bool "for" (Set (Var "X")) "being" ($#l1_csspace :::"ComplexUnitarySpace":::) (Bool "for" (Set (Var "seq1")) "," (Set (Var "seq2")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set "(" (Set (Var "seq1")) ($#k3_normsp_1 :::"-"::: ) (Set (Var "seq2")) ")" ) ($#k1_valued_0 :::"^\"::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "seq1")) ($#k1_valued_0 :::"^\"::: ) (Set (Var "k")) ")" ) ($#k3_normsp_1 :::"-"::: ) (Set "(" (Set (Var "seq2")) ($#k1_valued_0 :::"^\"::: ) (Set (Var "k")) ")" )))))) ; theorem :: CLVECT_2:89 (Bool "for" (Set (Var "X")) "being" ($#l1_csspace :::"ComplexUnitarySpace":::) (Bool "for" (Set (Var "z")) "being" ($#m1_hidden :::"Complex":::) (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set "(" (Set (Var "z")) ($#k6_clvect_1 :::"*"::: ) (Set (Var "seq")) ")" ) ($#k1_valued_0 :::"^\"::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "z")) ($#k6_clvect_1 :::"*"::: ) (Set "(" (Set (Var "seq")) ($#k1_valued_0 :::"^\"::: ) (Set (Var "k")) ")" ))))))) ; theorem :: CLVECT_2:90 (Bool "for" (Set (Var "X")) "being" ($#l1_csspace :::"ComplexUnitarySpace":::) (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "seq")) "is" ($#v1_clvect_2 :::"convergent"::: ) )) "holds" (Bool "(" (Bool (Set (Set (Var "seq")) ($#k1_valued_0 :::"^\"::: ) (Set (Var "k"))) "is" ($#v1_clvect_2 :::"convergent"::: ) ) & (Bool (Set ($#k1_clvect_2 :::"lim"::: ) (Set "(" (Set (Var "seq")) ($#k1_valued_0 :::"^\"::: ) (Set (Var "k")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_clvect_2 :::"lim"::: ) (Set (Var "seq")))) ")" )))) ; theorem :: CLVECT_2:91 (Bool "for" (Set (Var "X")) "being" ($#l1_csspace :::"ComplexUnitarySpace":::) (Bool "for" (Set (Var "seq")) "," (Set (Var "seq1")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "seq")) "is" ($#v1_clvect_2 :::"convergent"::: ) ) & (Bool "ex" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Set (Var "seq")) ($#r1_hidden :::"="::: ) (Set (Set (Var "seq1")) ($#k1_valued_0 :::"^\"::: ) (Set (Var "k")))))) "holds" (Bool (Set (Var "seq1")) "is" ($#v1_clvect_2 :::"convergent"::: ) ))) ; theorem :: CLVECT_2:92 (Bool "for" (Set (Var "X")) "being" ($#l1_csspace :::"ComplexUnitarySpace":::) (Bool "for" (Set (Var "seq")) "," (Set (Var "seq1")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "seq")) "is" ($#v2_clvect_2 :::"Cauchy"::: ) ) & (Bool "ex" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Set (Var "seq")) ($#r1_hidden :::"="::: ) (Set (Set (Var "seq1")) ($#k1_valued_0 :::"^\"::: ) (Set (Var "k")))))) "holds" (Bool (Set (Var "seq1")) "is" ($#v2_clvect_2 :::"Cauchy"::: ) ))) ; theorem :: CLVECT_2:93 (Bool "for" (Set (Var "X")) "being" ($#l1_csspace :::"ComplexUnitarySpace":::) (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "seq")) "is" ($#v2_clvect_2 :::"Cauchy"::: ) )) "holds" (Bool (Set (Set (Var "seq")) ($#k1_valued_0 :::"^\"::: ) (Set (Var "k"))) "is" ($#v2_clvect_2 :::"Cauchy"::: ) )))) ; theorem :: CLVECT_2:94 (Bool "for" (Set (Var "X")) "being" ($#l1_csspace :::"ComplexUnitarySpace":::) (Bool "for" (Set (Var "seq1")) "," (Set (Var "seq2")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "seq1")) ($#r2_clvect_2 :::"is_compared_to"::: ) (Set (Var "seq2")))) "holds" (Bool (Set (Set (Var "seq1")) ($#k1_valued_0 :::"^\"::: ) (Set (Var "k"))) ($#r2_clvect_2 :::"is_compared_to"::: ) (Set (Set (Var "seq2")) ($#k1_valued_0 :::"^\"::: ) (Set (Var "k"))))))) ; theorem :: CLVECT_2:95 (Bool "for" (Set (Var "X")) "being" ($#l1_csspace :::"ComplexUnitarySpace":::) (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "seq")) "is" ($#v3_clvect_2 :::"bounded"::: ) )) "holds" (Bool (Set (Set (Var "seq")) ($#k1_valued_0 :::"^\"::: ) (Set (Var "k"))) "is" ($#v3_clvect_2 :::"bounded"::: ) )))) ; theorem :: CLVECT_2:96 (Bool "for" (Set (Var "X")) "being" ($#l1_csspace :::"ComplexUnitarySpace":::) (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "seq")) "is" ($#v3_funct_1 :::"constant"::: ) )) "holds" (Bool (Set (Set (Var "seq")) ($#k1_valued_0 :::"^\"::: ) (Set (Var "k"))) "is" ($#v3_funct_1 :::"constant"::: ) )))) ; definitionlet "X" be ($#l1_csspace :::"ComplexUnitarySpace":::); attr "X" is :::"complete"::: means :: CLVECT_2:def 11 (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"sequence":::) "of" "X" "st" (Bool (Bool (Set (Var "seq")) "is" ($#v2_clvect_2 :::"Cauchy"::: ) )) "holds" (Bool (Set (Var "seq")) "is" ($#v1_clvect_2 :::"convergent"::: ) )); end; :: deftheorem defines :::"complete"::: CLVECT_2:def 11 : (Bool "for" (Set (Var "X")) "being" ($#l1_csspace :::"ComplexUnitarySpace":::) "holds" (Bool "(" (Bool (Set (Var "X")) "is" ($#v4_clvect_2 :::"complete"::: ) ) "iff" (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "seq")) "is" ($#v2_clvect_2 :::"Cauchy"::: ) )) "holds" (Bool (Set (Var "seq")) "is" ($#v1_clvect_2 :::"convergent"::: ) )) ")" )); theorem :: CLVECT_2:97 (Bool "for" (Set (Var "X")) "being" ($#l1_csspace :::"ComplexUnitarySpace":::) (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "X")) "is" ($#v4_clvect_2 :::"complete"::: ) ) & (Bool (Set (Var "seq")) "is" ($#v2_clvect_2 :::"Cauchy"::: ) )) "holds" (Bool (Set (Var "seq")) "is" ($#v3_clvect_2 :::"bounded"::: ) ))) ;