:: C0SP1  semantic presentation begin  definitionlet "V" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l2_algstr_0 :::"addLoopStr"::: )  ; let "V1" be   ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "V")); attr "V1" is  :::"having-inverse":::  means :: C0SP1:def 1 (Bool  "for" (Set (Var "v")) "being"   ($#m1_subset_1 :::"Element":::) "of" "V"  "st" (Bool (Bool (Set (Var "v"))  ($#r2_hidden :::"in"::: )  "V1")) "holds"  (Bool (Set   ($#k4_algstr_0 :::"-"::: )  (Set (Var "v")))  ($#r2_hidden :::"in"::: )  "V1")); end; 





:: deftheorem    defines :::"having-inverse"::: C0SP1:def 1 :  (Bool  "for" (Set (Var "V")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l2_algstr_0 :::"addLoopStr"::: )    (Bool  "for" (Set (Var "V1")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V")) "holds"   (Bool  "("  (Bool (Set (Var "V1")) "is"   ($#v1_c0sp1 :::"having-inverse"::: )  ) "iff" (Bool  "for" (Set (Var "v")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "V"))  "st" (Bool (Bool (Set (Var "v"))  ($#r2_hidden :::"in"::: )  (Set (Var "V1")))) "holds"  (Bool (Set   ($#k4_algstr_0 :::"-"::: )  (Set (Var "v")))  ($#r2_hidden :::"in"::: )  (Set (Var "V1"))))  ")" ))); 
 definitionlet "V" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l2_algstr_0 :::"addLoopStr"::: )  ; let "V1" be   ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "V")); attr "V1" is  :::"additively-closed":::  means :: C0SP1:def 2 (Bool  "("  (Bool "V1" "is"   ($#v1_ideal_1 :::"add-closed"::: )  ) & (Bool "V1" "is"   ($#v1_c0sp1 :::"having-inverse"::: )  )  ")" ); end; 





:: deftheorem    defines :::"additively-closed"::: C0SP1:def 2 :  (Bool  "for" (Set (Var "V")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l2_algstr_0 :::"addLoopStr"::: )    (Bool  "for" (Set (Var "V1")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V")) "holds"   (Bool  "("  (Bool (Set (Var "V1")) "is"   ($#v2_c0sp1 :::"additively-closed"::: )  ) "iff" (Bool  "("  (Bool (Set (Var "V1")) "is"   ($#v1_ideal_1 :::"add-closed"::: )  ) & (Bool (Set (Var "V1")) "is"   ($#v1_c0sp1 :::"having-inverse"::: )  )  ")" )  ")" ))); 
 registrationlet "V" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l2_algstr_0 :::"addLoopStr"::: )  ; 
cluster (Set   ($#k2_struct_0 :::"[#]"::: )  "V") ->   ($#v1_ideal_1 :::"add-closed"::: )     ($#v1_c0sp1 :::"having-inverse"::: )   ; 
end; registrationlet "V" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l6_algstr_0 :::"doubleLoopStr"::: )  ; 
cluster   ($#v2_c0sp1 :::"additively-closed"::: )    ->   ($#v1_ideal_1 :::"add-closed"::: )     ($#v1_c0sp1 :::"having-inverse"::: )    for    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k1_zfmisc_1 :::"bool"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "V")); 

cluster   ($#v1_ideal_1 :::"add-closed"::: )     ($#v1_c0sp1 :::"having-inverse"::: )    ->   ($#v2_c0sp1 :::"additively-closed"::: )    for    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k1_zfmisc_1 :::"bool"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "V")); 
end; registrationlet "V" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l2_algstr_0 :::"addLoopStr"::: )  ; 
cluster  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v1_ideal_1 :::"add-closed"::: )     ($#v1_c0sp1 :::"having-inverse"::: )    for    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k1_zfmisc_1 :::"bool"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "V")); 
end; definitionlet "V" be   ($#l6_algstr_0 :::"Ring":::); mode  :::"Subring":::  "of" "V" ->   ($#l6_algstr_0 :::"Ring":::) means :: C0SP1:def 3 (Bool  "("  (Bool (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" it)  ($#r1_tarski :::"c="::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "V")) & (Bool (Set  "the"  ($#u1_algstr_0 :::"addF"::: )  "of" it)  ($#r1_hidden :::"="::: )  (Set (Set  "the"  ($#u1_algstr_0 :::"addF"::: )  "of" "V")  ($#k1_realset1 :::"||"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" it))) & (Bool (Set  "the"  ($#u2_algstr_0 :::"multF"::: )  "of" it)  ($#r1_hidden :::"="::: )  (Set (Set  "the"  ($#u2_algstr_0 :::"multF"::: )  "of" "V")  ($#k1_realset1 :::"||"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" it))) & (Bool (Set   ($#k5_struct_0 :::"1."::: )  it)  ($#r1_hidden :::"="::: )  (Set   ($#k5_struct_0 :::"1."::: )  "V")) & (Bool (Set   ($#k4_struct_0 :::"0."::: )  it)  ($#r1_hidden :::"="::: )  (Set   ($#k4_struct_0 :::"0."::: )  "V"))  ")" ); end; 





:: deftheorem    defines :::"Subring"::: C0SP1:def 3 :  (Bool  "for" (Set (Var "V")) "," (Set (Var "b2")) "being"   ($#l6_algstr_0 :::"Ring":::) "holds"   (Bool  "("  (Bool (Set (Var "b2")) "is"    ($#m1_c0sp1 :::"Subring"::: )   "of" (Set (Var "V"))) "iff" (Bool  "("  (Bool (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "b2")))  ($#r1_tarski :::"c="::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "V")))) & (Bool (Set  "the"  ($#u1_algstr_0 :::"addF"::: )  "of" (Set (Var "b2")))  ($#r1_hidden :::"="::: )  (Set (Set  "the"  ($#u1_algstr_0 :::"addF"::: )  "of" (Set (Var "V")))  ($#k1_realset1 :::"||"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "b2"))))) & (Bool (Set  "the"  ($#u2_algstr_0 :::"multF"::: )  "of" (Set (Var "b2")))  ($#r1_hidden :::"="::: )  (Set (Set  "the"  ($#u2_algstr_0 :::"multF"::: )  "of" (Set (Var "V")))  ($#k1_realset1 :::"||"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "b2"))))) & (Bool (Set   ($#k5_struct_0 :::"1."::: )  (Set (Var "b2")))  ($#r1_hidden :::"="::: )  (Set   ($#k5_struct_0 :::"1."::: )  (Set (Var "V")))) & (Bool (Set   ($#k4_struct_0 :::"0."::: )  (Set (Var "b2")))  ($#r1_hidden :::"="::: )  (Set   ($#k4_struct_0 :::"0."::: )  (Set (Var "V"))))  ")" )  ")" )); 
 






















theorem :: C0SP1:1 (Bool  "for" (Set (Var "X")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "d1")) "," (Set (Var "d2")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Var "X"))  (Bool  "for" (Set (Var "A")) "being"   ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "X"))  (Bool  "for" (Set (Var "M")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "X")) "," (Set (Var "X")) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set (Var "X"))  (Bool  "for" (Set (Var "V")) "being"   ($#l6_algstr_0 :::"Ring":::)  (Bool  "for" (Set (Var "V1")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V"))  "st" (Bool (Bool (Set (Var "V1"))  ($#r1_hidden :::"="::: )  (Set (Var "X"))) & (Bool (Set (Var "A"))  ($#r1_hidden :::"="::: )  (Set (Set  "the"  ($#u1_algstr_0 :::"addF"::: )  "of" (Set (Var "V")))  ($#k1_realset1 :::"||"::: )  (Set (Var "V1")))) & (Bool (Set (Var "M"))  ($#r1_hidden :::"="::: )  (Set (Set  "the"  ($#u2_algstr_0 :::"multF"::: )  "of" (Set (Var "V")))  ($#k1_realset1 :::"||"::: )  (Set (Var "V1")))) & (Bool (Set (Var "d1"))  ($#r1_hidden :::"="::: )  (Set   ($#k5_struct_0 :::"1."::: )  (Set (Var "V")))) & (Bool (Set (Var "d2"))  ($#r1_hidden :::"="::: )  (Set   ($#k4_struct_0 :::"0."::: )  (Set (Var "V")))) & (Bool (Set (Var "V1")) "is"   ($#v1_c0sp1 :::"having-inverse"::: )  )) "holds"  (Bool (Set   ($#g6_algstr_0 :::"doubleLoopStr"::: )  "(#"  (Set (Var "X")) "," (Set (Var "A")) "," (Set (Var "M")) "," (Set (Var "d1")) "," (Set (Var "d2")) "#)" ) "is"    ($#m1_c0sp1 :::"Subring"::: )   "of" (Set (Var "V"))))))))) ; 
 registrationlet "V" be   ($#l6_algstr_0 :::"Ring":::); 
cluster  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v12_algstr_0 :::"left_complementable"::: )     ($#v13_algstr_0 :::"right_complementable"::: )     ($#v14_algstr_0 :::"complementable"::: )     ($#v36_algstr_0 :::"strict"::: )     ($#v2_rlvect_1 :::"Abelian"::: )     ($#v3_rlvect_1 :::"add-associative"::: )     ($#v4_rlvect_1 :::"right_zeroed"::: )   bbbadV9_RLVECT_1()   ($#v1_group_1 :::"unital"::: )     ($#v3_group_1 :::"associative"::: )     ($#v1_vectsp_1 :::"right-distributive"::: )     ($#v2_vectsp_1 :::"left-distributive"::: )     ($#v3_vectsp_1 :::"right_unital"::: )     ($#v4_vectsp_1 :::"well-unital"::: )     ($#v5_vectsp_1 :::"distributive"::: )     ($#v6_vectsp_1 :::"left_unital"::: )    for    ($#m1_c0sp1 :::"Subring"::: )   "of" "V"; 
end; definitionlet "V" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l5_algstr_0 :::"multLoopStr_0"::: )  ; let "V1" be   ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "V")); attr "V1" is  :::"multiplicatively-closed":::  means :: C0SP1:def 4 (Bool  "("  (Bool (Set   ($#k5_struct_0 :::"1."::: )  "V")  ($#r2_hidden :::"in"::: )  "V1") & (Bool  "("   "for" (Set (Var "v")) "," (Set (Var "u")) "being"   ($#m1_subset_1 :::"Element":::) "of" "V"  "st" (Bool (Bool (Set (Var "v"))  ($#r2_hidden :::"in"::: )  "V1") & (Bool (Set (Var "u"))  ($#r2_hidden :::"in"::: )  "V1")) "holds"  (Bool (Set (Set (Var "v"))  ($#k6_algstr_0 :::"*"::: )  (Set (Var "u")))  ($#r2_hidden :::"in"::: )  "V1")  ")" )  ")" ); end; 





:: deftheorem    defines :::"multiplicatively-closed"::: C0SP1:def 4 :  (Bool  "for" (Set (Var "V")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l5_algstr_0 :::"multLoopStr_0"::: )    (Bool  "for" (Set (Var "V1")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V")) "holds"   (Bool  "("  (Bool (Set (Var "V1")) "is"   ($#v3_c0sp1 :::"multiplicatively-closed"::: )  ) "iff" (Bool  "("  (Bool (Set   ($#k5_struct_0 :::"1."::: )  (Set (Var "V")))  ($#r2_hidden :::"in"::: )  (Set (Var "V1"))) & (Bool  "("   "for" (Set (Var "v")) "," (Set (Var "u")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "V"))  "st" (Bool (Bool (Set (Var "v"))  ($#r2_hidden :::"in"::: )  (Set (Var "V1"))) & (Bool (Set (Var "u"))  ($#r2_hidden :::"in"::: )  (Set (Var "V1")))) "holds"  (Bool (Set (Set (Var "v"))  ($#k6_algstr_0 :::"*"::: )  (Set (Var "u")))  ($#r2_hidden :::"in"::: )  (Set (Var "V1")))  ")" )  ")" )  ")" ))); 
 definitionlet "V" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l2_algstr_0 :::"addLoopStr"::: )  ; let "V1" be   ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "V")); assume 
(Bool  "("  (Bool (Set (Const "V1")) "is"   ($#v1_ideal_1 :::"add-closed"::: )  ) & (Bool (Bool  "not" (Set (Const "V1")) "is"   ($#v1_xboole_0 :::"empty"::: )  ))  ")" )
 ; func  :::"Add_":::  "(" "V1" "," "V" ")"  ->   ($#m1_subset_1 :::"BinOp":::) "of" "V1" equals :: C0SP1:def 5 (Set (Set  "the"  ($#u1_algstr_0 :::"addF"::: )  "of" "V")  ($#k1_realset1 :::"||"::: )  "V1"); end; 







:: deftheorem    defines :::"Add_"::: C0SP1:def 5 :  (Bool  "for" (Set (Var "V")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l2_algstr_0 :::"addLoopStr"::: )    (Bool  "for" (Set (Var "V1")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V"))  "st" (Bool (Bool (Set (Var "V1")) "is"   ($#v1_ideal_1 :::"add-closed"::: )  ) & (Bool (Bool  "not" (Set (Var "V1")) "is"   ($#v1_xboole_0 :::"empty"::: )  ))) "holds"  (Bool (Set   ($#k1_c0sp1 :::"Add_"::: )   "(" (Set (Var "V1")) "," (Set (Var "V")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set  "the"  ($#u1_algstr_0 :::"addF"::: )  "of" (Set (Var "V")))  ($#k1_realset1 :::"||"::: )  (Set (Var "V1")))))); 
 definitionlet "V" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l5_algstr_0 :::"multLoopStr_0"::: )  ; let "V1" be   ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "V")); assume 
(Bool  "("  (Bool (Set (Const "V1")) "is"   ($#v3_c0sp1 :::"multiplicatively-closed"::: )  ) & (Bool (Bool  "not" (Set (Const "V1")) "is"   ($#v1_xboole_0 :::"empty"::: )  ))  ")" )
 ; func  :::"mult_":::  "(" "V1" "," "V" ")"  ->   ($#m1_subset_1 :::"BinOp":::) "of" "V1" equals :: C0SP1:def 6 (Set (Set  "the"  ($#u2_algstr_0 :::"multF"::: )  "of" "V")  ($#k1_realset1 :::"||"::: )  "V1"); end; 







:: deftheorem    defines :::"mult_"::: C0SP1:def 6 :  (Bool  "for" (Set (Var "V")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l5_algstr_0 :::"multLoopStr_0"::: )    (Bool  "for" (Set (Var "V1")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V"))  "st" (Bool (Bool (Set (Var "V1")) "is"   ($#v3_c0sp1 :::"multiplicatively-closed"::: )  ) & (Bool (Bool  "not" (Set (Var "V1")) "is"   ($#v1_xboole_0 :::"empty"::: )  ))) "holds"  (Bool (Set   ($#k2_c0sp1 :::"mult_"::: )   "(" (Set (Var "V1")) "," (Set (Var "V")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set  "the"  ($#u2_algstr_0 :::"multF"::: )  "of" (Set (Var "V")))  ($#k1_realset1 :::"||"::: )  (Set (Var "V1")))))); 
 definitionlet "V" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v13_algstr_0 :::"right_complementable"::: )     ($#v3_rlvect_1 :::"add-associative"::: )     ($#v4_rlvect_1 :::"right_zeroed"::: )     ($#l6_algstr_0 :::"doubleLoopStr"::: )  ; let "V1" be   ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "V")); assume 
(Bool  "("  (Bool (Set (Const "V1")) "is"   ($#v1_ideal_1 :::"add-closed"::: )  ) & (Bool (Set (Const "V1")) "is"   ($#v1_c0sp1 :::"having-inverse"::: )  ) & (Bool (Bool  "not" (Set (Const "V1")) "is"   ($#v1_xboole_0 :::"empty"::: )  ))  ")" )
 ; func  :::"Zero_":::  "(" "V1" "," "V" ")"  ->    ($#m1_subset_1 :::"Element"::: )   "of" "V1" equals :: C0SP1:def 7 (Set   ($#k4_struct_0 :::"0."::: )  "V"); end; 







:: deftheorem    defines :::"Zero_"::: C0SP1:def 7 :  (Bool  "for" (Set (Var "V")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v13_algstr_0 :::"right_complementable"::: )     ($#v3_rlvect_1 :::"add-associative"::: )     ($#v4_rlvect_1 :::"right_zeroed"::: )     ($#l6_algstr_0 :::"doubleLoopStr"::: )    (Bool  "for" (Set (Var "V1")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V"))  "st" (Bool (Bool (Set (Var "V1")) "is"   ($#v1_ideal_1 :::"add-closed"::: )  ) & (Bool (Set (Var "V1")) "is"   ($#v1_c0sp1 :::"having-inverse"::: )  ) & (Bool (Bool  "not" (Set (Var "V1")) "is"   ($#v1_xboole_0 :::"empty"::: )  ))) "holds"  (Bool (Set   ($#k3_c0sp1 :::"Zero_"::: )   "(" (Set (Var "V1")) "," (Set (Var "V")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k4_struct_0 :::"0."::: )  (Set (Var "V")))))); 
 definitionlet "V" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l5_algstr_0 :::"multLoopStr_0"::: )  ; let "V1" be   ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "V")); assume 
(Bool  "("  (Bool (Set (Const "V1")) "is"   ($#v3_c0sp1 :::"multiplicatively-closed"::: )  ) & (Bool (Bool  "not" (Set (Const "V1")) "is"   ($#v1_xboole_0 :::"empty"::: )  ))  ")" )
 ; func  :::"One_":::  "(" "V1" "," "V" ")"  ->    ($#m1_subset_1 :::"Element"::: )   "of" "V1" equals :: C0SP1:def 8 (Set   ($#k5_struct_0 :::"1."::: )  "V"); end; 







:: deftheorem    defines :::"One_"::: C0SP1:def 8 :  (Bool  "for" (Set (Var "V")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l5_algstr_0 :::"multLoopStr_0"::: )    (Bool  "for" (Set (Var "V1")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V"))  "st" (Bool (Bool (Set (Var "V1")) "is"   ($#v3_c0sp1 :::"multiplicatively-closed"::: )  ) & (Bool (Bool  "not" (Set (Var "V1")) "is"   ($#v1_xboole_0 :::"empty"::: )  ))) "holds"  (Bool (Set   ($#k4_c0sp1 :::"One_"::: )   "(" (Set (Var "V1")) "," (Set (Var "V")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k5_struct_0 :::"1."::: )  (Set (Var "V")))))); 
 
theorem :: C0SP1:2 (Bool  "for" (Set (Var "V")) "being"   ($#l6_algstr_0 :::"Ring":::)  (Bool  "for" (Set (Var "V1")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V"))  "st" (Bool (Bool (Set (Var "V1")) "is"   ($#v2_c0sp1 :::"additively-closed"::: )  ) & (Bool (Set (Var "V1")) "is"   ($#v3_c0sp1 :::"multiplicatively-closed"::: )  ) & (Bool (Bool  "not" (Set (Var "V1")) "is"   ($#v1_xboole_0 :::"empty"::: )  ))) "holds"  (Bool (Set   ($#g6_algstr_0 :::"doubleLoopStr"::: )  "(#"  (Set (Var "V1")) "," (Set  "("  ($#k1_c0sp1 :::"Add_"::: )   "(" (Set (Var "V1")) "," (Set (Var "V")) ")"  ")" ) "," (Set  "("  ($#k2_c0sp1 :::"mult_"::: )   "(" (Set (Var "V1")) "," (Set (Var "V")) ")"  ")" ) "," (Set  "("  ($#k4_c0sp1 :::"One_"::: )   "(" (Set (Var "V1")) "," (Set (Var "V")) ")"  ")" ) "," (Set  "("  ($#k3_c0sp1 :::"Zero_"::: )   "(" (Set (Var "V1")) "," (Set (Var "V")) ")"  ")" ) "#)" ) "is"   ($#l6_algstr_0 :::"Ring":::)))) ; 
 begin  











definitionlet "V" be   ($#l1_funcsdom :::"Algebra":::); mode  :::"Subalgebra":::  "of" "V" ->   ($#l1_funcsdom :::"Algebra":::) means :: C0SP1:def 9 (Bool  "("  (Bool (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" it)  ($#r1_tarski :::"c="::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "V")) & (Bool (Set  "the"  ($#u1_algstr_0 :::"addF"::: )  "of" it)  ($#r1_hidden :::"="::: )  (Set (Set  "the"  ($#u1_algstr_0 :::"addF"::: )  "of" "V")  ($#k1_realset1 :::"||"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" it))) & (Bool (Set  "the"  ($#u2_algstr_0 :::"multF"::: )  "of" it)  ($#r1_hidden :::"="::: )  (Set (Set  "the"  ($#u2_algstr_0 :::"multF"::: )  "of" "V")  ($#k1_realset1 :::"||"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" it))) & (Bool (Set  "the"  ($#u1_rlvect_1 :::"Mult"::: )  "of" it)  ($#r1_hidden :::"="::: )  (Set (Set  "the"  ($#u1_rlvect_1 :::"Mult"::: )  "of" "V")  ($#k2_partfun1 :::"|"::: )  (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set  ($#k1_numbers :::"REAL"::: ) ) "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" it) ($#k2_zfmisc_1 :::":]"::: ) ))) & (Bool (Set   ($#k5_struct_0 :::"1."::: )  it)  ($#r1_hidden :::"="::: )  (Set   ($#k5_struct_0 :::"1."::: )  "V")) & (Bool (Set   ($#k4_struct_0 :::"0."::: )  it)  ($#r1_hidden :::"="::: )  (Set   ($#k4_struct_0 :::"0."::: )  "V"))  ")" ); end; 





:: deftheorem    defines :::"Subalgebra"::: C0SP1:def 9 :  (Bool  "for" (Set (Var "V")) "," (Set (Var "b2")) "being"   ($#l1_funcsdom :::"Algebra":::) "holds"   (Bool  "("  (Bool (Set (Var "b2")) "is"    ($#m2_c0sp1 :::"Subalgebra"::: )   "of" (Set (Var "V"))) "iff" (Bool  "("  (Bool (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "b2")))  ($#r1_tarski :::"c="::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "V")))) & (Bool (Set  "the"  ($#u1_algstr_0 :::"addF"::: )  "of" (Set (Var "b2")))  ($#r1_hidden :::"="::: )  (Set (Set  "the"  ($#u1_algstr_0 :::"addF"::: )  "of" (Set (Var "V")))  ($#k1_realset1 :::"||"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "b2"))))) & (Bool (Set  "the"  ($#u2_algstr_0 :::"multF"::: )  "of" (Set (Var "b2")))  ($#r1_hidden :::"="::: )  (Set (Set  "the"  ($#u2_algstr_0 :::"multF"::: )  "of" (Set (Var "V")))  ($#k1_realset1 :::"||"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "b2"))))) & (Bool (Set  "the"  ($#u1_rlvect_1 :::"Mult"::: )  "of" (Set (Var "b2")))  ($#r1_hidden :::"="::: )  (Set (Set  "the"  ($#u1_rlvect_1 :::"Mult"::: )  "of" (Set (Var "V")))  ($#k2_partfun1 :::"|"::: )  (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set  ($#k1_numbers :::"REAL"::: ) ) "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "b2"))) ($#k2_zfmisc_1 :::":]"::: ) ))) & (Bool (Set   ($#k5_struct_0 :::"1."::: )  (Set (Var "b2")))  ($#r1_hidden :::"="::: )  (Set   ($#k5_struct_0 :::"1."::: )  (Set (Var "V")))) & (Bool (Set   ($#k4_struct_0 :::"0."::: )  (Set (Var "b2")))  ($#r1_hidden :::"="::: )  (Set   ($#k4_struct_0 :::"0."::: )  (Set (Var "V"))))  ")" )  ")" )); 
 
theorem :: C0SP1:3 (Bool  "for" (Set (Var "X")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "d1")) "," (Set (Var "d2")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Var "X"))  (Bool  "for" (Set (Var "A")) "being"   ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "X"))  (Bool  "for" (Set (Var "M")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "X")) "," (Set (Var "X")) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set (Var "X"))  (Bool  "for" (Set (Var "V")) "being"   ($#l1_funcsdom :::"Algebra":::)  (Bool  "for" (Set (Var "V1")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V"))  (Bool  "for" (Set (Var "MR")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set  ($#k1_numbers :::"REAL"::: ) ) "," (Set (Var "X")) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set (Var "X"))  "st" (Bool (Bool (Set (Var "V1"))  ($#r1_hidden :::"="::: )  (Set (Var "X"))) & (Bool (Set (Var "d1"))  ($#r1_hidden :::"="::: )  (Set   ($#k4_struct_0 :::"0."::: )  (Set (Var "V")))) & (Bool (Set (Var "d2"))  ($#r1_hidden :::"="::: )  (Set   ($#k5_struct_0 :::"1."::: )  (Set (Var "V")))) & (Bool (Set (Var "A"))  ($#r1_hidden :::"="::: )  (Set (Set  "the"  ($#u1_algstr_0 :::"addF"::: )  "of" (Set (Var "V")))  ($#k1_realset1 :::"||"::: )  (Set (Var "V1")))) & (Bool (Set (Var "M"))  ($#r1_hidden :::"="::: )  (Set (Set  "the"  ($#u2_algstr_0 :::"multF"::: )  "of" (Set (Var "V")))  ($#k1_realset1 :::"||"::: )  (Set (Var "V1")))) & (Bool (Set (Var "MR"))  ($#r1_hidden :::"="::: )  (Set (Set  "the"  ($#u1_rlvect_1 :::"Mult"::: )  "of" (Set (Var "V")))  ($#k2_partfun1 :::"|"::: )  (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set  ($#k1_numbers :::"REAL"::: ) ) "," (Set (Var "V1")) ($#k2_zfmisc_1 :::":]"::: ) ))) & (Bool (Set (Var "V1")) "is"   ($#v1_c0sp1 :::"having-inverse"::: )  )) "holds"  (Bool (Set   ($#g1_funcsdom :::"AlgebraStr"::: )  "(#"  (Set (Var "X")) "," (Set (Var "M")) "," (Set (Var "A")) "," (Set (Var "MR")) "," (Set (Var "d2")) "," (Set (Var "d1")) "#)" ) "is"    ($#m2_c0sp1 :::"Subalgebra"::: )   "of" (Set (Var "V")))))))))) ; 
 registrationlet "V" be   ($#l1_funcsdom :::"Algebra":::); 
cluster  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v12_algstr_0 :::"left_complementable"::: )     ($#v13_algstr_0 :::"right_complementable"::: )     ($#v14_algstr_0 :::"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"::: )   bbbadV9_RLVECT_1()   ($#v1_funcsdom :::"strict"::: )     ($#v2_funcsdom :::"vector-associative"::: )     ($#v1_group_1 :::"unital"::: )     ($#v3_group_1 :::"associative"::: )     ($#v5_group_1 :::"commutative"::: )     ($#v1_vectsp_1 :::"right-distributive"::: )     ($#v3_vectsp_1 :::"right_unital"::: )     ($#v4_vectsp_1 :::"well-unital"::: )     ($#v6_vectsp_1 :::"left_unital"::: )    for    ($#m2_c0sp1 :::"Subalgebra"::: )   "of" "V"; 
end; definitionlet "V" be   ($#l1_funcsdom :::"Algebra":::); let "V1" be   ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "V")); attr "V1" is  :::"additively-linearly-closed":::  means :: C0SP1:def 10 (Bool  "("  (Bool "V1" "is"   ($#v1_ideal_1 :::"add-closed"::: )  ) & (Bool "V1" "is"   ($#v1_c0sp1 :::"having-inverse"::: )  ) & (Bool  "("   "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Real":::)  (Bool  "for" (Set (Var "v")) "being"   ($#m1_subset_1 :::"Element":::) "of" "V"  "st" (Bool (Bool (Set (Var "v"))  ($#r2_hidden :::"in"::: )  "V1")) "holds"  (Bool (Set (Set (Var "a"))  ($#k1_rlvect_1 :::"*"::: )  (Set (Var "v")))  ($#r2_hidden :::"in"::: )  "V1"))  ")" )  ")" ); end; 





:: deftheorem    defines :::"additively-linearly-closed"::: C0SP1:def 10 :  (Bool  "for" (Set (Var "V")) "being"   ($#l1_funcsdom :::"Algebra":::)  (Bool  "for" (Set (Var "V1")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V")) "holds"   (Bool  "("  (Bool (Set (Var "V1")) "is"   ($#v4_c0sp1 :::"additively-linearly-closed"::: )  ) "iff" (Bool  "("  (Bool (Set (Var "V1")) "is"   ($#v1_ideal_1 :::"add-closed"::: )  ) & (Bool (Set (Var "V1")) "is"   ($#v1_c0sp1 :::"having-inverse"::: )  ) & (Bool  "("   "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Real":::)  (Bool  "for" (Set (Var "v")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "V"))  "st" (Bool (Bool (Set (Var "v"))  ($#r2_hidden :::"in"::: )  (Set (Var "V1")))) "holds"  (Bool (Set (Set (Var "a"))  ($#k1_rlvect_1 :::"*"::: )  (Set (Var "v")))  ($#r2_hidden :::"in"::: )  (Set (Var "V1"))))  ")" )  ")" )  ")" ))); 
 registrationlet "V" be   ($#l1_funcsdom :::"Algebra":::); 
cluster   ($#v4_c0sp1 :::"additively-linearly-closed"::: )    ->   ($#v2_c0sp1 :::"additively-closed"::: )    for    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k1_zfmisc_1 :::"bool"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "V")); 
end; definitionlet "V" be   ($#l1_funcsdom :::"Algebra":::); let "V1" be   ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "V")); assume 
(Bool  "("  (Bool (Set (Const "V1")) "is"   ($#v4_c0sp1 :::"additively-linearly-closed"::: )  ) & (Bool (Bool  "not" (Set (Const "V1")) "is"   ($#v1_xboole_0 :::"empty"::: )  ))  ")" )
 ; func  :::"Mult_":::  "(" "V1" "," "V" ")"  ->   ($#m1_subset_1 :::"Function":::) "of" (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set  ($#k1_numbers :::"REAL"::: ) ) "," "V1" ($#k2_zfmisc_1 :::":]"::: ) ) "," "V1" equals :: C0SP1:def 11 (Set (Set  "the"  ($#u1_rlvect_1 :::"Mult"::: )  "of" "V")  ($#k2_partfun1 :::"|"::: )  (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set  ($#k1_numbers :::"REAL"::: ) ) "," "V1" ($#k2_zfmisc_1 :::":]"::: ) )); end; 







:: deftheorem    defines :::"Mult_"::: C0SP1:def 11 :  (Bool  "for" (Set (Var "V")) "being"   ($#l1_funcsdom :::"Algebra":::)  (Bool  "for" (Set (Var "V1")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V"))  "st" (Bool (Bool (Set (Var "V1")) "is"   ($#v4_c0sp1 :::"additively-linearly-closed"::: )  ) & (Bool (Bool  "not" (Set (Var "V1")) "is"   ($#v1_xboole_0 :::"empty"::: )  ))) "holds"  (Bool (Set   ($#k5_c0sp1 :::"Mult_"::: )   "(" (Set (Var "V1")) "," (Set (Var "V")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set  "the"  ($#u1_rlvect_1 :::"Mult"::: )  "of" (Set (Var "V")))  ($#k2_partfun1 :::"|"::: )  (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set  ($#k1_numbers :::"REAL"::: ) ) "," (Set (Var "V1")) ($#k2_zfmisc_1 :::":]"::: ) ))))); 
 definitionlet "V" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_rlvect_1 :::"RLSStruct"::: )  ; attr "V" is  :::"scalar-mult-cancelable":::  means :: C0SP1:def 12 (Bool  "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Real":::)  (Bool  "for" (Set (Var "v")) "being"   ($#m1_subset_1 :::"Element":::) "of" "V"  "holds"  (Bool  "("   "not" (Bool (Set (Set (Var "a"))  ($#k1_rlvect_1 :::"*"::: )  (Set (Var "v")))  ($#r1_hidden :::"="::: )  (Set   ($#k4_struct_0 :::"0."::: )  "V")) "or" (Bool (Set (Var "a"))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  )) "or" (Bool (Set (Var "v"))  ($#r1_hidden :::"="::: )  (Set   ($#k4_struct_0 :::"0."::: )  "V"))  ")" ))); end; 




:: deftheorem    defines :::"scalar-mult-cancelable"::: C0SP1:def 12 :  (Bool  "for" (Set (Var "V")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_rlvect_1 :::"RLSStruct"::: )   "holds"   (Bool  "("  (Bool (Set (Var "V")) "is"   ($#v5_c0sp1 :::"scalar-mult-cancelable"::: )  ) "iff" (Bool  "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Real":::)  (Bool  "for" (Set (Var "v")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "V"))  "holds"  (Bool  "("   "not" (Bool (Set (Set (Var "a"))  ($#k1_rlvect_1 :::"*"::: )  (Set (Var "v")))  ($#r1_hidden :::"="::: )  (Set   ($#k4_struct_0 :::"0."::: )  (Set (Var "V")))) "or" (Bool (Set (Var "a"))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  )) "or" (Bool (Set (Var "v"))  ($#r1_hidden :::"="::: )  (Set   ($#k4_struct_0 :::"0."::: )  (Set (Var "V"))))  ")" )))  ")" )); 
 
theorem :: C0SP1:4 (Bool  "for" (Set (Var "V")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v13_algstr_0 :::"right_complementable"::: )     ($#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"::: )     ($#v2_funcsdom :::"vector-associative"::: )     ($#l1_funcsdom :::"AlgebraStr"::: )    (Bool  "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Real":::) "holds"  (Bool (Set (Set (Var "a"))  ($#k1_rlvect_1 :::"*"::: )  (Set  "("  ($#k4_struct_0 :::"0."::: )  (Set (Var "V")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k4_struct_0 :::"0."::: )  (Set (Var "V")))))) ; 
 
theorem :: C0SP1:5 (Bool  "for" (Set (Var "V")) "being"  ($#~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"::: )     ($#v2_funcsdom :::"vector-associative"::: )     ($#l1_funcsdom :::"AlgebraStr"::: )    "st" (Bool (Bool (Set (Var "V")) "is"   ($#v5_c0sp1 :::"scalar-mult-cancelable"::: )  )) "holds"  (Bool (Set (Var "V")) "is"   ($#l1_rlvect_1 :::"RealLinearSpace":::))) ; 
 
theorem :: C0SP1:6 (Bool  "for" (Set (Var "V")) "being"   ($#l1_funcsdom :::"Algebra":::)  (Bool  "for" (Set (Var "V1")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V"))  "st" (Bool (Bool (Set (Var "V1")) "is"   ($#v4_c0sp1 :::"additively-linearly-closed"::: )  ) & (Bool (Set (Var "V1")) "is"   ($#v3_c0sp1 :::"multiplicatively-closed"::: )  ) & (Bool (Bool  "not" (Set (Var "V1")) "is"   ($#v1_xboole_0 :::"empty"::: )  ))) "holds"  (Bool (Set   ($#g1_funcsdom :::"AlgebraStr"::: )  "(#"  (Set (Var "V1")) "," (Set  "("  ($#k2_c0sp1 :::"mult_"::: )   "(" (Set (Var "V1")) "," (Set (Var "V")) ")"  ")" ) "," (Set  "("  ($#k1_c0sp1 :::"Add_"::: )   "(" (Set (Var "V1")) "," (Set (Var "V")) ")"  ")" ) "," (Set  "("  ($#k5_c0sp1 :::"Mult_"::: )   "(" (Set (Var "V1")) "," (Set (Var "V")) ")"  ")" ) "," (Set  "("  ($#k4_c0sp1 :::"One_"::: )   "(" (Set (Var "V1")) "," (Set (Var "V")) ")"  ")" ) "," (Set  "("  ($#k3_c0sp1 :::"Zero_"::: )   "(" (Set (Var "V1")) "," (Set (Var "V")) ")"  ")" ) "#)" ) "is"    ($#m2_c0sp1 :::"Subalgebra"::: )   "of" (Set (Var "V"))))) ; 
 registrationlet "X" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )  ; 
cluster (Set   ($#k12_funcsdom :::"RAlgebra"::: )  "X") ->   ($#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"::: )     ($#v2_funcsdom :::"vector-associative"::: )     ($#v3_group_1 :::"associative"::: )     ($#v5_group_1 :::"commutative"::: )     ($#v1_vectsp_1 :::"right-distributive"::: )     ($#v3_vectsp_1 :::"right_unital"::: )   ; 
end; 
theorem :: C0SP1:7 (Bool  "for" (Set (Var "X")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )   "holds"  (Bool (Set   ($#k12_funcsdom :::"RAlgebra"::: )  (Set (Var "X"))) "is"   ($#l1_rlvect_1 :::"RealLinearSpace":::))) ; 
 
theorem :: C0SP1:8 (Bool  "for" (Set (Var "V")) "being"   ($#l1_funcsdom :::"Algebra":::)  (Bool  "for" (Set (Var "V1")) "being"    ($#m2_c0sp1 :::"Subalgebra"::: )   "of" (Set (Var "V")) "holds"   (Bool  "("  (Bool  "("   "for" (Set (Var "v1")) "," (Set (Var "w1")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "V1"))  (Bool  "for" (Set (Var "v")) "," (Set (Var "w")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "V"))  "st" (Bool (Bool (Set (Var "v1"))  ($#r1_hidden :::"="::: )  (Set (Var "v"))) & (Bool (Set (Var "w1"))  ($#r1_hidden :::"="::: )  (Set (Var "w")))) "holds"  (Bool (Set (Set (Var "v1"))  ($#k3_rlvect_1 :::"+"::: )  (Set (Var "w1")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "v"))  ($#k3_rlvect_1 :::"+"::: )  (Set (Var "w")))))  ")" ) & (Bool  "("   "for" (Set (Var "v1")) "," (Set (Var "w1")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "V1"))  (Bool  "for" (Set (Var "v")) "," (Set (Var "w")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "V"))  "st" (Bool (Bool (Set (Var "v1"))  ($#r1_hidden :::"="::: )  (Set (Var "v"))) & (Bool (Set (Var "w1"))  ($#r1_hidden :::"="::: )  (Set (Var "w")))) "holds"  (Bool (Set (Set (Var "v1"))  ($#k8_group_1 :::"*"::: )  (Set (Var "w1")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "v"))  ($#k8_group_1 :::"*"::: )  (Set (Var "w")))))  ")" ) & (Bool  "("   "for" (Set (Var "v1")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "V1"))  (Bool  "for" (Set (Var "v")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "V"))  (Bool  "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Set (Var "v1"))  ($#r1_hidden :::"="::: )  (Set (Var "v")))) "holds"  (Bool (Set (Set (Var "a"))  ($#k1_rlvect_1 :::"*"::: )  (Set (Var "v1")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "a"))  ($#k1_rlvect_1 :::"*"::: )  (Set (Var "v"))))))  ")" ) & (Bool (Set   ($#k1_group_1 :::"1_"::: )  (Set (Var "V1")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_group_1 :::"1_"::: )  (Set (Var "V")))) & (Bool (Set   ($#k4_struct_0 :::"0."::: )  (Set (Var "V1")))  ($#r1_hidden :::"="::: )  (Set   ($#k4_struct_0 :::"0."::: )  (Set (Var "V"))))  ")" ))) ; 
 begin  definitionlet "X" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )  ; func  :::"BoundedFunctions"::: "X" ->  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k12_funcsdom :::"RAlgebra"::: )  "X" ")" ) equals :: C0SP1:def 13  "{"  (Set (Var "f")) where f "is"   ($#m1_subset_1 :::"Function":::) "of" "X" "," (Set  ($#k1_numbers :::"REAL"::: ) ) : (Bool (Set (Set (Var "f"))  ($#k2_partfun1 :::"|"::: )  "X") "is"   ($#v1_comseq_2 :::"bounded"::: )  )  "}"  ; end; 





:: deftheorem    defines :::"BoundedFunctions"::: C0SP1:def 13 :  (Bool  "for" (Set (Var "X")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )   "holds"  (Bool (Set   ($#k6_c0sp1 :::"BoundedFunctions"::: )  (Set (Var "X")))  ($#r1_hidden :::"="::: )   "{"  (Set (Var "f")) where f "is"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set  ($#k1_numbers :::"REAL"::: ) ) : (Bool (Set (Set (Var "f"))  ($#k2_partfun1 :::"|"::: )  (Set (Var "X"))) "is"   ($#v1_comseq_2 :::"bounded"::: )  )  "}"  )); 
 
theorem :: C0SP1:9 (Bool  "for" (Set (Var "X")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set   ($#k6_c0sp1 :::"BoundedFunctions"::: )  (Set (Var "X"))) "is"   ($#v4_c0sp1 :::"additively-linearly-closed"::: )  ) & (Bool (Set   ($#k6_c0sp1 :::"BoundedFunctions"::: )  (Set (Var "X"))) "is"   ($#v3_c0sp1 :::"multiplicatively-closed"::: )  )  ")" )) ; 
 registrationlet "X" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )  ; 
cluster (Set   ($#k6_c0sp1 :::"BoundedFunctions"::: )  "X") ->  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v3_c0sp1 :::"multiplicatively-closed"::: )     ($#v4_c0sp1 :::"additively-linearly-closed"::: )   ; 
end; definitionlet "X" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )  ; func  :::"R_Algebra_of_BoundedFunctions"::: "X" ->   ($#l1_funcsdom :::"Algebra":::) equals :: C0SP1:def 14 (Set   ($#g1_funcsdom :::"AlgebraStr"::: )  "(#"  (Set  "("  ($#k6_c0sp1 :::"BoundedFunctions"::: )  "X" ")" ) "," (Set  "("  ($#k2_c0sp1 :::"mult_"::: )   "(" (Set  "("  ($#k6_c0sp1 :::"BoundedFunctions"::: )  "X" ")" ) "," (Set  "("  ($#k12_funcsdom :::"RAlgebra"::: )  "X" ")" ) ")"  ")" ) "," (Set  "("  ($#k1_c0sp1 :::"Add_"::: )   "(" (Set  "("  ($#k6_c0sp1 :::"BoundedFunctions"::: )  "X" ")" ) "," (Set  "("  ($#k12_funcsdom :::"RAlgebra"::: )  "X" ")" ) ")"  ")" ) "," (Set  "("  ($#k5_c0sp1 :::"Mult_"::: )   "(" (Set  "("  ($#k6_c0sp1 :::"BoundedFunctions"::: )  "X" ")" ) "," (Set  "("  ($#k12_funcsdom :::"RAlgebra"::: )  "X" ")" ) ")"  ")" ) "," (Set  "("  ($#k4_c0sp1 :::"One_"::: )   "(" (Set  "("  ($#k6_c0sp1 :::"BoundedFunctions"::: )  "X" ")" ) "," (Set  "("  ($#k12_funcsdom :::"RAlgebra"::: )  "X" ")" ) ")"  ")" ) "," (Set  "("  ($#k3_c0sp1 :::"Zero_"::: )   "(" (Set  "("  ($#k6_c0sp1 :::"BoundedFunctions"::: )  "X" ")" ) "," (Set  "("  ($#k12_funcsdom :::"RAlgebra"::: )  "X" ")" ) ")"  ")" ) "#)" ); end; 





:: deftheorem    defines :::"R_Algebra_of_BoundedFunctions"::: C0SP1:def 14 :  (Bool  "for" (Set (Var "X")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )   "holds"  (Bool (Set   ($#k7_c0sp1 :::"R_Algebra_of_BoundedFunctions"::: )  (Set (Var "X")))  ($#r1_hidden :::"="::: )  (Set   ($#g1_funcsdom :::"AlgebraStr"::: )  "(#"  (Set  "("  ($#k6_c0sp1 :::"BoundedFunctions"::: )  (Set (Var "X")) ")" ) "," (Set  "("  ($#k2_c0sp1 :::"mult_"::: )   "(" (Set  "("  ($#k6_c0sp1 :::"BoundedFunctions"::: )  (Set (Var "X")) ")" ) "," (Set  "("  ($#k12_funcsdom :::"RAlgebra"::: )  (Set (Var "X")) ")" ) ")"  ")" ) "," (Set  "("  ($#k1_c0sp1 :::"Add_"::: )   "(" (Set  "("  ($#k6_c0sp1 :::"BoundedFunctions"::: )  (Set (Var "X")) ")" ) "," (Set  "("  ($#k12_funcsdom :::"RAlgebra"::: )  (Set (Var "X")) ")" ) ")"  ")" ) "," (Set  "("  ($#k5_c0sp1 :::"Mult_"::: )   "(" (Set  "("  ($#k6_c0sp1 :::"BoundedFunctions"::: )  (Set (Var "X")) ")" ) "," (Set  "("  ($#k12_funcsdom :::"RAlgebra"::: )  (Set (Var "X")) ")" ) ")"  ")" ) "," (Set  "("  ($#k4_c0sp1 :::"One_"::: )   "(" (Set  "("  ($#k6_c0sp1 :::"BoundedFunctions"::: )  (Set (Var "X")) ")" ) "," (Set  "("  ($#k12_funcsdom :::"RAlgebra"::: )  (Set (Var "X")) ")" ) ")"  ")" ) "," (Set  "("  ($#k3_c0sp1 :::"Zero_"::: )   "(" (Set  "("  ($#k6_c0sp1 :::"BoundedFunctions"::: )  (Set (Var "X")) ")" ) "," (Set  "("  ($#k12_funcsdom :::"RAlgebra"::: )  (Set (Var "X")) ")" ) ")"  ")" ) "#)" ))); 
 
theorem :: C0SP1:10 (Bool  "for" (Set (Var "X")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )   "holds"  (Bool (Set   ($#k7_c0sp1 :::"R_Algebra_of_BoundedFunctions"::: )  (Set (Var "X"))) "is"    ($#m2_c0sp1 :::"Subalgebra"::: )   "of" (Set   ($#k12_funcsdom :::"RAlgebra"::: )  (Set (Var "X"))))) ; 
 
theorem :: C0SP1:11 (Bool  "for" (Set (Var "X")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )   "holds"  (Bool (Set   ($#k7_c0sp1 :::"R_Algebra_of_BoundedFunctions"::: )  (Set (Var "X"))) "is"   ($#l1_rlvect_1 :::"RealLinearSpace":::))) ; 
 










theorem :: C0SP1:12 (Bool  "for" (Set (Var "X")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "F")) "," (Set (Var "G")) "," (Set (Var "H")) "being"   ($#m1_subset_1 :::"VECTOR":::) "of" (Set  "("  ($#k7_c0sp1 :::"R_Algebra_of_BoundedFunctions"::: )  (Set (Var "X")) ")" )  (Bool  "for" (Set (Var "f")) "," (Set (Var "g")) "," (Set (Var "h")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set  ($#k1_numbers :::"REAL"::: ) )  "st" (Bool (Bool (Set (Var "f"))  ($#r1_hidden :::"="::: )  (Set (Var "F"))) & (Bool (Set (Var "g"))  ($#r1_hidden :::"="::: )  (Set (Var "G"))) & (Bool (Set (Var "h"))  ($#r1_hidden :::"="::: )  (Set (Var "H")))) "holds"  (Bool  "("  (Bool (Set (Var "H"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "F"))  ($#k3_rlvect_1 :::"+"::: )  (Set (Var "G")))) "iff" (Bool  "for" (Set (Var "x")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Var "X")) "holds"  (Bool (Set (Set (Var "h"))  ($#k1_seq_1 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "f"))  ($#k1_seq_1 :::"."::: )  (Set (Var "x")) ")" )  ($#k7_real_1 :::"+"::: )  (Set  "(" (Set (Var "g"))  ($#k1_seq_1 :::"."::: )  (Set (Var "x")) ")" ))))  ")" )))) ; 
 
theorem :: C0SP1:13 (Bool  "for" (Set (Var "X")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Real":::)  (Bool  "for" (Set (Var "F")) "," (Set (Var "G")) "being"   ($#m1_subset_1 :::"VECTOR":::) "of" (Set  "("  ($#k7_c0sp1 :::"R_Algebra_of_BoundedFunctions"::: )  (Set (Var "X")) ")" )  (Bool  "for" (Set (Var "f")) "," (Set (Var "g")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set  ($#k1_numbers :::"REAL"::: ) )  "st" (Bool (Bool (Set (Var "f"))  ($#r1_hidden :::"="::: )  (Set (Var "F"))) & (Bool (Set (Var "g"))  ($#r1_hidden :::"="::: )  (Set (Var "G")))) "holds"  (Bool  "("  (Bool (Set (Var "G"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "a"))  ($#k1_rlvect_1 :::"*"::: )  (Set (Var "F")))) "iff" (Bool  "for" (Set (Var "x")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Var "X")) "holds"  (Bool (Set (Set (Var "g"))  ($#k1_seq_1 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "a"))  ($#k8_real_1 :::"*"::: )  (Set  "(" (Set (Var "f"))  ($#k1_seq_1 :::"."::: )  (Set (Var "x")) ")" ))))  ")" ))))) ; 
 
theorem :: C0SP1:14 (Bool  "for" (Set (Var "X")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "F")) "," (Set (Var "G")) "," (Set (Var "H")) "being"   ($#m1_subset_1 :::"VECTOR":::) "of" (Set  "("  ($#k7_c0sp1 :::"R_Algebra_of_BoundedFunctions"::: )  (Set (Var "X")) ")" )  (Bool  "for" (Set (Var "f")) "," (Set (Var "g")) "," (Set (Var "h")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set  ($#k1_numbers :::"REAL"::: ) )  "st" (Bool (Bool (Set (Var "f"))  ($#r1_hidden :::"="::: )  (Set (Var "F"))) & (Bool (Set (Var "g"))  ($#r1_hidden :::"="::: )  (Set (Var "G"))) & (Bool (Set (Var "h"))  ($#r1_hidden :::"="::: )  (Set (Var "H")))) "holds"  (Bool  "("  (Bool (Set (Var "H"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "F"))  ($#k8_group_1 :::"*"::: )  (Set (Var "G")))) "iff" (Bool  "for" (Set (Var "x")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Var "X")) "holds"  (Bool (Set (Set (Var "h"))  ($#k1_seq_1 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "f"))  ($#k1_seq_1 :::"."::: )  (Set (Var "x")) ")" )  ($#k8_real_1 :::"*"::: )  (Set  "(" (Set (Var "g"))  ($#k1_seq_1 :::"."::: )  (Set (Var "x")) ")" ))))  ")" )))) ; 
 
theorem :: C0SP1:15 (Bool  "for" (Set (Var "X")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )   "holds"  (Bool (Set   ($#k4_struct_0 :::"0."::: )  (Set  "("  ($#k7_c0sp1 :::"R_Algebra_of_BoundedFunctions"::: )  (Set (Var "X")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "X"))  ($#k8_funcop_1 :::"-->"::: )  (Set  ($#k6_numbers :::"0"::: ) )))) ; 
 
theorem :: C0SP1:16 (Bool  "for" (Set (Var "X")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )   "holds"  (Bool (Set   ($#k1_group_1 :::"1_"::: )  (Set  "("  ($#k7_c0sp1 :::"R_Algebra_of_BoundedFunctions"::: )  (Set (Var "X")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "X"))  ($#k8_funcop_1 :::"-->"::: )  (Num 1)))) ; 
 definitionlet "X" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )  ; let "F" be    ($#m1_hidden :::"set"::: )  ; assume 
(Bool (Set (Const "F"))  ($#r2_hidden :::"in"::: )  (Set   ($#k6_c0sp1 :::"BoundedFunctions"::: )  (Set (Const "X"))))
 ; func  :::"modetrans":::  "(" "F" "," "X" ")"  ->   ($#m1_subset_1 :::"Function":::) "of" "X" "," (Set  ($#k1_numbers :::"REAL"::: ) ) means :: C0SP1:def 15 (Bool  "("  (Bool it  ($#r1_hidden :::"="::: )  "F") & (Bool (Set it  ($#k2_partfun1 :::"|"::: )  "X") "is"   ($#v1_comseq_2 :::"bounded"::: )  )  ")" ); end; 







:: deftheorem    defines :::"modetrans"::: C0SP1:def 15 :  (Bool  "for" (Set (Var "X")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "F")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "F"))  ($#r2_hidden :::"in"::: )  (Set   ($#k6_c0sp1 :::"BoundedFunctions"::: )  (Set (Var "X"))))) "holds"  (Bool  "for" (Set (Var "b3")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set  ($#k1_numbers :::"REAL"::: ) ) "holds"   (Bool  "("  (Bool (Set (Var "b3"))  ($#r1_hidden :::"="::: )  (Set   ($#k8_c0sp1 :::"modetrans"::: )   "(" (Set (Var "F")) "," (Set (Var "X")) ")" )) "iff" (Bool  "("  (Bool (Set (Var "b3"))  ($#r1_hidden :::"="::: )  (Set (Var "F"))) & (Bool (Set (Set (Var "b3"))  ($#k2_partfun1 :::"|"::: )  (Set (Var "X"))) "is"   ($#v1_comseq_2 :::"bounded"::: )  )  ")" )  ")" )))); 
 definitionlet "X" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )  ; let "f" be   ($#m1_subset_1 :::"Function":::) "of" (Set (Const "X")) "," (Set  ($#k1_numbers :::"REAL"::: ) ); func  :::"PreNorms"::: "f" ->  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )   ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) ) equals :: C0SP1:def 16  "{"  (Set  "("  ($#k18_complex1 :::"abs"::: )  (Set  "(" "f"  ($#k1_seq_1 :::"."::: )  (Set (Var "x")) ")" ) ")" ) where x "is"    ($#m1_subset_1 :::"Element"::: )   "of" "X" : (Bool verum)  "}"  ; end; 






:: deftheorem    defines :::"PreNorms"::: C0SP1:def 16 :  (Bool  "for" (Set (Var "X")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set  ($#k1_numbers :::"REAL"::: ) ) "holds"  (Bool (Set   ($#k9_c0sp1 :::"PreNorms"::: )  (Set (Var "f")))  ($#r1_hidden :::"="::: )   "{"  (Set  "("  ($#k18_complex1 :::"abs"::: )  (Set  "(" (Set (Var "f"))  ($#k1_seq_1 :::"."::: )  (Set (Var "x")) ")" ) ")" ) where x "is"    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Var "X")) : (Bool verum)  "}"  ))); 
 
theorem :: C0SP1:17 (Bool  "for" (Set (Var "X")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set  ($#k1_numbers :::"REAL"::: ) )  "st" (Bool (Bool (Set (Set (Var "f"))  ($#k2_partfun1 :::"|"::: )  (Set (Var "X"))) "is"   ($#v1_comseq_2 :::"bounded"::: )  )) "holds"  (Bool (Set   ($#k9_c0sp1 :::"PreNorms"::: )  (Set (Var "f"))) "is"   ($#v4_xxreal_2 :::"bounded_above"::: )  ))) ; 
 
theorem :: C0SP1:18 (Bool  "for" (Set (Var "X")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set  ($#k1_numbers :::"REAL"::: ) ) "holds"   (Bool  "("  (Bool (Set (Set (Var "f"))  ($#k2_partfun1 :::"|"::: )  (Set (Var "X"))) "is"   ($#v1_comseq_2 :::"bounded"::: )  ) "iff" (Bool (Set   ($#k9_c0sp1 :::"PreNorms"::: )  (Set (Var "f"))) "is"   ($#v4_xxreal_2 :::"bounded_above"::: )  )  ")" ))) ; 
 definitionlet "X" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )  ; func  :::"BoundedFunctionsNorm"::: "X" ->   ($#m1_subset_1 :::"Function":::) "of" (Set  "("  ($#k6_c0sp1 :::"BoundedFunctions"::: )  "X" ")" ) "," (Set  ($#k1_numbers :::"REAL"::: ) ) means :: C0SP1:def 17 (Bool  "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set   ($#k6_c0sp1 :::"BoundedFunctions"::: )  "X"))) "holds"  (Bool (Set it  ($#k1_seq_1 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set   ($#k4_seq_4 :::"upper_bound"::: )  (Set  "("  ($#k9_c0sp1 :::"PreNorms"::: )  (Set  "("  ($#k8_c0sp1 :::"modetrans"::: )   "(" (Set (Var "x")) "," "X" ")"  ")" ) ")" )))); end; 





:: deftheorem    defines :::"BoundedFunctionsNorm"::: C0SP1:def 17 :  (Bool  "for" (Set (Var "X")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "b2")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  "("  ($#k6_c0sp1 :::"BoundedFunctions"::: )  (Set (Var "X")) ")" ) "," (Set  ($#k1_numbers :::"REAL"::: ) ) "holds"   (Bool  "("  (Bool (Set (Var "b2"))  ($#r1_hidden :::"="::: )  (Set   ($#k10_c0sp1 :::"BoundedFunctionsNorm"::: )  (Set (Var "X")))) "iff" (Bool  "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set   ($#k6_c0sp1 :::"BoundedFunctions"::: )  (Set (Var "X"))))) "holds"  (Bool (Set (Set (Var "b2"))  ($#k1_seq_1 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set   ($#k4_seq_4 :::"upper_bound"::: )  (Set  "("  ($#k9_c0sp1 :::"PreNorms"::: )  (Set  "("  ($#k8_c0sp1 :::"modetrans"::: )   "(" (Set (Var "x")) "," (Set (Var "X")) ")"  ")" ) ")" ))))  ")" ))); 
 
theorem :: C0SP1:19 (Bool  "for" (Set (Var "X")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set  ($#k1_numbers :::"REAL"::: ) )  "st" (Bool (Bool (Set (Set (Var "f"))  ($#k2_partfun1 :::"|"::: )  (Set (Var "X"))) "is"   ($#v1_comseq_2 :::"bounded"::: )  )) "holds"  (Bool (Set   ($#k8_c0sp1 :::"modetrans"::: )   "(" (Set (Var "f")) "," (Set (Var "X")) ")" )  ($#r2_relset_1 :::"="::: )  (Set (Var "f"))))) ; 
 
theorem :: C0SP1:20 (Bool  "for" (Set (Var "X")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set  ($#k1_numbers :::"REAL"::: ) )  "st" (Bool (Bool (Set (Set (Var "f"))  ($#k2_partfun1 :::"|"::: )  (Set (Var "X"))) "is"   ($#v1_comseq_2 :::"bounded"::: )  )) "holds"  (Bool (Set (Set  "("  ($#k10_c0sp1 :::"BoundedFunctionsNorm"::: )  (Set (Var "X")) ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "f")))  ($#r1_hidden :::"="::: )  (Set   ($#k4_seq_4 :::"upper_bound"::: )  (Set  "("  ($#k9_c0sp1 :::"PreNorms"::: )  (Set (Var "f")) ")" ))))) ; 
 definitionlet "X" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )  ; func  :::"R_Normed_Algebra_of_BoundedFunctions"::: "X" ->    ($#l1_lopban_2 :::"Normed_AlgebraStr"::: )   equals :: C0SP1:def 18 (Set   ($#g1_lopban_2 :::"Normed_AlgebraStr"::: )  "(#"  (Set  "("  ($#k6_c0sp1 :::"BoundedFunctions"::: )  "X" ")" ) "," (Set  "("  ($#k2_c0sp1 :::"mult_"::: )   "(" (Set  "("  ($#k6_c0sp1 :::"BoundedFunctions"::: )  "X" ")" ) "," (Set  "("  ($#k12_funcsdom :::"RAlgebra"::: )  "X" ")" ) ")"  ")" ) "," (Set  "("  ($#k1_c0sp1 :::"Add_"::: )   "(" (Set  "("  ($#k6_c0sp1 :::"BoundedFunctions"::: )  "X" ")" ) "," (Set  "("  ($#k12_funcsdom :::"RAlgebra"::: )  "X" ")" ) ")"  ")" ) "," (Set  "("  ($#k5_c0sp1 :::"Mult_"::: )   "(" (Set  "("  ($#k6_c0sp1 :::"BoundedFunctions"::: )  "X" ")" ) "," (Set  "("  ($#k12_funcsdom :::"RAlgebra"::: )  "X" ")" ) ")"  ")" ) "," (Set  "("  ($#k4_c0sp1 :::"One_"::: )   "(" (Set  "("  ($#k6_c0sp1 :::"BoundedFunctions"::: )  "X" ")" ) "," (Set  "("  ($#k12_funcsdom :::"RAlgebra"::: )  "X" ")" ) ")"  ")" ) "," (Set  "("  ($#k3_c0sp1 :::"Zero_"::: )   "(" (Set  "("  ($#k6_c0sp1 :::"BoundedFunctions"::: )  "X" ")" ) "," (Set  "("  ($#k12_funcsdom :::"RAlgebra"::: )  "X" ")" ) ")"  ")" ) "," (Set  "("  ($#k10_c0sp1 :::"BoundedFunctionsNorm"::: )  "X" ")" ) "#)" ); end; 





:: deftheorem    defines :::"R_Normed_Algebra_of_BoundedFunctions"::: C0SP1:def 18 :  (Bool  "for" (Set (Var "X")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )   "holds"  (Bool (Set   ($#k11_c0sp1 :::"R_Normed_Algebra_of_BoundedFunctions"::: )  (Set (Var "X")))  ($#r1_hidden :::"="::: )  (Set   ($#g1_lopban_2 :::"Normed_AlgebraStr"::: )  "(#"  (Set  "("  ($#k6_c0sp1 :::"BoundedFunctions"::: )  (Set (Var "X")) ")" ) "," (Set  "("  ($#k2_c0sp1 :::"mult_"::: )   "(" (Set  "("  ($#k6_c0sp1 :::"BoundedFunctions"::: )  (Set (Var "X")) ")" ) "," (Set  "("  ($#k12_funcsdom :::"RAlgebra"::: )  (Set (Var "X")) ")" ) ")"  ")" ) "," (Set  "("  ($#k1_c0sp1 :::"Add_"::: )   "(" (Set  "("  ($#k6_c0sp1 :::"BoundedFunctions"::: )  (Set (Var "X")) ")" ) "," (Set  "("  ($#k12_funcsdom :::"RAlgebra"::: )  (Set (Var "X")) ")" ) ")"  ")" ) "," (Set  "("  ($#k5_c0sp1 :::"Mult_"::: )   "(" (Set  "("  ($#k6_c0sp1 :::"BoundedFunctions"::: )  (Set (Var "X")) ")" ) "," (Set  "("  ($#k12_funcsdom :::"RAlgebra"::: )  (Set (Var "X")) ")" ) ")"  ")" ) "," (Set  "("  ($#k4_c0sp1 :::"One_"::: )   "(" (Set  "("  ($#k6_c0sp1 :::"BoundedFunctions"::: )  (Set (Var "X")) ")" ) "," (Set  "("  ($#k12_funcsdom :::"RAlgebra"::: )  (Set (Var "X")) ")" ) ")"  ")" ) "," (Set  "("  ($#k3_c0sp1 :::"Zero_"::: )   "(" (Set  "("  ($#k6_c0sp1 :::"BoundedFunctions"::: )  (Set (Var "X")) ")" ) "," (Set  "("  ($#k12_funcsdom :::"RAlgebra"::: )  (Set (Var "X")) ")" ) ")"  ")" ) "," (Set  "("  ($#k10_c0sp1 :::"BoundedFunctionsNorm"::: )  (Set (Var "X")) ")" ) "#)" ))); 
 registrationlet "X" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )  ; 
cluster (Set   ($#k11_c0sp1 :::"R_Normed_Algebra_of_BoundedFunctions"::: )  "X") ->  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )  ; 
end; registrationlet "X" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )  ; 
cluster (Set   ($#k11_c0sp1 :::"R_Normed_Algebra_of_BoundedFunctions"::: )  "X") ->   ($#v1_group_1 :::"unital"::: )   ; 
end; 
theorem :: C0SP1:21 (Bool  "for" (Set (Var "W")) "being"    ($#l1_lopban_2 :::"Normed_AlgebraStr"::: )    (Bool  "for" (Set (Var "V")) "being"   ($#l1_funcsdom :::"Algebra":::)  "st" (Bool (Bool (Set   ($#g1_funcsdom :::"AlgebraStr"::: )  "(#"  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "W"))) "," (Set  "the"  ($#u2_algstr_0 :::"multF"::: )  "of" (Set (Var "W"))) "," (Set  "the"  ($#u1_algstr_0 :::"addF"::: )  "of" (Set (Var "W"))) "," (Set  "the"  ($#u1_rlvect_1 :::"Mult"::: )  "of" (Set (Var "W"))) "," (Set  "the"  ($#u3_struct_0 :::"OneF"::: )  "of" (Set (Var "W"))) "," (Set  "the"  ($#u2_struct_0 :::"ZeroF"::: )  "of" (Set (Var "W"))) "#)" )  ($#r1_hidden :::"="::: )  (Set (Var "V")))) "holds"  (Bool (Set (Var "W")) "is"   ($#l1_funcsdom :::"Algebra":::)))) ; 
 





theorem :: C0SP1:22 (Bool  "for" (Set (Var "X")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )   "holds"  (Bool (Set   ($#k11_c0sp1 :::"R_Normed_Algebra_of_BoundedFunctions"::: )  (Set (Var "X"))) "is"   ($#l1_funcsdom :::"Algebra":::))) ; 
 
theorem :: C0SP1:23 (Bool  "for" (Set (Var "X")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "F")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k11_c0sp1 :::"R_Normed_Algebra_of_BoundedFunctions"::: )  (Set (Var "X")) ")" ) "holds"  (Bool (Set (Set  "("  ($#k5_c0sp1 :::"Mult_"::: )   "(" (Set  "("  ($#k6_c0sp1 :::"BoundedFunctions"::: )  (Set (Var "X")) ")" ) "," (Set  "("  ($#k12_funcsdom :::"RAlgebra"::: )  (Set (Var "X")) ")" ) ")"  ")" )  ($#k1_binop_1 :::"."::: )   "(" (Num 1) "," (Set (Var "F")) ")" )  ($#r1_hidden :::"="::: )  (Set (Var "F"))))) ; 
 
theorem :: C0SP1:24 (Bool  "for" (Set (Var "X")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )   "holds"  (Bool (Set   ($#k11_c0sp1 :::"R_Normed_Algebra_of_BoundedFunctions"::: )  (Set (Var "X"))) "is"   ($#l1_rlvect_1 :::"RealLinearSpace":::))) ; 
 
theorem :: C0SP1:25 (Bool  "for" (Set (Var "X")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )   "holds"  (Bool (Set (Set (Var "X"))  ($#k8_funcop_1 :::"-->"::: )  (Set  ($#k6_numbers :::"0"::: ) ))  ($#r1_hidden :::"="::: )  (Set   ($#k4_struct_0 :::"0."::: )  (Set  "("  ($#k11_c0sp1 :::"R_Normed_Algebra_of_BoundedFunctions"::: )  (Set (Var "X")) ")" )))) ; 
 
theorem :: C0SP1:26 (Bool  "for" (Set (Var "X")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "x")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Var "X"))  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set  ($#k1_numbers :::"REAL"::: ) )  (Bool  "for" (Set (Var "F")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k11_c0sp1 :::"R_Normed_Algebra_of_BoundedFunctions"::: )  (Set (Var "X")) ")" )  "st" (Bool (Bool (Set (Var "f"))  ($#r1_hidden :::"="::: )  (Set (Var "F"))) & (Bool (Set (Set (Var "f"))  ($#k2_partfun1 :::"|"::: )  (Set (Var "X"))) "is"   ($#v1_comseq_2 :::"bounded"::: )  )) "holds"  (Bool (Set   ($#k18_complex1 :::"abs"::: )  (Set  "(" (Set (Var "f"))  ($#k1_seq_1 :::"."::: )  (Set (Var "x")) ")" ))  ($#r1_xxreal_0 :::"<="::: )  (Set  ($#k1_normsp_0 :::"||."::: ) (Set (Var "F")) ($#k1_normsp_0 :::".||"::: ) )))))) ; 
 
theorem :: C0SP1:27 (Bool  "for" (Set (Var "X")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "F")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k11_c0sp1 :::"R_Normed_Algebra_of_BoundedFunctions"::: )  (Set (Var "X")) ")" ) "holds"  (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<="::: )  (Set  ($#k1_normsp_0 :::"||."::: ) (Set (Var "F")) ($#k1_normsp_0 :::".||"::: ) )))) ; 
 
theorem :: C0SP1:28 (Bool  "for" (Set (Var "X")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "F")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k11_c0sp1 :::"R_Normed_Algebra_of_BoundedFunctions"::: )  (Set (Var "X")) ")" )  "st" (Bool (Bool (Set (Var "F"))  ($#r1_hidden :::"="::: )  (Set   ($#k4_struct_0 :::"0."::: )  (Set  "("  ($#k11_c0sp1 :::"R_Normed_Algebra_of_BoundedFunctions"::: )  (Set (Var "X")) ")" )))) "holds"  (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_hidden :::"="::: )  (Set  ($#k1_normsp_0 :::"||."::: ) (Set (Var "F")) ($#k1_normsp_0 :::".||"::: ) )))) ; 
 
theorem :: C0SP1:29 (Bool  "for" (Set (Var "X")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "f")) "," (Set (Var "g")) "," (Set (Var "h")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set  ($#k1_numbers :::"REAL"::: ) )  (Bool  "for" (Set (Var "F")) "," (Set (Var "G")) "," (Set (Var "H")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k11_c0sp1 :::"R_Normed_Algebra_of_BoundedFunctions"::: )  (Set (Var "X")) ")" )  "st" (Bool (Bool (Set (Var "f"))  ($#r1_hidden :::"="::: )  (Set (Var "F"))) & (Bool (Set (Var "g"))  ($#r1_hidden :::"="::: )  (Set (Var "G"))) & (Bool (Set (Var "h"))  ($#r1_hidden :::"="::: )  (Set (Var "H")))) "holds"  (Bool  "("  (Bool (Set (Var "H"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "F"))  ($#k1_algstr_0 :::"+"::: )  (Set (Var "G")))) "iff" (Bool  "for" (Set (Var "x")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Var "X")) "holds"  (Bool (Set (Set (Var "h"))  ($#k1_seq_1 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "f"))  ($#k1_seq_1 :::"."::: )  (Set (Var "x")) ")" )  ($#k7_real_1 :::"+"::: )  (Set  "(" (Set (Var "g"))  ($#k1_seq_1 :::"."::: )  (Set (Var "x")) ")" ))))  ")" )))) ; 
 
theorem :: C0SP1:30 (Bool  "for" (Set (Var "X")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Real":::)  (Bool  "for" (Set (Var "f")) "," (Set (Var "g")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set  ($#k1_numbers :::"REAL"::: ) )  (Bool  "for" (Set (Var "F")) "," (Set (Var "G")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k11_c0sp1 :::"R_Normed_Algebra_of_BoundedFunctions"::: )  (Set (Var "X")) ")" )  "st" (Bool (Bool (Set (Var "f"))  ($#r1_hidden :::"="::: )  (Set (Var "F"))) & (Bool (Set (Var "g"))  ($#r1_hidden :::"="::: )  (Set (Var "G")))) "holds"  (Bool  "("  (Bool (Set (Var "G"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "a"))  ($#k1_rlvect_1 :::"*"::: )  (Set (Var "F")))) "iff" (Bool  "for" (Set (Var "x")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Var "X")) "holds"  (Bool (Set (Set (Var "g"))  ($#k1_seq_1 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "a"))  ($#k8_real_1 :::"*"::: )  (Set  "(" (Set (Var "f"))  ($#k1_seq_1 :::"."::: )  (Set (Var "x")) ")" ))))  ")" ))))) ; 
 
theorem :: C0SP1:31 (Bool  "for" (Set (Var "X")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "f")) "," (Set (Var "g")) "," (Set (Var "h")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set  ($#k1_numbers :::"REAL"::: ) )  (Bool  "for" (Set (Var "F")) "," (Set (Var "G")) "," (Set (Var "H")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k11_c0sp1 :::"R_Normed_Algebra_of_BoundedFunctions"::: )  (Set (Var "X")) ")" )  "st" (Bool (Bool (Set (Var "f"))  ($#r1_hidden :::"="::: )  (Set (Var "F"))) & (Bool (Set (Var "g"))  ($#r1_hidden :::"="::: )  (Set (Var "G"))) & (Bool (Set (Var "h"))  ($#r1_hidden :::"="::: )  (Set (Var "H")))) "holds"  (Bool  "("  (Bool (Set (Var "H"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "F"))  ($#k6_algstr_0 :::"*"::: )  (Set (Var "G")))) "iff" (Bool  "for" (Set (Var "x")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Var "X")) "holds"  (Bool (Set (Set (Var "h"))  ($#k1_seq_1 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "f"))  ($#k1_seq_1 :::"."::: )  (Set (Var "x")) ")" )  ($#k8_real_1 :::"*"::: )  (Set  "(" (Set (Var "g"))  ($#k1_seq_1 :::"."::: )  (Set (Var "x")) ")" ))))  ")" )))) ; 
 
theorem :: C0SP1:32 (Bool  "for" (Set (Var "X")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Real":::)  (Bool  "for" (Set (Var "F")) "," (Set (Var "G")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k11_c0sp1 :::"R_Normed_Algebra_of_BoundedFunctions"::: )  (Set (Var "X")) ")" ) "holds"   (Bool  "("   "("  (Bool (Bool (Set  ($#k1_normsp_0 :::"||."::: ) (Set (Var "F")) ($#k1_normsp_0 :::".||"::: ) )  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "implies" (Bool (Set (Var "F"))  ($#r1_hidden :::"="::: )  (Set   ($#k4_struct_0 :::"0."::: )  (Set  "("  ($#k11_c0sp1 :::"R_Normed_Algebra_of_BoundedFunctions"::: )  (Set (Var "X")) ")" )))  ")"  &  "("  (Bool (Bool (Set (Var "F"))  ($#r1_hidden :::"="::: )  (Set   ($#k4_struct_0 :::"0."::: )  (Set  "("  ($#k11_c0sp1 :::"R_Normed_Algebra_of_BoundedFunctions"::: )  (Set (Var "X")) ")" )))) "implies" (Bool (Set  ($#k1_normsp_0 :::"||."::: ) (Set (Var "F")) ($#k1_normsp_0 :::".||"::: ) )  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")"  & (Bool (Set  ($#k1_normsp_0 :::"||."::: ) (Set  "(" (Set (Var "a"))  ($#k1_rlvect_1 :::"*"::: )  (Set (Var "F")) ")" ) ($#k1_normsp_0 :::".||"::: ) )  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k18_complex1 :::"abs"::: )  (Set (Var "a")) ")" )  ($#k8_real_1 :::"*"::: )  (Set  ($#k1_normsp_0 :::"||."::: ) (Set (Var "F")) ($#k1_normsp_0 :::".||"::: ) ))) & (Bool (Set  ($#k1_normsp_0 :::"||."::: ) (Set  "(" (Set (Var "F"))  ($#k1_algstr_0 :::"+"::: )  (Set (Var "G")) ")" ) ($#k1_normsp_0 :::".||"::: ) )  ($#r1_xxreal_0 :::"<="::: )  (Set (Set  ($#k1_normsp_0 :::"||."::: ) (Set (Var "F")) ($#k1_normsp_0 :::".||"::: ) )  ($#k7_real_1 :::"+"::: )  (Set  ($#k1_normsp_0 :::"||."::: ) (Set (Var "G")) ($#k1_normsp_0 :::".||"::: ) )))  ")" )))) ; 
 
theorem :: C0SP1:33 (Bool  "for" (Set (Var "X")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set   ($#k11_c0sp1 :::"R_Normed_Algebra_of_BoundedFunctions"::: )  (Set (Var "X"))) "is"   ($#v4_normsp_0 :::"reflexive"::: )  ) & (Bool (Set   ($#k11_c0sp1 :::"R_Normed_Algebra_of_BoundedFunctions"::: )  (Set (Var "X"))) "is"   ($#v3_normsp_0 :::"discerning"::: )  ) & (Bool (Set   ($#k11_c0sp1 :::"R_Normed_Algebra_of_BoundedFunctions"::: )  (Set (Var "X"))) "is"   ($#v2_normsp_1 :::"RealNormSpace-like"::: )  )  ")" )) ; 
 registrationlet "X" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )  ; 
cluster (Set   ($#k11_c0sp1 :::"R_Normed_Algebra_of_BoundedFunctions"::: )  "X") ->   ($#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"::: )   ; 
end; 
theorem :: C0SP1:34 (Bool  "for" (Set (Var "X")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "f")) "," (Set (Var "g")) "," (Set (Var "h")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set  ($#k1_numbers :::"REAL"::: ) )  (Bool  "for" (Set (Var "F")) "," (Set (Var "G")) "," (Set (Var "H")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k11_c0sp1 :::"R_Normed_Algebra_of_BoundedFunctions"::: )  (Set (Var "X")) ")" )  "st" (Bool (Bool (Set (Var "f"))  ($#r1_hidden :::"="::: )  (Set (Var "F"))) & (Bool (Set (Var "g"))  ($#r1_hidden :::"="::: )  (Set (Var "G"))) & (Bool (Set (Var "h"))  ($#r1_hidden :::"="::: )  (Set (Var "H")))) "holds"  (Bool  "("  (Bool (Set (Var "H"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "F"))  ($#k5_algstr_0 :::"-"::: )  (Set (Var "G")))) "iff" (Bool  "for" (Set (Var "x")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Var "X")) "holds"  (Bool (Set (Set (Var "h"))  ($#k1_seq_1 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "f"))  ($#k1_seq_1 :::"."::: )  (Set (Var "x")) ")" )  ($#k9_real_1 :::"-"::: )  (Set  "(" (Set (Var "g"))  ($#k1_seq_1 :::"."::: )  (Set (Var "x")) ")" ))))  ")" )))) ; 
 
theorem :: C0SP1:35 (Bool  "for" (Set (Var "X")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "seq")) "being"   ($#m1_subset_1 :::"sequence":::) "of" (Set  "("  ($#k11_c0sp1 :::"R_Normed_Algebra_of_BoundedFunctions"::: )  (Set (Var "X")) ")" )  "st" (Bool (Bool (Set (Var "seq")) "is"   ($#v1_rsspace3 :::"Cauchy_sequence_by_Norm"::: )  )) "holds"  (Bool (Set (Var "seq")) "is"   ($#v3_normsp_1 :::"convergent"::: )  ))) ; 
 
theorem :: C0SP1:36 (Bool  "for" (Set (Var "X")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )   "holds"  (Bool (Set   ($#k11_c0sp1 :::"R_Normed_Algebra_of_BoundedFunctions"::: )  (Set (Var "X"))) "is"   ($#l1_normsp_1 :::"RealBanachSpace":::))) ; 
 registrationlet "X" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )  ; 
cluster (Set   ($#k11_c0sp1 :::"R_Normed_Algebra_of_BoundedFunctions"::: )  "X") ->   ($#v3_lopban_1 :::"complete"::: )   ; 
end; 
theorem :: C0SP1:37 (Bool  "for" (Set (Var "X")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )   "holds"  (Bool (Set   ($#k11_c0sp1 :::"R_Normed_Algebra_of_BoundedFunctions"::: )  (Set (Var "X"))) "is"   ($#l1_lopban_2 :::"Banach_Algebra":::))) ;