:: CSSPACE2  semantic presentation begin  
theorem :: CSSPACE2:1 (Bool  "("  (Bool (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set  ($#k18_csspace :::"Complex_l2_Space"::: ) ))  ($#r1_hidden :::"="::: )  (Set   ($#k11_csspace :::"the_set_of_l2ComplexSequences"::: )  )) & (Bool  "("   "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Var "x")) "is"   ($#m1_subset_1 :::"Element":::) "of" (Set  ($#k18_csspace :::"Complex_l2_Space"::: ) )) "iff" (Bool  "("  (Bool (Set (Var "x")) "is"   ($#m1_subset_1 :::"Complex_Sequence":::)) & (Bool (Set (Set  ($#k55_valued_1 :::"|."::: ) (Set  "("  ($#k2_csspace :::"seq_id"::: )  (Set (Var "x")) ")" ) ($#k55_valued_1 :::".|"::: ) )  ($#k20_valued_1 :::"(#)"::: )  (Set  ($#k55_valued_1 :::"|."::: ) (Set  "("  ($#k2_csspace :::"seq_id"::: )  (Set (Var "x")) ")" ) ($#k55_valued_1 :::".|"::: ) )) "is"   ($#v1_series_1 :::"summable"::: )  )  ")" )  ")" )  ")" ) & (Bool  "("   "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Var "x")) "is"   ($#m1_subset_1 :::"Element":::) "of" (Set  ($#k18_csspace :::"Complex_l2_Space"::: ) )) "iff" (Bool  "("  (Bool (Set (Var "x")) "is"   ($#m1_subset_1 :::"Complex_Sequence":::)) & (Bool (Set (Set  "("  ($#k2_csspace :::"seq_id"::: )  (Set (Var "x")) ")" )  ($#k19_valued_1 :::"(#)"::: )  (Set  "(" (Set  "("  ($#k2_csspace :::"seq_id"::: )  (Set (Var "x")) ")" )  ($#k2_comseq_2 :::"*'"::: )  ")" )) "is"   ($#v2_comseq_3 :::"absolutely_summable"::: )  )  ")" )  ")" )  ")" ) & (Bool (Set   ($#k4_struct_0 :::"0."::: )  (Set  ($#k18_csspace :::"Complex_l2_Space"::: ) ))  ($#r1_hidden :::"="::: )  (Set   ($#k6_csspace :::"CZeroseq"::: )  )) & (Bool  "("   "for" (Set (Var "u")) "being"   ($#m1_subset_1 :::"VECTOR":::) "of" (Set  ($#k18_csspace :::"Complex_l2_Space"::: ) ) "holds"  (Bool (Set (Var "u"))  ($#r1_hidden :::"="::: )  (Set   ($#k2_csspace :::"seq_id"::: )  (Set (Var "u"))))  ")" ) & (Bool  "("   "for" (Set (Var "u")) "," (Set (Var "v")) "being"   ($#m1_subset_1 :::"VECTOR":::) "of" (Set  ($#k18_csspace :::"Complex_l2_Space"::: ) ) "holds"  (Bool (Set (Set (Var "u"))  ($#k1_algstr_0 :::"+"::: )  (Set (Var "v")))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k2_csspace :::"seq_id"::: )  (Set (Var "u")) ")" )  ($#k1_series_1 :::"+"::: )  (Set  "("  ($#k2_csspace :::"seq_id"::: )  (Set (Var "v")) ")" )))  ")" ) & (Bool  "("   "for" (Set (Var "r")) "being"   ($#m1_hidden :::"Complex":::)  (Bool  "for" (Set (Var "u")) "being"   ($#m1_subset_1 :::"VECTOR":::) "of" (Set  ($#k18_csspace :::"Complex_l2_Space"::: ) ) "holds"  (Bool (Set (Set (Var "r"))  ($#k1_clvect_1 :::"*"::: )  (Set (Var "u")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "r"))  ($#k25_valued_1 :::"(#)"::: )  (Set  "("  ($#k2_csspace :::"seq_id"::: )  (Set (Var "u")) ")" ))))  ")" ) & (Bool  "("   "for" (Set (Var "u")) "being"   ($#m1_subset_1 :::"VECTOR":::) "of" (Set  ($#k18_csspace :::"Complex_l2_Space"::: ) ) "holds"   (Bool  "("  (Bool (Set   ($#k4_algstr_0 :::"-"::: )  (Set (Var "u")))  ($#r1_hidden :::"="::: )  (Set   ($#k31_valued_1 :::"-"::: )  (Set  "("  ($#k2_csspace :::"seq_id"::: )  (Set (Var "u")) ")" ))) & (Bool (Set   ($#k2_csspace :::"seq_id"::: )  (Set  "("  ($#k4_algstr_0 :::"-"::: )  (Set (Var "u")) ")" ))  ($#r2_funct_2 :::"="::: )  (Set   ($#k31_valued_1 :::"-"::: )  (Set  "("  ($#k2_csspace :::"seq_id"::: )  (Set (Var "u")) ")" )))  ")" )  ")" ) & (Bool  "("   "for" (Set (Var "u")) "," (Set (Var "v")) "being"   ($#m1_subset_1 :::"VECTOR":::) "of" (Set  ($#k18_csspace :::"Complex_l2_Space"::: ) ) "holds"  (Bool (Set (Set (Var "u"))  ($#k5_algstr_0 :::"-"::: )  (Set (Var "v")))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k2_csspace :::"seq_id"::: )  (Set (Var "u")) ")" )  ($#k46_valued_1 :::"-"::: )  (Set  "("  ($#k2_csspace :::"seq_id"::: )  (Set (Var "v")) ")" )))  ")" ) & (Bool  "("   "for" (Set (Var "v")) "," (Set (Var "w")) "being"   ($#m1_subset_1 :::"VECTOR":::) "of" (Set  ($#k18_csspace :::"Complex_l2_Space"::: ) ) "holds"   (Bool  "("  (Bool (Set (Set  ($#k55_valued_1 :::"|."::: ) (Set  "("  ($#k2_csspace :::"seq_id"::: )  (Set (Var "v")) ")" ) ($#k55_valued_1 :::".|"::: ) )  ($#k20_valued_1 :::"(#)"::: )  (Set  ($#k55_valued_1 :::"|."::: ) (Set  "("  ($#k2_csspace :::"seq_id"::: )  (Set (Var "w")) ")" ) ($#k55_valued_1 :::".|"::: ) )) "is"   ($#v1_series_1 :::"summable"::: )  ) & (Bool  "("   "for" (Set (Var "v")) "," (Set (Var "w")) "being"   ($#m1_subset_1 :::"VECTOR":::) "of" (Set  ($#k18_csspace :::"Complex_l2_Space"::: ) ) "holds"  (Bool (Set (Set (Var "v"))  ($#k12_csspace :::".|."::: )  (Set (Var "w")))  ($#r1_hidden :::"="::: )  (Set   ($#k11_comseq_3 :::"Sum"::: )  (Set  "(" (Set  "("  ($#k2_csspace :::"seq_id"::: )  (Set (Var "v")) ")" )  ($#k19_valued_1 :::"(#)"::: )  (Set  "(" (Set  "("  ($#k2_csspace :::"seq_id"::: )  (Set (Var "w")) ")" )  ($#k2_comseq_2 :::"*'"::: )  ")" ) ")" )))  ")" )  ")" )  ")" )  ")" ) ; 
 
theorem :: CSSPACE2:2 (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  ($#k18_csspace :::"Complex_l2_Space"::: ) )  (Bool  "for" (Set (Var "a")) "being"   ($#m1_hidden :::"Complex":::) "holds"   (Bool  "("   "("  (Bool (Bool (Set (Set (Var "x"))  ($#k12_csspace :::".|."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "implies" (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set   ($#k4_struct_0 :::"0."::: )  (Set  ($#k18_csspace :::"Complex_l2_Space"::: ) )))  ")"  &  "("  (Bool (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set   ($#k4_struct_0 :::"0."::: )  (Set  ($#k18_csspace :::"Complex_l2_Space"::: ) )))) "implies" (Bool (Set (Set (Var "x"))  ($#k12_csspace :::".|."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")"  & (Bool (Set   ($#k3_complex1 :::"Re"::: )  (Set  "(" (Set (Var "x"))  ($#k12_csspace :::".|."::: )  (Set (Var "x")) ")" ))  ($#r1_xxreal_0 :::">="::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set   ($#k4_complex1 :::"Im"::: )  (Set  "(" (Set (Var "x"))  ($#k12_csspace :::".|."::: )  (Set (Var "x")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Set (Var "x"))  ($#k12_csspace :::".|."::: )  (Set (Var "y")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "y"))  ($#k12_csspace :::".|."::: )  (Set (Var "x")) ")" )  ($#k15_complex1 :::"*'"::: )  )) & (Bool (Set (Set  "(" (Set (Var "x"))  ($#k1_algstr_0 :::"+"::: )  (Set (Var "y")) ")" )  ($#k12_csspace :::".|."::: )  (Set (Var "z")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "x"))  ($#k12_csspace :::".|."::: )  (Set (Var "z")) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" (Set (Var "y"))  ($#k12_csspace :::".|."::: )  (Set (Var "z")) ")" ))) & (Bool (Set (Set  "(" (Set (Var "a"))  ($#k1_clvect_1 :::"*"::: )  (Set (Var "x")) ")" )  ($#k12_csspace :::".|."::: )  (Set (Var "y")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "a"))  ($#k3_xcmplx_0 :::"*"::: )  (Set  "(" (Set (Var "x"))  ($#k12_csspace :::".|."::: )  (Set (Var "y")) ")" )))  ")" ))) ; 
 registration
cluster (Set   ($#k18_csspace :::"Complex_l2_Space"::: )  ) ->   ($#v2_csspace :::"ComplexUnitarySpace-like"::: )   ; 
end; registration
cluster (Set   ($#k18_csspace :::"Complex_l2_Space"::: )  ) ->   ($#v4_clvect_2 :::"complete"::: )   ; 
end; registration
cluster bbbadV2_STRUCT_0()   ($#v13_algstr_0 :::"right_complementable"::: )   bbbadV2_RLVECT_1() bbbadV3_RLVECT_1() bbbadV4_RLVECT_1()   ($#v2_clvect_1 :::"vector-distributive"::: )     ($#v3_clvect_1 :::"scalar-distributive"::: )     ($#v4_clvect_1 :::"scalar-associative"::: )     ($#v5_clvect_1 :::"scalar-unital"::: )     ($#v2_csspace :::"ComplexUnitarySpace-like"::: )     ($#v4_clvect_2 :::"complete"::: )    for    ($#l1_csspace :::"CUNITSTR"::: )  ; 
end; definitionmode ComplexHilbertSpace is   ($#v4_clvect_2 :::"complete"::: )    ($#l1_csspace :::"ComplexUnitarySpace":::); end; begin  
theorem :: CSSPACE2:3 (Bool  "for" (Set (Var "z1")) "," (Set (Var "z2")) "being"   ($#m1_hidden :::"Complex":::)  "st" (Bool (Bool (Set (Set  "("  ($#k3_complex1 :::"Re"::: )  (Set (Var "z1")) ")" )  ($#k8_real_1 :::"*"::: )  (Set  "("  ($#k4_complex1 :::"Im"::: )  (Set (Var "z2")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k3_complex1 :::"Re"::: )  (Set (Var "z2")) ")" )  ($#k8_real_1 :::"*"::: )  (Set  "("  ($#k4_complex1 :::"Im"::: )  (Set (Var "z1")) ")" ))) & (Bool (Set (Set  "(" (Set  "("  ($#k3_complex1 :::"Re"::: )  (Set (Var "z1")) ")" )  ($#k8_real_1 :::"*"::: )  (Set  "("  ($#k3_complex1 :::"Re"::: )  (Set (Var "z2")) ")" ) ")" )  ($#k7_real_1 :::"+"::: )  (Set  "(" (Set  "("  ($#k4_complex1 :::"Im"::: )  (Set (Var "z1")) ")" )  ($#k8_real_1 :::"*"::: )  (Set  "("  ($#k4_complex1 :::"Im"::: )  (Set (Var "z2")) ")" ) ")" ))  ($#r1_xxreal_0 :::">="::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set  ($#k17_complex1 :::"|."::: ) (Set  "(" (Set (Var "z1"))  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "z2")) ")" ) ($#k17_complex1 :::".|"::: ) )  ($#r1_hidden :::"="::: )  (Set (Set  ($#k17_complex1 :::"|."::: ) (Set (Var "z1")) ($#k17_complex1 :::".|"::: ) )  ($#k7_real_1 :::"+"::: )  (Set  ($#k17_complex1 :::"|."::: ) (Set (Var "z2")) ($#k17_complex1 :::".|"::: ) )))) ; 
 
theorem :: CSSPACE2:4 (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#m1_hidden :::"Complex":::) "holds"  (Bool (Set (Num 2)  ($#k8_real_1 :::"*"::: )  (Set  ($#k17_complex1 :::"|."::: ) (Set  "(" (Set (Var "x"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "y")) ")" ) ($#k17_complex1 :::".|"::: ) ))  ($#r1_xxreal_0 :::"<="::: )  (Set (Set  "(" (Set  ($#k17_complex1 :::"|."::: ) (Set (Var "x")) ($#k17_complex1 :::".|"::: ) )  ($#k5_square_1 :::"^2"::: )  ")" )  ($#k7_real_1 :::"+"::: )  (Set  "(" (Set  ($#k17_complex1 :::"|."::: ) (Set (Var "y")) ($#k17_complex1 :::".|"::: ) )  ($#k5_square_1 :::"^2"::: )  ")" )))) ; 
 
theorem :: CSSPACE2:5 (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#m1_hidden :::"Complex":::) "holds"   (Bool  "("  (Bool (Set (Set  ($#k17_complex1 :::"|."::: ) (Set  "(" (Set (Var "x"))  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "y")) ")" ) ($#k17_complex1 :::".|"::: ) )  ($#k8_real_1 :::"*"::: )  (Set  ($#k17_complex1 :::"|."::: ) (Set  "(" (Set (Var "x"))  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "y")) ")" ) ($#k17_complex1 :::".|"::: ) ))  ($#r1_xxreal_0 :::"<="::: )  (Set (Set  "(" (Set  "(" (Num 2)  ($#k8_real_1 :::"*"::: )  (Set  ($#k17_complex1 :::"|."::: ) (Set (Var "x")) ($#k17_complex1 :::".|"::: ) ) ")" )  ($#k8_real_1 :::"*"::: )  (Set  ($#k17_complex1 :::"|."::: ) (Set (Var "x")) ($#k17_complex1 :::".|"::: ) ) ")" )  ($#k7_real_1 :::"+"::: )  (Set  "(" (Set  "(" (Num 2)  ($#k8_real_1 :::"*"::: )  (Set  ($#k17_complex1 :::"|."::: ) (Set (Var "y")) ($#k17_complex1 :::".|"::: ) ) ")" )  ($#k8_real_1 :::"*"::: )  (Set  ($#k17_complex1 :::"|."::: ) (Set (Var "y")) ($#k17_complex1 :::".|"::: ) ) ")" ))) & (Bool (Set (Set  ($#k17_complex1 :::"|."::: ) (Set (Var "x")) ($#k17_complex1 :::".|"::: ) )  ($#k8_real_1 :::"*"::: )  (Set  ($#k17_complex1 :::"|."::: ) (Set (Var "x")) ($#k17_complex1 :::".|"::: ) ))  ($#r1_xxreal_0 :::"<="::: )  (Set (Set  "(" (Set  "(" (Num 2)  ($#k8_real_1 :::"*"::: )  (Set  ($#k17_complex1 :::"|."::: ) (Set  "(" (Set (Var "x"))  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "y")) ")" ) ($#k17_complex1 :::".|"::: ) ) ")" )  ($#k8_real_1 :::"*"::: )  (Set  ($#k17_complex1 :::"|."::: ) (Set  "(" (Set (Var "x"))  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "y")) ")" ) ($#k17_complex1 :::".|"::: ) ) ")" )  ($#k7_real_1 :::"+"::: )  (Set  "(" (Set  "(" (Num 2)  ($#k8_real_1 :::"*"::: )  (Set  ($#k17_complex1 :::"|."::: ) (Set (Var "y")) ($#k17_complex1 :::".|"::: ) ) ")" )  ($#k8_real_1 :::"*"::: )  (Set  ($#k17_complex1 :::"|."::: ) (Set (Var "y")) ($#k17_complex1 :::".|"::: ) ) ")" )))  ")" )) ; 
 
theorem :: CSSPACE2:6 canceled; 
 
theorem :: CSSPACE2:7 (Bool  "for" (Set (Var "seq")) "being"   ($#m1_subset_1 :::"Complex_Sequence":::) "holds"  (Bool (Set   ($#k10_comseq_3 :::"Partial_Sums"::: )  (Set  "(" (Set (Var "seq"))  ($#k2_comseq_2 :::"*'"::: )  ")" ))  ($#r2_funct_2 :::"="::: )  (Set (Set  "("  ($#k10_comseq_3 :::"Partial_Sums"::: )  (Set (Var "seq")) ")" )  ($#k2_comseq_2 :::"*'"::: )  ))) ; 
 
theorem :: CSSPACE2:8 (Bool  "for" (Set (Var "seq")) "being"   ($#m1_subset_1 :::"Complex_Sequence":::)  (Bool  "for" (Set (Var "n")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool  "("   "for" (Set (Var "i")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"   (Bool  "("  (Bool (Set (Set  "("  ($#k7_comseq_3 :::"Re"::: )  (Set (Var "seq")) ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "i")))  ($#r1_xxreal_0 :::">="::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Set  "("  ($#k8_comseq_3 :::"Im"::: )  (Set (Var "seq")) ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "i")))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")" )  ")" )) "holds"  (Bool (Set (Set  ($#k55_valued_1 :::"|."::: ) (Set  "("  ($#k10_comseq_3 :::"Partial_Sums"::: )  (Set (Var "seq")) ")" ) ($#k55_valued_1 :::".|"::: ) )  ($#k1_seq_1 :::"."::: )  (Set (Var "n")))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k3_series_1 :::"Partial_Sums"::: )  (Set  ($#k55_valued_1 :::"|."::: ) (Set (Var "seq")) ($#k55_valued_1 :::".|"::: ) ) ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "n")))))) ; 
 
theorem :: CSSPACE2:9 (Bool  "for" (Set (Var "seq")) "being"   ($#m1_subset_1 :::"Complex_Sequence":::)  "st" (Bool (Bool (Set (Var "seq")) "is"   ($#v1_comseq_3 :::"summable"::: )  )) "holds"  (Bool (Set   ($#k11_comseq_3 :::"Sum"::: )  (Set  "(" (Set (Var "seq"))  ($#k2_comseq_2 :::"*'"::: )  ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k11_comseq_3 :::"Sum"::: )  (Set (Var "seq")) ")" )  ($#k15_complex1 :::"*'"::: )  ))) ; 
 
theorem :: CSSPACE2:10 (Bool  "for" (Set (Var "seq")) "being"   ($#m1_subset_1 :::"Complex_Sequence":::)  "st" (Bool (Bool (Set (Var "seq")) "is"   ($#v2_comseq_3 :::"absolutely_summable"::: )  )) "holds"  (Bool (Set  ($#k17_complex1 :::"|."::: ) (Set  "("  ($#k11_comseq_3 :::"Sum"::: )  (Set (Var "seq")) ")" ) ($#k17_complex1 :::".|"::: ) )  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k4_series_1 :::"Sum"::: )  (Set  ($#k55_valued_1 :::"|."::: ) (Set (Var "seq")) ($#k55_valued_1 :::".|"::: ) )))) ; 
 
theorem :: CSSPACE2:11 (Bool  "for" (Set (Var "seq")) "being"   ($#m1_subset_1 :::"Complex_Sequence":::)  "st" (Bool (Bool (Set (Var "seq")) "is"   ($#v1_comseq_3 :::"summable"::: )  ) & (Bool  "("   "for" (Set (Var "n")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"   (Bool  "("  (Bool (Set (Set  "("  ($#k7_comseq_3 :::"Re"::: )  (Set (Var "seq")) ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "n")))  ($#r1_xxreal_0 :::">="::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Set  "("  ($#k8_comseq_3 :::"Im"::: )  (Set (Var "seq")) ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "n")))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")" )  ")" )) "holds"  (Bool (Set  ($#k17_complex1 :::"|."::: ) (Set  "("  ($#k11_comseq_3 :::"Sum"::: )  (Set (Var "seq")) ")" ) ($#k17_complex1 :::".|"::: ) )  ($#r1_hidden :::"="::: )  (Set   ($#k4_series_1 :::"Sum"::: )  (Set  ($#k55_valued_1 :::"|."::: ) (Set (Var "seq")) ($#k55_valued_1 :::".|"::: ) )))) ; 
 
theorem :: CSSPACE2:12 (Bool  "for" (Set (Var "seq")) "being"   ($#m1_subset_1 :::"Complex_Sequence":::)  (Bool  "for" (Set (Var "n")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"   (Bool  "("  (Bool (Set (Set  "("  ($#k7_comseq_3 :::"Re"::: )  (Set  "(" (Set (Var "seq"))  ($#k19_valued_1 :::"(#)"::: )  (Set  "(" (Set (Var "seq"))  ($#k2_comseq_2 :::"*'"::: )  ")" ) ")" ) ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "n")))  ($#r1_xxreal_0 :::">="::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Set  "("  ($#k8_comseq_3 :::"Im"::: )  (Set  "(" (Set (Var "seq"))  ($#k19_valued_1 :::"(#)"::: )  (Set  "(" (Set (Var "seq"))  ($#k2_comseq_2 :::"*'"::: )  ")" ) ")" ) ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "n")))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")" ))) ; 
 
theorem :: CSSPACE2:13 (Bool  "for" (Set (Var "seq")) "being"   ($#m1_subset_1 :::"Complex_Sequence":::)  "st" (Bool (Bool (Set (Var "seq")) "is"   ($#v2_comseq_3 :::"absolutely_summable"::: )  ) & (Bool (Set   ($#k4_series_1 :::"Sum"::: )  (Set  ($#k55_valued_1 :::"|."::: ) (Set (Var "seq")) ($#k55_valued_1 :::".|"::: ) ))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool  "for" (Set (Var "n")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"  (Bool (Set (Set (Var "seq"))  ($#k3_funct_2 :::"."::: )  (Set (Var "n")))  ($#r1_hidden :::"="::: )  (Set   ($#k5_complex1 :::"0c"::: )  )))) ; 
 
theorem :: CSSPACE2:14 (Bool  "for" (Set (Var "seq")) "being"   ($#m1_subset_1 :::"Complex_Sequence":::) "holds"  (Bool (Set  ($#k55_valued_1 :::"|."::: ) (Set (Var "seq")) ($#k55_valued_1 :::".|"::: ) )  ($#r2_funct_2 :::"="::: )  (Set  ($#k55_valued_1 :::"|."::: ) (Set  "(" (Set (Var "seq"))  ($#k2_comseq_2 :::"*'"::: )  ")" ) ($#k55_valued_1 :::".|"::: ) ))) ; 
 
theorem :: CSSPACE2:15 (Bool  "for" (Set (Var "c")) "being"   ($#m1_hidden :::"Complex":::)  (Bool  "for" (Set (Var "seq")) "being"   ($#m1_subset_1 :::"Complex_Sequence":::)  "st" (Bool (Bool (Set (Var "seq")) "is"   ($#v2_comseq_2 :::"convergent"::: )  )) "holds"  (Bool  "for" (Set (Var "rseq")) "being"   ($#m1_subset_1 :::"Real_Sequence":::)  "st" (Bool (Bool  "("   "for" (Set (Var "m")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"  (Bool (Set (Set (Var "rseq"))  ($#k1_seq_1 :::"."::: )  (Set (Var "m")))  ($#r1_hidden :::"="::: )  (Set (Set  ($#k17_complex1 :::"|."::: ) (Set  "(" (Set  "(" (Set (Var "seq"))  ($#k3_funct_2 :::"."::: )  (Set (Var "m")) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "c")) ")" ) ($#k17_complex1 :::".|"::: ) )  ($#k8_real_1 :::"*"::: )  (Set  ($#k17_complex1 :::"|."::: ) (Set  "(" (Set  "(" (Set (Var "seq"))  ($#k3_funct_2 :::"."::: )  (Set (Var "m")) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "c")) ")" ) ($#k17_complex1 :::".|"::: ) )))  ")" )) "holds"  (Bool  "("  (Bool (Set (Var "rseq")) "is"   ($#v2_comseq_2 :::"convergent"::: )  ) & (Bool (Set   ($#k2_seq_2 :::"lim"::: )  (Set (Var "rseq")))  ($#r1_hidden :::"="::: )  (Set (Set  ($#k17_complex1 :::"|."::: ) (Set  "(" (Set  "("  ($#k3_comseq_2 :::"lim"::: )  (Set (Var "seq")) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "c")) ")" ) ($#k17_complex1 :::".|"::: ) )  ($#k8_real_1 :::"*"::: )  (Set  ($#k17_complex1 :::"|."::: ) (Set  "(" (Set  "("  ($#k3_comseq_2 :::"lim"::: )  (Set (Var "seq")) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "c")) ")" ) ($#k17_complex1 :::".|"::: ) )))  ")" )))) ; 
 
theorem :: CSSPACE2:16 (Bool  "for" (Set (Var "c")) "being"   ($#m1_hidden :::"Complex":::)  (Bool  "for" (Set (Var "seq1")) "being"   ($#m1_subset_1 :::"Real_Sequence":::)  (Bool  "for" (Set (Var "seq")) "being"   ($#m1_subset_1 :::"Complex_Sequence":::)  "st" (Bool (Bool (Set (Var "seq")) "is"   ($#v2_comseq_2 :::"convergent"::: )  ) & (Bool (Set (Var "seq1")) "is"   ($#v2_comseq_2 :::"convergent"::: )  )) "holds"  (Bool  "for" (Set (Var "rseq")) "being"   ($#m1_subset_1 :::"Real_Sequence":::)  "st" (Bool (Bool  "("   "for" (Set (Var "i")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"  (Bool (Set (Set (Var "rseq"))  ($#k1_seq_1 :::"."::: )  (Set (Var "i")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  ($#k17_complex1 :::"|."::: ) (Set  "(" (Set  "(" (Set (Var "seq"))  ($#k3_funct_2 :::"."::: )  (Set (Var "i")) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "c")) ")" ) ($#k17_complex1 :::".|"::: ) )  ($#k8_real_1 :::"*"::: )  (Set  ($#k17_complex1 :::"|."::: ) (Set  "(" (Set  "(" (Set (Var "seq"))  ($#k3_funct_2 :::"."::: )  (Set (Var "i")) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "c")) ")" ) ($#k17_complex1 :::".|"::: ) ) ")" )  ($#k7_real_1 :::"+"::: )  (Set  "(" (Set (Var "seq1"))  ($#k1_seq_1 :::"."::: )  (Set (Var "i")) ")" )))  ")" )) "holds"  (Bool  "("  (Bool (Set (Var "rseq")) "is"   ($#v2_comseq_2 :::"convergent"::: )  ) & (Bool (Set   ($#k2_seq_2 :::"lim"::: )  (Set (Var "rseq")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  ($#k17_complex1 :::"|."::: ) (Set  "(" (Set  "("  ($#k3_comseq_2 :::"lim"::: )  (Set (Var "seq")) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "c")) ")" ) ($#k17_complex1 :::".|"::: ) )  ($#k8_real_1 :::"*"::: )  (Set  ($#k17_complex1 :::"|."::: ) (Set  "(" (Set  "("  ($#k3_comseq_2 :::"lim"::: )  (Set (Var "seq")) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "c")) ")" ) ($#k17_complex1 :::".|"::: ) ) ")" )  ($#k7_real_1 :::"+"::: )  (Set  "("  ($#k2_seq_2 :::"lim"::: )  (Set (Var "seq1")) ")" )))  ")" ))))) ; 
 
theorem :: CSSPACE2:17 (Bool  "for" (Set (Var "c")) "being"   ($#m1_hidden :::"Complex":::)  (Bool  "for" (Set (Var "seq")) "being"   ($#m1_subset_1 :::"Complex_Sequence":::)  "st" (Bool (Bool (Set (Var "seq")) "is"   ($#v2_comseq_2 :::"convergent"::: )  )) "holds"  (Bool  "for" (Set (Var "rseq")) "being"   ($#m1_subset_1 :::"Real_Sequence":::)  "st" (Bool (Bool  "("   "for" (Set (Var "m")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"  (Bool (Set (Set (Var "rseq"))  ($#k1_seq_1 :::"."::: )  (Set (Var "m")))  ($#r1_hidden :::"="::: )  (Set (Set  ($#k17_complex1 :::"|."::: ) (Set  "(" (Set  "(" (Set (Var "seq"))  ($#k3_funct_2 :::"."::: )  (Set (Var "m")) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "c")) ")" ) ($#k17_complex1 :::".|"::: ) )  ($#k8_real_1 :::"*"::: )  (Set  ($#k17_complex1 :::"|."::: ) (Set  "(" (Set  "(" (Set (Var "seq"))  ($#k3_funct_2 :::"."::: )  (Set (Var "m")) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "c")) ")" ) ($#k17_complex1 :::".|"::: ) )))  ")" )) "holds"  (Bool  "("  (Bool (Set (Var "rseq")) "is"   ($#v2_comseq_2 :::"convergent"::: )  ) & (Bool (Set   ($#k2_seq_2 :::"lim"::: )  (Set (Var "rseq")))  ($#r1_hidden :::"="::: )  (Set (Set  ($#k17_complex1 :::"|."::: ) (Set  "(" (Set  "("  ($#k3_comseq_2 :::"lim"::: )  (Set (Var "seq")) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "c")) ")" ) ($#k17_complex1 :::".|"::: ) )  ($#k8_real_1 :::"*"::: )  (Set  ($#k17_complex1 :::"|."::: ) (Set  "(" (Set  "("  ($#k3_comseq_2 :::"lim"::: )  (Set (Var "seq")) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "c")) ")" ) ($#k17_complex1 :::".|"::: ) )))  ")" )))) ; 
 
theorem :: CSSPACE2:18 (Bool  "for" (Set (Var "c")) "being"   ($#m1_hidden :::"Complex":::)  (Bool  "for" (Set (Var "seq1")) "being"   ($#m1_subset_1 :::"Real_Sequence":::)  (Bool  "for" (Set (Var "seq")) "being"   ($#m1_subset_1 :::"Complex_Sequence":::)  "st" (Bool (Bool (Set (Var "seq")) "is"   ($#v2_comseq_2 :::"convergent"::: )  ) & (Bool (Set (Var "seq1")) "is"   ($#v2_comseq_2 :::"convergent"::: )  )) "holds"  (Bool  "for" (Set (Var "rseq")) "being"   ($#m1_subset_1 :::"Real_Sequence":::)  "st" (Bool (Bool  "("   "for" (Set (Var "i")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"  (Bool (Set (Set (Var "rseq"))  ($#k1_seq_1 :::"."::: )  (Set (Var "i")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  ($#k17_complex1 :::"|."::: ) (Set  "(" (Set  "(" (Set (Var "seq"))  ($#k3_funct_2 :::"."::: )  (Set (Var "i")) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "c")) ")" ) ($#k17_complex1 :::".|"::: ) )  ($#k8_real_1 :::"*"::: )  (Set  ($#k17_complex1 :::"|."::: ) (Set  "(" (Set  "(" (Set (Var "seq"))  ($#k3_funct_2 :::"."::: )  (Set (Var "i")) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "c")) ")" ) ($#k17_complex1 :::".|"::: ) ) ")" )  ($#k7_real_1 :::"+"::: )  (Set  "(" (Set (Var "seq1"))  ($#k1_seq_1 :::"."::: )  (Set (Var "i")) ")" )))  ")" )) "holds"  (Bool  "("  (Bool (Set (Var "rseq")) "is"   ($#v2_comseq_2 :::"convergent"::: )  ) & (Bool (Set   ($#k2_seq_2 :::"lim"::: )  (Set (Var "rseq")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  ($#k17_complex1 :::"|."::: ) (Set  "(" (Set  "("  ($#k3_comseq_2 :::"lim"::: )  (Set (Var "seq")) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "c")) ")" ) ($#k17_complex1 :::".|"::: ) )  ($#k8_real_1 :::"*"::: )  (Set  ($#k17_complex1 :::"|."::: ) (Set  "(" (Set  "("  ($#k3_comseq_2 :::"lim"::: )  (Set (Var "seq")) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "c")) ")" ) ($#k17_complex1 :::".|"::: ) ) ")" )  ($#k7_real_1 :::"+"::: )  (Set  "("  ($#k2_seq_2 :::"lim"::: )  (Set (Var "seq1")) ")" )))  ")" ))))) ;