:: RSSPACE2  semantic presentation begin  
theorem :: RSSPACE2:1 (Bool  "("  (Bool (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set  ($#k13_rsspace :::"l2_Space"::: ) ))  ($#r1_hidden :::"="::: )  (Set   ($#k11_rsspace :::"the_set_of_l2RealSequences"::: )  )) & (Bool  "("   "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Var "x")) "is"   ($#m1_subset_1 :::"VECTOR":::) "of" (Set  ($#k13_rsspace :::"l2_Space"::: ) )) "iff" (Bool  "("  (Bool (Set (Var "x")) "is"   ($#m1_subset_1 :::"Real_Sequence":::)) & (Bool (Set (Set  "("  ($#k2_rsspace :::"seq_id"::: )  (Set (Var "x")) ")" )  ($#k20_valued_1 :::"(#)"::: )  (Set  "("  ($#k2_rsspace :::"seq_id"::: )  (Set (Var "x")) ")" )) "is"   ($#v1_series_1 :::"summable"::: )  )  ")" )  ")" )  ")" ) & (Bool (Set   ($#k4_struct_0 :::"0."::: )  (Set  ($#k13_rsspace :::"l2_Space"::: ) ))  ($#r1_hidden :::"="::: )  (Set   ($#k6_rsspace :::"Zeroseq"::: )  )) & (Bool  "("   "for" (Set (Var "u")) "being"   ($#m1_subset_1 :::"VECTOR":::) "of" (Set  ($#k13_rsspace :::"l2_Space"::: ) ) "holds"  (Bool (Set (Var "u"))  ($#r1_hidden :::"="::: )  (Set   ($#k2_rsspace :::"seq_id"::: )  (Set (Var "u"))))  ")" ) & (Bool  "("   "for" (Set (Var "u")) "," (Set (Var "v")) "being"   ($#m1_subset_1 :::"VECTOR":::) "of" (Set  ($#k13_rsspace :::"l2_Space"::: ) ) "holds"  (Bool (Set (Set (Var "u"))  ($#k3_rlvect_1 :::"+"::: )  (Set (Var "v")))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k2_rsspace :::"seq_id"::: )  (Set (Var "u")) ")" )  ($#k1_series_1 :::"+"::: )  (Set  "("  ($#k2_rsspace :::"seq_id"::: )  (Set (Var "v")) ")" )))  ")" ) & (Bool  "("   "for" (Set (Var "r")) "being"   ($#m1_subset_1 :::"Real":::)  (Bool  "for" (Set (Var "u")) "being"   ($#m1_subset_1 :::"VECTOR":::) "of" (Set  ($#k13_rsspace :::"l2_Space"::: ) ) "holds"  (Bool (Set (Set (Var "r"))  ($#k1_rlvect_1 :::"*"::: )  (Set (Var "u")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "r"))  ($#k26_valued_1 :::"(#)"::: )  (Set  "("  ($#k2_rsspace :::"seq_id"::: )  (Set (Var "u")) ")" ))))  ")" ) & (Bool  "("   "for" (Set (Var "u")) "being"   ($#m1_subset_1 :::"VECTOR":::) "of" (Set  ($#k13_rsspace :::"l2_Space"::: ) ) "holds"   (Bool  "("  (Bool (Set   ($#k4_algstr_0 :::"-"::: )  (Set (Var "u")))  ($#r1_hidden :::"="::: )  (Set   ($#k32_valued_1 :::"-"::: )  (Set  "("  ($#k2_rsspace :::"seq_id"::: )  (Set (Var "u")) ")" ))) & (Bool (Set   ($#k2_rsspace :::"seq_id"::: )  (Set  "("  ($#k4_algstr_0 :::"-"::: )  (Set (Var "u")) ")" ))  ($#r2_funct_2 :::"="::: )  (Set   ($#k32_valued_1 :::"-"::: )  (Set  "("  ($#k2_rsspace :::"seq_id"::: )  (Set (Var "u")) ")" )))  ")" )  ")" ) & (Bool  "("   "for" (Set (Var "u")) "," (Set (Var "v")) "being"   ($#m1_subset_1 :::"VECTOR":::) "of" (Set  ($#k13_rsspace :::"l2_Space"::: ) ) "holds"  (Bool (Set (Set (Var "u"))  ($#k5_algstr_0 :::"-"::: )  (Set (Var "v")))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k2_rsspace :::"seq_id"::: )  (Set (Var "u")) ")" )  ($#k47_valued_1 :::"-"::: )  (Set  "("  ($#k2_rsspace :::"seq_id"::: )  (Set (Var "v")) ")" )))  ")" ) & (Bool  "("   "for" (Set (Var "v")) "," (Set (Var "w")) "being"   ($#m1_subset_1 :::"VECTOR":::) "of" (Set  ($#k13_rsspace :::"l2_Space"::: ) ) "holds"   (Bool  "("  (Bool (Set (Set  "("  ($#k2_rsspace :::"seq_id"::: )  (Set (Var "v")) ")" )  ($#k20_valued_1 :::"(#)"::: )  (Set  "("  ($#k2_rsspace :::"seq_id"::: )  (Set (Var "w")) ")" )) "is"   ($#v1_series_1 :::"summable"::: )  ) & (Bool  "("   "for" (Set (Var "v")) "," (Set (Var "w")) "being"   ($#m1_subset_1 :::"VECTOR":::) "of" (Set  ($#k13_rsspace :::"l2_Space"::: ) ) "holds"  (Bool (Set (Set (Var "v"))  ($#k1_bhsp_1 :::".|."::: )  (Set (Var "w")))  ($#r1_hidden :::"="::: )  (Set   ($#k4_series_1 :::"Sum"::: )  (Set  "(" (Set  "("  ($#k2_rsspace :::"seq_id"::: )  (Set (Var "v")) ")" )  ($#k20_valued_1 :::"(#)"::: )  (Set  "("  ($#k2_rsspace :::"seq_id"::: )  (Set (Var "w")) ")" ) ")" )))  ")" )  ")" )  ")" )  ")" ) ; 
 
theorem :: RSSPACE2:2 (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  ($#k13_rsspace :::"l2_Space"::: ) )  (Bool  "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Real":::) "holds"   (Bool  "("   "("  (Bool (Bool (Set (Set (Var "x"))  ($#k1_bhsp_1 :::".|."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "implies" (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set   ($#k4_struct_0 :::"0."::: )  (Set  ($#k13_rsspace :::"l2_Space"::: ) )))  ")"  &  "("  (Bool (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set   ($#k4_struct_0 :::"0."::: )  (Set  ($#k13_rsspace :::"l2_Space"::: ) )))) "implies" (Bool (Set (Set (Var "x"))  ($#k1_bhsp_1 :::".|."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")"  & (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<="::: )  (Set (Set (Var "x"))  ($#k1_bhsp_1 :::".|."::: )  (Set (Var "x")))) & (Bool (Set (Set (Var "x"))  ($#k1_bhsp_1 :::".|."::: )  (Set (Var "y")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "y"))  ($#k1_bhsp_1 :::".|."::: )  (Set (Var "x")))) & (Bool (Set (Set  "(" (Set (Var "x"))  ($#k3_rlvect_1 :::"+"::: )  (Set (Var "y")) ")" )  ($#k1_bhsp_1 :::".|."::: )  (Set (Var "z")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "x"))  ($#k1_bhsp_1 :::".|."::: )  (Set (Var "z")) ")" )  ($#k7_real_1 :::"+"::: )  (Set  "(" (Set (Var "y"))  ($#k1_bhsp_1 :::".|."::: )  (Set (Var "z")) ")" ))) & (Bool (Set (Set  "(" (Set (Var "a"))  ($#k1_rlvect_1 :::"*"::: )  (Set (Var "x")) ")" )  ($#k1_bhsp_1 :::".|."::: )  (Set (Var "y")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "a"))  ($#k8_real_1 :::"*"::: )  (Set  "(" (Set (Var "x"))  ($#k1_bhsp_1 :::".|."::: )  (Set (Var "y")) ")" )))  ")" ))) ; 
 registration
cluster (Set   ($#k13_rsspace :::"l2_Space"::: )  ) ->   ($#v2_bhsp_1 :::"RealUnitarySpace-like"::: )   ; 
end; registration
cluster (Set   ($#k13_rsspace :::"l2_Space"::: )  ) ->   ($#v3_bhsp_3 :::"complete"::: )   ; 
end; registration
cluster bbbadV2_STRUCT_0()   ($#v13_algstr_0 :::"right_complementable"::: )     ($#v2_rlvect_1 :::"Abelian"::: )     ($#v3_rlvect_1 :::"add-associative"::: )     ($#v4_rlvect_1 :::"right_zeroed"::: )     ($#v5_rlvect_1 :::"vector-distributive"::: )     ($#v6_rlvect_1 :::"scalar-distributive"::: )     ($#v7_rlvect_1 :::"scalar-associative"::: )     ($#v8_rlvect_1 :::"scalar-unital"::: )     ($#v2_bhsp_1 :::"RealUnitarySpace-like"::: )     ($#v3_bhsp_3 :::"complete"::: )    for    ($#l1_bhsp_1 :::"UNITSTR"::: )  ; 
end; definitionmode RealHilbertSpace is   ($#v3_bhsp_3 :::"complete"::: )    ($#l1_bhsp_1 :::"RealUnitarySpace":::); end; begin  
theorem :: RSSPACE2:3 (Bool  "for" (Set (Var "r")) "being"   ($#m1_subset_1 :::"Real_Sequence":::)  "st" (Bool (Bool  "("   "for" (Set (Var "n")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"  (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<="::: )  (Set (Set (Var "r"))  ($#k1_seq_1 :::"."::: )  (Set (Var "n"))))  ")" )) "holds"  (Bool  "("  (Bool  "("   "for" (Set (Var "n")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"  (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<="::: )  (Set (Set  "("  ($#k3_series_1 :::"Partial_Sums"::: )  (Set (Var "r")) ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "n"))))  ")" ) & (Bool  "("   "for" (Set (Var "n")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"  (Bool (Set (Set (Var "r"))  ($#k1_seq_1 :::"."::: )  (Set (Var "n")))  ($#r1_xxreal_0 :::"<="::: )  (Set (Set  "("  ($#k3_series_1 :::"Partial_Sums"::: )  (Set (Var "r")) ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "n"))))  ")" ) &  "("  (Bool (Bool (Set (Var "r")) "is"   ($#v1_series_1 :::"summable"::: )  )) "implies" (Bool  "("  (Bool  "("   "for" (Set (Var "n")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"  (Bool (Set (Set  "("  ($#k3_series_1 :::"Partial_Sums"::: )  (Set (Var "r")) ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "n")))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k4_series_1 :::"Sum"::: )  (Set (Var "r"))))  ")" ) & (Bool  "("   "for" (Set (Var "n")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"  (Bool (Set (Set (Var "r"))  ($#k1_seq_1 :::"."::: )  (Set (Var "n")))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k4_series_1 :::"Sum"::: )  (Set (Var "r"))))  ")" )  ")" )  ")"   ")" )) ; 
 
theorem :: RSSPACE2:4 (Bool  "("  (Bool  "("   "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#m1_subset_1 :::"Real":::) "holds"  (Bool (Set (Set  "(" (Set (Var "x"))  ($#k7_real_1 :::"+"::: )  (Set (Var "y")) ")" )  ($#k8_real_1 :::"*"::: )  (Set  "(" (Set (Var "x"))  ($#k7_real_1 :::"+"::: )  (Set (Var "y")) ")" ))  ($#r1_xxreal_0 :::"<="::: )  (Set (Set  "(" (Set  "(" (Num 2)  ($#k8_real_1 :::"*"::: )  (Set (Var "x")) ")" )  ($#k8_real_1 :::"*"::: )  (Set (Var "x")) ")" )  ($#k7_real_1 :::"+"::: )  (Set  "(" (Set  "(" (Num 2)  ($#k8_real_1 :::"*"::: )  (Set (Var "y")) ")" )  ($#k8_real_1 :::"*"::: )  (Set (Var "y")) ")" )))  ")" ) & (Bool  "("   "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#m1_subset_1 :::"Real":::) "holds"  (Bool (Set (Set (Var "x"))  ($#k8_real_1 :::"*"::: )  (Set (Var "x")))  ($#r1_xxreal_0 :::"<="::: )  (Set (Set  "(" (Set  "(" (Num 2)  ($#k8_real_1 :::"*"::: )  (Set  "(" (Set (Var "x"))  ($#k9_real_1 :::"-"::: )  (Set (Var "y")) ")" ) ")" )  ($#k8_real_1 :::"*"::: )  (Set  "(" (Set (Var "x"))  ($#k9_real_1 :::"-"::: )  (Set (Var "y")) ")" ) ")" )  ($#k7_real_1 :::"+"::: )  (Set  "(" (Set  "(" (Num 2)  ($#k8_real_1 :::"*"::: )  (Set (Var "y")) ")" )  ($#k8_real_1 :::"*"::: )  (Set (Var "y")) ")" )))  ")" )  ")" ) ; 
 
theorem :: RSSPACE2:5 (Bool  "for" (Set (Var "e")) "being"   ($#m1_subset_1 :::"Real":::)  (Bool  "for" (Set (Var "s")) "being"   ($#m1_subset_1 :::"Real_Sequence":::)  "st" (Bool (Bool (Set (Var "s")) "is"   ($#v2_comseq_2 :::"convergent"::: )  ) & (Bool  "ex" (Set (Var "k")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "st"  (Bool  "for" (Set (Var "i")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Var "k"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "i")))) "holds"  (Bool (Set (Set (Var "s"))  ($#k1_seq_1 :::"."::: )  (Set (Var "i")))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "e")))))) "holds"  (Bool (Set   ($#k2_seq_2 :::"lim"::: )  (Set (Var "s")))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "e"))))) ; 
 
theorem :: RSSPACE2:6 (Bool  "for" (Set (Var "c")) "being"   ($#m1_subset_1 :::"Real":::)  (Bool  "for" (Set (Var "s")) "being"   ($#m1_subset_1 :::"Real_Sequence":::)  "st" (Bool (Bool (Set (Var "s")) "is"   ($#v2_comseq_2 :::"convergent"::: )  )) "holds"  (Bool  "for" (Set (Var "r")) "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 "r"))  ($#k1_seq_1 :::"."::: )  (Set (Var "i")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set (Var "s"))  ($#k1_seq_1 :::"."::: )  (Set (Var "i")) ")" )  ($#k9_real_1 :::"-"::: )  (Set (Var "c")) ")" )  ($#k8_real_1 :::"*"::: )  (Set  "(" (Set  "(" (Set (Var "s"))  ($#k1_seq_1 :::"."::: )  (Set (Var "i")) ")" )  ($#k9_real_1 :::"-"::: )  (Set (Var "c")) ")" )))  ")" )) "holds"  (Bool  "("  (Bool (Set (Var "r")) "is"   ($#v2_comseq_2 :::"convergent"::: )  ) & (Bool (Set   ($#k2_seq_2 :::"lim"::: )  (Set (Var "r")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "("  ($#k2_seq_2 :::"lim"::: )  (Set (Var "s")) ")" )  ($#k9_real_1 :::"-"::: )  (Set (Var "c")) ")" )  ($#k8_real_1 :::"*"::: )  (Set  "(" (Set  "("  ($#k2_seq_2 :::"lim"::: )  (Set (Var "s")) ")" )  ($#k9_real_1 :::"-"::: )  (Set (Var "c")) ")" )))  ")" )))) ; 
 
theorem :: RSSPACE2:7 (Bool  "for" (Set (Var "c")) "being"   ($#m1_subset_1 :::"Real":::)  (Bool  "for" (Set (Var "s")) "," (Set (Var "s1")) "being"   ($#m1_subset_1 :::"Real_Sequence":::)  "st" (Bool (Bool (Set (Var "s")) "is"   ($#v2_comseq_2 :::"convergent"::: )  ) & (Bool (Set (Var "s1")) "is"   ($#v2_comseq_2 :::"convergent"::: )  )) "holds"  (Bool  "for" (Set (Var "r")) "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 "r"))  ($#k1_seq_1 :::"."::: )  (Set (Var "i")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set  "(" (Set (Var "s"))  ($#k1_seq_1 :::"."::: )  (Set (Var "i")) ")" )  ($#k9_real_1 :::"-"::: )  (Set (Var "c")) ")" )  ($#k8_real_1 :::"*"::: )  (Set  "(" (Set  "(" (Set (Var "s"))  ($#k1_seq_1 :::"."::: )  (Set (Var "i")) ")" )  ($#k9_real_1 :::"-"::: )  (Set (Var "c")) ")" ) ")" )  ($#k7_real_1 :::"+"::: )  (Set  "(" (Set (Var "s1"))  ($#k1_seq_1 :::"."::: )  (Set (Var "i")) ")" )))  ")" )) "holds"  (Bool  "("  (Bool (Set (Var "r")) "is"   ($#v2_comseq_2 :::"convergent"::: )  ) & (Bool (Set   ($#k2_seq_2 :::"lim"::: )  (Set (Var "r")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set  "("  ($#k2_seq_2 :::"lim"::: )  (Set (Var "s")) ")" )  ($#k9_real_1 :::"-"::: )  (Set (Var "c")) ")" )  ($#k8_real_1 :::"*"::: )  (Set  "(" (Set  "("  ($#k2_seq_2 :::"lim"::: )  (Set (Var "s")) ")" )  ($#k9_real_1 :::"-"::: )  (Set (Var "c")) ")" ) ")" )  ($#k7_real_1 :::"+"::: )  (Set  "("  ($#k2_seq_2 :::"lim"::: )  (Set (Var "s1")) ")" )))  ")" )))) ;