:: NORMSP_1  semantic presentation begin  definitionattr "c1" is  :::"strict"::: ; struct  :::"NORMSTR":::  ->    ($#l1_rlvect_1 :::"RLSStruct"::: )   ","    ($#l2_normsp_0 :::"N-ZeroStr"::: )  ; aggr :::"NORMSTR":::(# :::"carrier":::, :::"ZeroF":::, :::"addF":::, :::"Mult":::, :::"normF"::: #) ->    ($#l1_normsp_1 :::"NORMSTR"::: )  ; end; registration
cluster  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v1_normsp_1 :::"strict"::: )    for    ($#l1_normsp_1 :::"NORMSTR"::: )  ; 
end; 



definitionlet "IT" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_normsp_1 :::"NORMSTR"::: )  ; attr "IT" is  :::"RealNormSpace-like":::  means :: NORMSP_1:def 1 (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#m1_subset_1 :::"Point":::) "of" "IT"  (Bool  "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Real":::) "holds"   (Bool  "("  (Bool (Set  ($#k1_normsp_0 :::"||."::: ) (Set  "(" (Set (Var "a"))  ($#k1_rlvect_1 :::"*"::: )  (Set (Var "x")) ")" ) ($#k1_normsp_0 :::".||"::: ) )  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k18_complex1 :::"abs"::: )  (Set (Var "a")) ")" )  ($#k8_real_1 :::"*"::: )  (Set  ($#k1_normsp_0 :::"||."::: ) (Set (Var "x")) ($#k1_normsp_0 :::".||"::: ) ))) & (Bool (Set  ($#k1_normsp_0 :::"||."::: ) (Set  "(" (Set (Var "x"))  ($#k1_algstr_0 :::"+"::: )  (Set (Var "y")) ")" ) ($#k1_normsp_0 :::".||"::: ) )  ($#r1_xxreal_0 :::"<="::: )  (Set (Set  ($#k1_normsp_0 :::"||."::: ) (Set (Var "x")) ($#k1_normsp_0 :::".||"::: ) )  ($#k7_real_1 :::"+"::: )  (Set  ($#k1_normsp_0 :::"||."::: ) (Set (Var "y")) ($#k1_normsp_0 :::".||"::: ) )))  ")" ))); end; 




:: deftheorem    defines :::"RealNormSpace-like"::: NORMSP_1:def 1 :  (Bool  "for" (Set (Var "IT")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_normsp_1 :::"NORMSTR"::: )   "holds"   (Bool  "("  (Bool (Set (Var "IT")) "is"   ($#v2_normsp_1 :::"RealNormSpace-like"::: )  ) "iff" (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set (Var "IT"))  (Bool  "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Real":::) "holds"   (Bool  "("  (Bool (Set  ($#k1_normsp_0 :::"||."::: ) (Set  "(" (Set (Var "a"))  ($#k1_rlvect_1 :::"*"::: )  (Set (Var "x")) ")" ) ($#k1_normsp_0 :::".||"::: ) )  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k18_complex1 :::"abs"::: )  (Set (Var "a")) ")" )  ($#k8_real_1 :::"*"::: )  (Set  ($#k1_normsp_0 :::"||."::: ) (Set (Var "x")) ($#k1_normsp_0 :::".||"::: ) ))) & (Bool (Set  ($#k1_normsp_0 :::"||."::: ) (Set  "(" (Set (Var "x"))  ($#k1_algstr_0 :::"+"::: )  (Set (Var "y")) ")" ) ($#k1_normsp_0 :::".||"::: ) )  ($#r1_xxreal_0 :::"<="::: )  (Set (Set  ($#k1_normsp_0 :::"||."::: ) (Set (Var "x")) ($#k1_normsp_0 :::".||"::: ) )  ($#k7_real_1 :::"+"::: )  (Set  ($#k1_normsp_0 :::"||."::: ) (Set (Var "y")) ($#k1_normsp_0 :::".||"::: ) )))  ")" )))  ")" )); 
 registration
cluster  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#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"::: )     ($#v3_normsp_0 :::"discerning"::: )     ($#v4_normsp_0 :::"reflexive"::: )     ($#v1_normsp_1 :::"strict"::: )     ($#v2_normsp_1 :::"RealNormSpace-like"::: )    for    ($#l1_normsp_1 :::"NORMSTR"::: )  ; 
end; definitionmode RealNormSpace is  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#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"::: )     ($#v3_normsp_0 :::"discerning"::: )     ($#v4_normsp_0 :::"reflexive"::: )     ($#v2_normsp_1 :::"RealNormSpace-like"::: )     ($#l1_normsp_1 :::"NORMSTR"::: )  ; end; 











theorem :: NORMSP_1:1 (Bool  "for" (Set (Var "RNS")) "being"   ($#l1_normsp_1 :::"RealNormSpace":::) "holds"  (Bool (Set  ($#k1_normsp_0 :::"||."::: ) (Set  "("  ($#k4_struct_0 :::"0."::: )  (Set (Var "RNS")) ")" ) ($#k1_normsp_0 :::".||"::: ) )  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))) ; 
 
theorem :: NORMSP_1:2 (Bool  "for" (Set (Var "RNS")) "being"   ($#l1_normsp_1 :::"RealNormSpace":::)  (Bool  "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set (Var "RNS")) "holds"  (Bool (Set  ($#k1_normsp_0 :::"||."::: ) (Set  "("  ($#k4_algstr_0 :::"-"::: )  (Set (Var "x")) ")" ) ($#k1_normsp_0 :::".||"::: ) )  ($#r1_hidden :::"="::: )  (Set  ($#k1_normsp_0 :::"||."::: ) (Set (Var "x")) ($#k1_normsp_0 :::".||"::: ) )))) ; 
 
theorem :: NORMSP_1:3 (Bool  "for" (Set (Var "RNS")) "being"   ($#l1_normsp_1 :::"RealNormSpace":::)  (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set (Var "RNS")) "holds"  (Bool (Set  ($#k1_normsp_0 :::"||."::: ) (Set  "(" (Set (Var "x"))  ($#k5_algstr_0 :::"-"::: )  (Set (Var "y")) ")" ) ($#k1_normsp_0 :::".||"::: ) )  ($#r1_xxreal_0 :::"<="::: )  (Set (Set  ($#k1_normsp_0 :::"||."::: ) (Set (Var "x")) ($#k1_normsp_0 :::".||"::: ) )  ($#k7_real_1 :::"+"::: )  (Set  ($#k1_normsp_0 :::"||."::: ) (Set (Var "y")) ($#k1_normsp_0 :::".||"::: ) ))))) ; 
 
theorem :: NORMSP_1:4 (Bool  "for" (Set (Var "RNS")) "being"   ($#l1_normsp_1 :::"RealNormSpace":::)  (Bool  "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set (Var "RNS")) "holds"  (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<="::: )  (Set  ($#k1_normsp_0 :::"||."::: ) (Set (Var "x")) ($#k1_normsp_0 :::".||"::: ) )))) ; 
 registrationlet "RNS" be   ($#l1_normsp_1 :::"RealNormSpace":::); let "x" be   ($#m1_subset_1 :::"Point":::) "of" (Set (Const "RNS")); 
cluster (Set  ($#k1_normsp_0 :::"||."::: ) "x" ($#k1_normsp_0 :::".||"::: ) ) ->  ($#~v3_xxreal_0  "non"   ($#v3_xxreal_0 :::"negative"::: )   )  ; 
end; 
theorem :: NORMSP_1:5 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_subset_1 :::"Real":::)  (Bool  "for" (Set (Var "RNS")) "being"   ($#l1_normsp_1 :::"RealNormSpace":::)  (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set (Var "RNS")) "holds"  (Bool (Set  ($#k1_normsp_0 :::"||."::: ) (Set  "(" (Set  "(" (Set (Var "a"))  ($#k1_rlvect_1 :::"*"::: )  (Set (Var "x")) ")" )  ($#k3_rlvect_1 :::"+"::: )  (Set  "(" (Set (Var "b"))  ($#k1_rlvect_1 :::"*"::: )  (Set (Var "y")) ")" ) ")" ) ($#k1_normsp_0 :::".||"::: ) )  ($#r1_xxreal_0 :::"<="::: )  (Set (Set  "(" (Set  "("  ($#k18_complex1 :::"abs"::: )  (Set (Var "a")) ")" )  ($#k8_real_1 :::"*"::: )  (Set  ($#k1_normsp_0 :::"||."::: ) (Set (Var "x")) ($#k1_normsp_0 :::".||"::: ) ) ")" )  ($#k7_real_1 :::"+"::: )  (Set  "(" (Set  "("  ($#k18_complex1 :::"abs"::: )  (Set (Var "b")) ")" )  ($#k8_real_1 :::"*"::: )  (Set  ($#k1_normsp_0 :::"||."::: ) (Set (Var "y")) ($#k1_normsp_0 :::".||"::: ) ) ")" )))))) ; 
 
theorem :: NORMSP_1:6 (Bool  "for" (Set (Var "RNS")) "being"   ($#l1_normsp_1 :::"RealNormSpace":::)  (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set (Var "RNS")) "holds"   (Bool  "("  (Bool (Set  ($#k1_normsp_0 :::"||."::: ) (Set  "(" (Set (Var "x"))  ($#k5_algstr_0 :::"-"::: )  (Set (Var "y")) ")" ) ($#k1_normsp_0 :::".||"::: ) )  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  )) "iff" (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set (Var "y")))  ")" ))) ; 
 
theorem :: NORMSP_1:7 (Bool  "for" (Set (Var "RNS")) "being"   ($#l1_normsp_1 :::"RealNormSpace":::)  (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set (Var "RNS")) "holds"  (Bool (Set  ($#k1_normsp_0 :::"||."::: ) (Set  "(" (Set (Var "x"))  ($#k5_algstr_0 :::"-"::: )  (Set (Var "y")) ")" ) ($#k1_normsp_0 :::".||"::: ) )  ($#r1_hidden :::"="::: )  (Set  ($#k1_normsp_0 :::"||."::: ) (Set  "(" (Set (Var "y"))  ($#k5_algstr_0 :::"-"::: )  (Set (Var "x")) ")" ) ($#k1_normsp_0 :::".||"::: ) )))) ; 
 
theorem :: NORMSP_1:8 (Bool  "for" (Set (Var "RNS")) "being"   ($#l1_normsp_1 :::"RealNormSpace":::)  (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set (Var "RNS")) "holds"  (Bool (Set (Set  ($#k1_normsp_0 :::"||."::: ) (Set (Var "x")) ($#k1_normsp_0 :::".||"::: ) )  ($#k9_real_1 :::"-"::: )  (Set  ($#k1_normsp_0 :::"||."::: ) (Set (Var "y")) ($#k1_normsp_0 :::".||"::: ) ))  ($#r1_xxreal_0 :::"<="::: )  (Set  ($#k1_normsp_0 :::"||."::: ) (Set  "(" (Set (Var "x"))  ($#k5_algstr_0 :::"-"::: )  (Set (Var "y")) ")" ) ($#k1_normsp_0 :::".||"::: ) )))) ; 
 
theorem :: NORMSP_1:9 (Bool  "for" (Set (Var "RNS")) "being"   ($#l1_normsp_1 :::"RealNormSpace":::)  (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set (Var "RNS")) "holds"  (Bool (Set   ($#k18_complex1 :::"abs"::: )  (Set  "(" (Set  ($#k1_normsp_0 :::"||."::: ) (Set (Var "x")) ($#k1_normsp_0 :::".||"::: ) )  ($#k9_real_1 :::"-"::: )  (Set  ($#k1_normsp_0 :::"||."::: ) (Set (Var "y")) ($#k1_normsp_0 :::".||"::: ) ) ")" ))  ($#r1_xxreal_0 :::"<="::: )  (Set  ($#k1_normsp_0 :::"||."::: ) (Set  "(" (Set (Var "x"))  ($#k5_algstr_0 :::"-"::: )  (Set (Var "y")) ")" ) ($#k1_normsp_0 :::".||"::: ) )))) ; 
 
theorem :: NORMSP_1:10 (Bool  "for" (Set (Var "RNS")) "being"   ($#l1_normsp_1 :::"RealNormSpace":::)  (Bool  "for" (Set (Var "x")) "," (Set (Var "z")) "," (Set (Var "y")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set (Var "RNS")) "holds"  (Bool (Set  ($#k1_normsp_0 :::"||."::: ) (Set  "(" (Set (Var "x"))  ($#k5_algstr_0 :::"-"::: )  (Set (Var "z")) ")" ) ($#k1_normsp_0 :::".||"::: ) )  ($#r1_xxreal_0 :::"<="::: )  (Set (Set  ($#k1_normsp_0 :::"||."::: ) (Set  "(" (Set (Var "x"))  ($#k5_algstr_0 :::"-"::: )  (Set (Var "y")) ")" ) ($#k1_normsp_0 :::".||"::: ) )  ($#k7_real_1 :::"+"::: )  (Set  ($#k1_normsp_0 :::"||."::: ) (Set  "(" (Set (Var "y"))  ($#k5_algstr_0 :::"-"::: )  (Set (Var "z")) ")" ) ($#k1_normsp_0 :::".||"::: ) ))))) ; 
 
theorem :: NORMSP_1:11 (Bool  "for" (Set (Var "RNS")) "being"   ($#l1_normsp_1 :::"RealNormSpace":::)  (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set (Var "RNS"))  "st" (Bool (Bool (Set (Var "x"))  ($#r1_hidden :::"<>"::: )  (Set (Var "y")))) "holds"  (Bool (Set  ($#k1_normsp_0 :::"||."::: ) (Set  "(" (Set (Var "x"))  ($#k5_algstr_0 :::"-"::: )  (Set (Var "y")) ")" ) ($#k1_normsp_0 :::".||"::: ) )  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  )))) ; 
 























theorem :: NORMSP_1:12 (Bool  "for" (Set (Var "f")) "being"   ($#m1_hidden :::"Function":::)  (Bool  "for" (Set (Var "RNS")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_struct_0 :::"1-sorted"::: )    (Bool  "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "RNS")) "holds"   (Bool  "("  (Bool (Set (Var "f")) "is"   ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "RNS"))) "iff" (Bool  "("  (Bool (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "f")))  ($#r1_hidden :::"="::: )  (Set   ($#k5_numbers :::"NAT"::: )  )) & (Bool  "("   "for" (Set (Var "d")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "d"))  ($#r2_hidden :::"in"::: )  (Set   ($#k5_numbers :::"NAT"::: )  ))) "holds"  (Bool (Set (Set (Var "f"))  ($#k1_funct_1 :::"."::: )  (Set (Var "d"))) "is"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "RNS")))  ")" )  ")" )  ")" )))) ; 
 
theorem :: NORMSP_1:13 (Bool  "for" (Set (Var "RNS")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_struct_0 :::"1-sorted"::: )    (Bool  "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "RNS")) (Bool  "ex" (Set (Var "S")) "being"   ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "RNS")) "st" (Bool (Set   ($#k10_xtuple_0 :::"rng"::: )  (Set (Var "S")))  ($#r1_hidden :::"="::: )  (Set  ($#k6_domain_1 :::"{"::: ) (Set (Var "x")) ($#k6_domain_1 :::"}"::: ) ))))) ; 
 
theorem :: NORMSP_1:14 (Bool  "for" (Set (Var "RNS")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_struct_0 :::"1-sorted"::: )    (Bool  "for" (Set (Var "S")) "being"   ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "RNS"))  "st" (Bool (Bool  "ex" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "RNS")) "st"  (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::) "holds"  (Bool (Set (Set (Var "S"))  ($#k1_funct_1 :::"."::: )  (Set (Var "n")))  ($#r1_hidden :::"="::: )  (Set (Var "x")))))) "holds"  (Bool  "ex" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "RNS")) "st" (Bool (Set   ($#k10_xtuple_0 :::"rng"::: )  (Set (Var "S")))  ($#r1_hidden :::"="::: )  (Set  ($#k6_domain_1 :::"{"::: ) (Set (Var "x")) ($#k6_domain_1 :::"}"::: ) ))))) ; 
 
theorem :: NORMSP_1:15 (Bool  "for" (Set (Var "RNS")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_struct_0 :::"1-sorted"::: )    (Bool  "for" (Set (Var "S")) "being"   ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "RNS"))  "st" (Bool (Bool  "ex" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "RNS")) "st" (Bool (Set   ($#k10_xtuple_0 :::"rng"::: )  (Set (Var "S")))  ($#r1_hidden :::"="::: )  (Set  ($#k6_domain_1 :::"{"::: ) (Set (Var "x")) ($#k6_domain_1 :::"}"::: ) )))) "holds"  (Bool  "for" (Set (Var "n")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"  (Bool (Set (Set (Var "S"))  ($#k3_funct_2 :::"."::: )  (Set (Var "n")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "S"))  ($#k3_funct_2 :::"."::: )  (Set  "(" (Set (Var "n"))  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" )))))) ; 
 
theorem :: NORMSP_1:16 (Bool  "for" (Set (Var "RNS")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_struct_0 :::"1-sorted"::: )    (Bool  "for" (Set (Var "S")) "being"   ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "RNS"))  "st" (Bool (Bool  "("   "for" (Set (Var "n")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"  (Bool (Set (Set (Var "S"))  ($#k3_funct_2 :::"."::: )  (Set (Var "n")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "S"))  ($#k3_funct_2 :::"."::: )  (Set  "(" (Set (Var "n"))  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" )))  ")" )) "holds"  (Bool  "for" (Set (Var "n")) "," (Set (Var "k")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"  (Bool (Set (Set (Var "S"))  ($#k3_funct_2 :::"."::: )  (Set (Var "n")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "S"))  ($#k3_funct_2 :::"."::: )  (Set  "(" (Set (Var "n"))  ($#k2_nat_1 :::"+"::: )  (Set (Var "k")) ")" )))))) ; 
 
theorem :: NORMSP_1:17 (Bool  "for" (Set (Var "RNS")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_struct_0 :::"1-sorted"::: )    (Bool  "for" (Set (Var "S")) "being"   ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "RNS"))  "st" (Bool (Bool  "("   "for" (Set (Var "n")) "," (Set (Var "k")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"  (Bool (Set (Set (Var "S"))  ($#k3_funct_2 :::"."::: )  (Set (Var "n")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "S"))  ($#k3_funct_2 :::"."::: )  (Set  "(" (Set (Var "n"))  ($#k2_nat_1 :::"+"::: )  (Set (Var "k")) ")" )))  ")" )) "holds"  (Bool  "for" (Set (Var "n")) "," (Set (Var "m")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"  (Bool (Set (Set (Var "S"))  ($#k3_funct_2 :::"."::: )  (Set (Var "n")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "S"))  ($#k3_funct_2 :::"."::: )  (Set (Var "m"))))))) ; 
 
theorem :: NORMSP_1:18 (Bool  "for" (Set (Var "RNS")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_struct_0 :::"1-sorted"::: )    (Bool  "for" (Set (Var "S")) "being"   ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "RNS"))  "st" (Bool (Bool  "("   "for" (Set (Var "n")) "," (Set (Var "m")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"  (Bool (Set (Set (Var "S"))  ($#k3_funct_2 :::"."::: )  (Set (Var "n")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "S"))  ($#k3_funct_2 :::"."::: )  (Set (Var "m"))))  ")" )) "holds"  (Bool  "ex" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "RNS")) "st"  (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::) "holds"  (Bool (Set (Set (Var "S"))  ($#k1_funct_1 :::"."::: )  (Set (Var "n")))  ($#r1_hidden :::"="::: )  (Set (Var "x"))))))) ; 
 definitionlet "RNS" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_struct_0 :::"1-sorted"::: )  ; let "S" be   ($#m1_subset_1 :::"sequence":::) "of" (Set (Const "RNS")); let "n" be    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ); :: original: :::"."::: redefine func "S" :::"."::: "n" ->   ($#m1_subset_1 :::"Element":::) "of" "RNS"; end; definitionlet "RNS" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l2_algstr_0 :::"addLoopStr"::: )  ; let "S1", "S2" be   ($#m1_subset_1 :::"sequence":::) "of" (Set (Const "RNS")); func "S1" :::"+"::: "S2" ->   ($#m1_subset_1 :::"sequence":::) "of" "RNS" means :: NORMSP_1:def 2 (Bool  "for" (Set (Var "n")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"  (Bool (Set it  ($#k1_normsp_1 :::"."::: )  (Set (Var "n")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" "S1"  ($#k1_normsp_1 :::"."::: )  (Set (Var "n")) ")" )  ($#k1_algstr_0 :::"+"::: )  (Set  "(" "S2"  ($#k1_normsp_1 :::"."::: )  (Set (Var "n")) ")" )))); end; 







:: deftheorem    defines :::"+"::: NORMSP_1:def 2 :  (Bool  "for" (Set (Var "RNS")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l2_algstr_0 :::"addLoopStr"::: )    (Bool  "for" (Set (Var "S1")) "," (Set (Var "S2")) "," (Set (Var "b4")) "being"   ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "RNS")) "holds"   (Bool  "("  (Bool (Set (Var "b4"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "S1"))  ($#k2_normsp_1 :::"+"::: )  (Set (Var "S2")))) "iff" (Bool  "for" (Set (Var "n")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"  (Bool (Set (Set (Var "b4"))  ($#k1_normsp_1 :::"."::: )  (Set (Var "n")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "S1"))  ($#k1_normsp_1 :::"."::: )  (Set (Var "n")) ")" )  ($#k1_algstr_0 :::"+"::: )  (Set  "(" (Set (Var "S2"))  ($#k1_normsp_1 :::"."::: )  (Set (Var "n")) ")" ))))  ")" ))); 
 definitionlet "RNS" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l2_algstr_0 :::"addLoopStr"::: )  ; let "S1", "S2" be   ($#m1_subset_1 :::"sequence":::) "of" (Set (Const "RNS")); func "S1" :::"-"::: "S2" ->   ($#m1_subset_1 :::"sequence":::) "of" "RNS" means :: NORMSP_1:def 3 (Bool  "for" (Set (Var "n")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"  (Bool (Set it  ($#k1_normsp_1 :::"."::: )  (Set (Var "n")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" "S1"  ($#k1_normsp_1 :::"."::: )  (Set (Var "n")) ")" )  ($#k5_algstr_0 :::"-"::: )  (Set  "(" "S2"  ($#k1_normsp_1 :::"."::: )  (Set (Var "n")) ")" )))); end; 







:: deftheorem    defines :::"-"::: NORMSP_1:def 3 :  (Bool  "for" (Set (Var "RNS")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l2_algstr_0 :::"addLoopStr"::: )    (Bool  "for" (Set (Var "S1")) "," (Set (Var "S2")) "," (Set (Var "b4")) "being"   ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "RNS")) "holds"   (Bool  "("  (Bool (Set (Var "b4"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "S1"))  ($#k3_normsp_1 :::"-"::: )  (Set (Var "S2")))) "iff" (Bool  "for" (Set (Var "n")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"  (Bool (Set (Set (Var "b4"))  ($#k1_normsp_1 :::"."::: )  (Set (Var "n")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "S1"))  ($#k1_normsp_1 :::"."::: )  (Set (Var "n")) ")" )  ($#k5_algstr_0 :::"-"::: )  (Set  "(" (Set (Var "S2"))  ($#k1_normsp_1 :::"."::: )  (Set (Var "n")) ")" ))))  ")" ))); 
 definitionlet "RNS" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l2_algstr_0 :::"addLoopStr"::: )  ; let "S" be   ($#m1_subset_1 :::"sequence":::) "of" (Set (Const "RNS")); let "x" be   ($#m1_subset_1 :::"Element":::) "of" (Set (Const "RNS")); func "S" :::"-"::: "x" ->   ($#m1_subset_1 :::"sequence":::) "of" "RNS" means :: NORMSP_1:def 4 (Bool  "for" (Set (Var "n")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"  (Bool (Set it  ($#k1_normsp_1 :::"."::: )  (Set (Var "n")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" "S"  ($#k1_normsp_1 :::"."::: )  (Set (Var "n")) ")" )  ($#k5_algstr_0 :::"-"::: )  "x"))); end; 







:: deftheorem    defines :::"-"::: NORMSP_1:def 4 :  (Bool  "for" (Set (Var "RNS")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l2_algstr_0 :::"addLoopStr"::: )    (Bool  "for" (Set (Var "S")) "being"   ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "RNS"))  (Bool  "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "RNS"))  (Bool  "for" (Set (Var "b4")) "being"   ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "RNS")) "holds"   (Bool  "("  (Bool (Set (Var "b4"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "S"))  ($#k4_normsp_1 :::"-"::: )  (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_normsp_1 :::"."::: )  (Set (Var "n")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "S"))  ($#k1_normsp_1 :::"."::: )  (Set (Var "n")) ")" )  ($#k5_algstr_0 :::"-"::: )  (Set (Var "x")))))  ")" ))))); 
 definitionlet "RNS" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_rlvect_1 :::"RLSStruct"::: )  ; let "S" be   ($#m1_subset_1 :::"sequence":::) "of" (Set (Const "RNS")); let "a" be   ($#m1_subset_1 :::"Real":::); func "a" :::"*"::: "S" ->   ($#m1_subset_1 :::"sequence":::) "of" "RNS" means :: NORMSP_1:def 5 (Bool  "for" (Set (Var "n")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"  (Bool (Set it  ($#k1_normsp_1 :::"."::: )  (Set (Var "n")))  ($#r1_hidden :::"="::: )  (Set "a"  ($#k1_rlvect_1 :::"*"::: )  (Set  "(" "S"  ($#k1_normsp_1 :::"."::: )  (Set (Var "n")) ")" )))); end; 







:: deftheorem    defines :::"*"::: NORMSP_1:def 5 :  (Bool  "for" (Set (Var "RNS")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_rlvect_1 :::"RLSStruct"::: )    (Bool  "for" (Set (Var "S")) "being"   ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "RNS"))  (Bool  "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Real":::)  (Bool  "for" (Set (Var "b4")) "being"   ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "RNS")) "holds"   (Bool  "("  (Bool (Set (Var "b4"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "a"))  ($#k5_normsp_1 :::"*"::: )  (Set (Var "S")))) "iff" (Bool  "for" (Set (Var "n")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"  (Bool (Set (Set (Var "b4"))  ($#k1_normsp_1 :::"."::: )  (Set (Var "n")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "a"))  ($#k1_rlvect_1 :::"*"::: )  (Set  "(" (Set (Var "S"))  ($#k1_normsp_1 :::"."::: )  (Set (Var "n")) ")" ))))  ")" ))))); 
 definitionlet "RNS" be   ($#l1_normsp_1 :::"RealNormSpace":::); let "S" be   ($#m1_subset_1 :::"sequence":::) "of" (Set (Const "RNS")); attr "S" is  :::"convergent":::  means :: NORMSP_1:def 6 (Bool  "ex" (Set (Var "g")) "being"   ($#m1_subset_1 :::"Point":::) "of" "RNS" "st"  (Bool  "for" (Set (Var "r")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "r")))) "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 "m"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "n")))) "holds"  (Bool (Set  ($#k1_normsp_0 :::"||."::: ) (Set  "(" (Set  "(" "S"  ($#k1_normsp_1 :::"."::: )  (Set (Var "n")) ")" )  ($#k5_algstr_0 :::"-"::: )  (Set (Var "g")) ")" ) ($#k1_normsp_0 :::".||"::: ) )  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "r"))))))); end; 





:: deftheorem    defines :::"convergent"::: NORMSP_1:def 6 :  (Bool  "for" (Set (Var "RNS")) "being"   ($#l1_normsp_1 :::"RealNormSpace":::)  (Bool  "for" (Set (Var "S")) "being"   ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "RNS")) "holds"   (Bool  "("  (Bool (Set (Var "S")) "is"   ($#v3_normsp_1 :::"convergent"::: )  ) "iff" (Bool  "ex" (Set (Var "g")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set (Var "RNS")) "st"  (Bool  "for" (Set (Var "r")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "r")))) "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 "m"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "n")))) "holds"  (Bool (Set  ($#k1_normsp_0 :::"||."::: ) (Set  "(" (Set  "(" (Set (Var "S"))  ($#k1_normsp_1 :::"."::: )  (Set (Var "n")) ")" )  ($#k5_algstr_0 :::"-"::: )  (Set (Var "g")) ")" ) ($#k1_normsp_0 :::".||"::: ) )  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "r")))))))  ")" ))); 
 
theorem :: NORMSP_1:19 (Bool  "for" (Set (Var "RNS")) "being"   ($#l1_normsp_1 :::"RealNormSpace":::)  (Bool  "for" (Set (Var "S1")) "," (Set (Var "S2")) "being"   ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "RNS"))  "st" (Bool (Bool (Set (Var "S1")) "is"   ($#v3_normsp_1 :::"convergent"::: )  ) & (Bool (Set (Var "S2")) "is"   ($#v3_normsp_1 :::"convergent"::: )  )) "holds"  (Bool (Set (Set (Var "S1"))  ($#k2_normsp_1 :::"+"::: )  (Set (Var "S2"))) "is"   ($#v3_normsp_1 :::"convergent"::: )  ))) ; 
 
theorem :: NORMSP_1:20 (Bool  "for" (Set (Var "RNS")) "being"   ($#l1_normsp_1 :::"RealNormSpace":::)  (Bool  "for" (Set (Var "S1")) "," (Set (Var "S2")) "being"   ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "RNS"))  "st" (Bool (Bool (Set (Var "S1")) "is"   ($#v3_normsp_1 :::"convergent"::: )  ) & (Bool (Set (Var "S2")) "is"   ($#v3_normsp_1 :::"convergent"::: )  )) "holds"  (Bool (Set (Set (Var "S1"))  ($#k3_normsp_1 :::"-"::: )  (Set (Var "S2"))) "is"   ($#v3_normsp_1 :::"convergent"::: )  ))) ; 
 
theorem :: NORMSP_1:21 (Bool  "for" (Set (Var "RNS")) "being"   ($#l1_normsp_1 :::"RealNormSpace":::)  (Bool  "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set (Var "RNS"))  (Bool  "for" (Set (Var "S")) "being"   ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "RNS"))  "st" (Bool (Bool (Set (Var "S")) "is"   ($#v3_normsp_1 :::"convergent"::: )  )) "holds"  (Bool (Set (Set (Var "S"))  ($#k4_normsp_1 :::"-"::: )  (Set (Var "x"))) "is"   ($#v3_normsp_1 :::"convergent"::: )  )))) ; 
 
theorem :: NORMSP_1:22 (Bool  "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Real":::)  (Bool  "for" (Set (Var "RNS")) "being"   ($#l1_normsp_1 :::"RealNormSpace":::)  (Bool  "for" (Set (Var "S")) "being"   ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "RNS"))  "st" (Bool (Bool (Set (Var "S")) "is"   ($#v3_normsp_1 :::"convergent"::: )  )) "holds"  (Bool (Set (Set (Var "a"))  ($#k5_normsp_1 :::"*"::: )  (Set (Var "S"))) "is"   ($#v3_normsp_1 :::"convergent"::: )  )))) ; 
 
theorem :: NORMSP_1:23 (Bool  "for" (Set (Var "RNS")) "being"   ($#l1_normsp_1 :::"RealNormSpace":::)  (Bool  "for" (Set (Var "S")) "being"   ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "RNS"))  "st" (Bool (Bool (Set (Var "S")) "is"   ($#v3_normsp_1 :::"convergent"::: )  )) "holds"  (Bool (Set  ($#k4_normsp_0 :::"||."::: ) (Set (Var "S")) ($#k4_normsp_0 :::".||"::: ) ) "is"   ($#v2_comseq_2 :::"convergent"::: )  ))) ; 
 definitionlet "RNS" be   ($#l1_normsp_1 :::"RealNormSpace":::); let "S" be   ($#m1_subset_1 :::"sequence":::) "of" (Set (Const "RNS")); assume 
(Bool (Set (Const "S")) "is"   ($#v3_normsp_1 :::"convergent"::: )  )
 ; func  :::"lim"::: "S" ->   ($#m1_subset_1 :::"Point":::) "of" "RNS" means :: NORMSP_1:def 7 (Bool  "for" (Set (Var "r")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "r")))) "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 "m"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "n")))) "holds"  (Bool (Set  ($#k1_normsp_0 :::"||."::: ) (Set  "(" (Set  "(" "S"  ($#k1_normsp_1 :::"."::: )  (Set (Var "n")) ")" )  ($#k5_algstr_0 :::"-"::: )  it ")" ) ($#k1_normsp_0 :::".||"::: ) )  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "r")))))); end; 







:: deftheorem    defines :::"lim"::: NORMSP_1:def 7 :  (Bool  "for" (Set (Var "RNS")) "being"   ($#l1_normsp_1 :::"RealNormSpace":::)  (Bool  "for" (Set (Var "S")) "being"   ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "RNS"))  "st" (Bool (Bool (Set (Var "S")) "is"   ($#v3_normsp_1 :::"convergent"::: )  )) "holds"  (Bool  "for" (Set (Var "b3")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set (Var "RNS")) "holds"   (Bool  "("  (Bool (Set (Var "b3"))  ($#r1_hidden :::"="::: )  (Set   ($#k6_normsp_1 :::"lim"::: )  (Set (Var "S")))) "iff" (Bool  "for" (Set (Var "r")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "r")))) "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 "m"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "n")))) "holds"  (Bool (Set  ($#k1_normsp_0 :::"||."::: ) (Set  "(" (Set  "(" (Set (Var "S"))  ($#k1_normsp_1 :::"."::: )  (Set (Var "n")) ")" )  ($#k5_algstr_0 :::"-"::: )  (Set (Var "b3")) ")" ) ($#k1_normsp_0 :::".||"::: ) )  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "r"))))))  ")" )))); 
 
theorem :: NORMSP_1:24 (Bool  "for" (Set (Var "RNS")) "being"   ($#l1_normsp_1 :::"RealNormSpace":::)  (Bool  "for" (Set (Var "g")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set (Var "RNS"))  (Bool  "for" (Set (Var "S")) "being"   ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "RNS"))  "st" (Bool (Bool (Set (Var "S")) "is"   ($#v3_normsp_1 :::"convergent"::: )  ) & (Bool (Set   ($#k6_normsp_1 :::"lim"::: )  (Set (Var "S")))  ($#r1_hidden :::"="::: )  (Set (Var "g")))) "holds"  (Bool  "("  (Bool (Set  ($#k4_normsp_0 :::"||."::: ) (Set  "(" (Set (Var "S"))  ($#k4_normsp_1 :::"-"::: )  (Set (Var "g")) ")" ) ($#k4_normsp_0 :::".||"::: ) ) "is"   ($#v2_comseq_2 :::"convergent"::: )  ) & (Bool (Set   ($#k2_seq_2 :::"lim"::: )  (Set  ($#k4_normsp_0 :::"||."::: ) (Set  "(" (Set (Var "S"))  ($#k4_normsp_1 :::"-"::: )  (Set (Var "g")) ")" ) ($#k4_normsp_0 :::".||"::: ) ))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")" )))) ; 
 
theorem :: NORMSP_1:25 (Bool  "for" (Set (Var "RNS")) "being"   ($#l1_normsp_1 :::"RealNormSpace":::)  (Bool  "for" (Set (Var "S1")) "," (Set (Var "S2")) "being"   ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "RNS"))  "st" (Bool (Bool (Set (Var "S1")) "is"   ($#v3_normsp_1 :::"convergent"::: )  ) & (Bool (Set (Var "S2")) "is"   ($#v3_normsp_1 :::"convergent"::: )  )) "holds"  (Bool (Set   ($#k6_normsp_1 :::"lim"::: )  (Set  "(" (Set (Var "S1"))  ($#k2_normsp_1 :::"+"::: )  (Set (Var "S2")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k6_normsp_1 :::"lim"::: )  (Set (Var "S1")) ")" )  ($#k3_rlvect_1 :::"+"::: )  (Set  "("  ($#k6_normsp_1 :::"lim"::: )  (Set (Var "S2")) ")" ))))) ; 
 
theorem :: NORMSP_1:26 (Bool  "for" (Set (Var "RNS")) "being"   ($#l1_normsp_1 :::"RealNormSpace":::)  (Bool  "for" (Set (Var "S1")) "," (Set (Var "S2")) "being"   ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "RNS"))  "st" (Bool (Bool (Set (Var "S1")) "is"   ($#v3_normsp_1 :::"convergent"::: )  ) & (Bool (Set (Var "S2")) "is"   ($#v3_normsp_1 :::"convergent"::: )  )) "holds"  (Bool (Set   ($#k6_normsp_1 :::"lim"::: )  (Set  "(" (Set (Var "S1"))  ($#k3_normsp_1 :::"-"::: )  (Set (Var "S2")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k6_normsp_1 :::"lim"::: )  (Set (Var "S1")) ")" )  ($#k5_algstr_0 :::"-"::: )  (Set  "("  ($#k6_normsp_1 :::"lim"::: )  (Set (Var "S2")) ")" ))))) ; 
 
theorem :: NORMSP_1:27 (Bool  "for" (Set (Var "RNS")) "being"   ($#l1_normsp_1 :::"RealNormSpace":::)  (Bool  "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set (Var "RNS"))  (Bool  "for" (Set (Var "S")) "being"   ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "RNS"))  "st" (Bool (Bool (Set (Var "S")) "is"   ($#v3_normsp_1 :::"convergent"::: )  )) "holds"  (Bool (Set   ($#k6_normsp_1 :::"lim"::: )  (Set  "(" (Set (Var "S"))  ($#k4_normsp_1 :::"-"::: )  (Set (Var "x")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k6_normsp_1 :::"lim"::: )  (Set (Var "S")) ")" )  ($#k5_algstr_0 :::"-"::: )  (Set (Var "x"))))))) ; 
 
theorem :: NORMSP_1:28 (Bool  "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Real":::)  (Bool  "for" (Set (Var "RNS")) "being"   ($#l1_normsp_1 :::"RealNormSpace":::)  (Bool  "for" (Set (Var "S")) "being"   ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "RNS"))  "st" (Bool (Bool (Set (Var "S")) "is"   ($#v3_normsp_1 :::"convergent"::: )  )) "holds"  (Bool (Set   ($#k6_normsp_1 :::"lim"::: )  (Set  "(" (Set (Var "a"))  ($#k5_normsp_1 :::"*"::: )  (Set (Var "S")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "a"))  ($#k1_rlvect_1 :::"*"::: )  (Set  "("  ($#k6_normsp_1 :::"lim"::: )  (Set (Var "S")) ")" )))))) ;