:: LOPBAN_1  semantic presentation begin  definitionlet "X" be    ($#m1_hidden :::"set"::: )  ; let "Y" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )  ; let "F" be   ($#m1_subset_1 :::"Function":::) "of" (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set  ($#k1_numbers :::"REAL"::: ) ) "," (Set (Const "Y")) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set (Const "Y")); let "a" be   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )  ; let "f" be   ($#m1_subset_1 :::"Function":::) "of" (Set (Const "X")) "," (Set (Const "Y")); :: original: :::"[;]"::: redefine func "F" :::"[;]":::  "(" "a" "," "f" ")"  ->    ($#m2_funct_2 :::"Element"::: )   "of" (Set   ($#k9_funct_2 :::"Funcs"::: )   "(" "X" "," "Y" ")" ); end; definitionlet "X" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )  ; let "Y" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l2_algstr_0 :::"addLoopStr"::: )  ; func  :::"FuncAdd":::  "(" "X" "," "Y" ")"  ->   ($#m1_subset_1 :::"BinOp":::) "of" (Set  "("  ($#k9_funct_2 :::"Funcs"::: )   "(" "X" "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "Y") ")"  ")" ) means :: LOPBAN_1:def 1 (Bool  "for" (Set (Var "f")) "," (Set (Var "g")) "being"    ($#m2_funct_2 :::"Element"::: )   "of" (Set   ($#k9_funct_2 :::"Funcs"::: )   "(" "X" "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "Y") ")" ) "holds"  (Bool (Set it  ($#k1_funcsdom :::"."::: )   "(" (Set (Var "f")) "," (Set (Var "g")) ")" )  ($#r2_funct_2 :::"="::: )  (Set (Set  "the"  ($#u1_algstr_0 :::"addF"::: )  "of" "Y")  ($#k3_funcsdom :::".:"::: )   "(" (Set (Var "f")) "," (Set (Var "g")) ")" ))); end; 






:: deftheorem    defines :::"FuncAdd"::: LOPBAN_1:def 1 :  (Bool  "for" (Set (Var "X")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "Y")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l2_algstr_0 :::"addLoopStr"::: )    (Bool  "for" (Set (Var "b3")) "being"   ($#m1_subset_1 :::"BinOp":::) "of" (Set  "("  ($#k9_funct_2 :::"Funcs"::: )   "(" (Set (Var "X")) "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "Y"))) ")"  ")" ) "holds"   (Bool  "("  (Bool (Set (Var "b3"))  ($#r1_hidden :::"="::: )  (Set   ($#k2_lopban_1 :::"FuncAdd"::: )   "(" (Set (Var "X")) "," (Set (Var "Y")) ")" )) "iff" (Bool  "for" (Set (Var "f")) "," (Set (Var "g")) "being"    ($#m2_funct_2 :::"Element"::: )   "of" (Set   ($#k9_funct_2 :::"Funcs"::: )   "(" (Set (Var "X")) "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "Y"))) ")" ) "holds"  (Bool (Set (Set (Var "b3"))  ($#k1_funcsdom :::"."::: )   "(" (Set (Var "f")) "," (Set (Var "g")) ")" )  ($#r2_funct_2 :::"="::: )  (Set (Set  "the"  ($#u1_algstr_0 :::"addF"::: )  "of" (Set (Var "Y")))  ($#k3_funcsdom :::".:"::: )   "(" (Set (Var "f")) "," (Set (Var "g")) ")" )))  ")" )))); 
 definitionlet "X" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )  ; let "Y" be   ($#l1_rlvect_1 :::"RealLinearSpace":::); func  :::"FuncExtMult":::  "(" "X" "," "Y" ")"  ->   ($#m1_subset_1 :::"Function":::) "of" (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set  ($#k1_numbers :::"REAL"::: ) ) "," (Set  "("  ($#k9_funct_2 :::"Funcs"::: )   "(" "X" "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "Y") ")"  ")" ) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set  "("  ($#k9_funct_2 :::"Funcs"::: )   "(" "X" "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "Y") ")"  ")" ) means :: LOPBAN_1:def 2 (Bool  "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Real":::)  (Bool  "for" (Set (Var "f")) "being"    ($#m2_funct_2 :::"Element"::: )   "of" (Set   ($#k9_funct_2 :::"Funcs"::: )   "(" "X" "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "Y") ")" )  (Bool  "for" (Set (Var "x")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" "X" "holds"  (Bool (Set (Set  "(" it  ($#k2_funcsdom :::"."::: )  (Set  ($#k1_domain_1 :::"["::: ) (Set (Var "a")) "," (Set (Var "f")) ($#k1_domain_1 :::"]"::: ) ) ")" )  ($#k3_funct_2 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "a"))  ($#k1_rlvect_1 :::"*"::: )  (Set  "(" (Set (Var "f"))  ($#k3_funct_2 :::"."::: )  (Set (Var "x")) ")" )))))); end; 






:: deftheorem    defines :::"FuncExtMult"::: LOPBAN_1:def 2 :  (Bool  "for" (Set (Var "X")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "Y")) "being"   ($#l1_rlvect_1 :::"RealLinearSpace":::)  (Bool  "for" (Set (Var "b3")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set  ($#k1_numbers :::"REAL"::: ) ) "," (Set  "("  ($#k9_funct_2 :::"Funcs"::: )   "(" (Set (Var "X")) "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "Y"))) ")"  ")" ) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set  "("  ($#k9_funct_2 :::"Funcs"::: )   "(" (Set (Var "X")) "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "Y"))) ")"  ")" ) "holds"   (Bool  "("  (Bool (Set (Var "b3"))  ($#r1_hidden :::"="::: )  (Set   ($#k3_lopban_1 :::"FuncExtMult"::: )   "(" (Set (Var "X")) "," (Set (Var "Y")) ")" )) "iff" (Bool  "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Real":::)  (Bool  "for" (Set (Var "f")) "being"    ($#m2_funct_2 :::"Element"::: )   "of" (Set   ($#k9_funct_2 :::"Funcs"::: )   "(" (Set (Var "X")) "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "Y"))) ")" )  (Bool  "for" (Set (Var "x")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Var "X")) "holds"  (Bool (Set (Set  "(" (Set (Var "b3"))  ($#k2_funcsdom :::"."::: )  (Set  ($#k1_domain_1 :::"["::: ) (Set (Var "a")) "," (Set (Var "f")) ($#k1_domain_1 :::"]"::: ) ) ")" )  ($#k3_funct_2 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "a"))  ($#k1_rlvect_1 :::"*"::: )  (Set  "(" (Set (Var "f"))  ($#k3_funct_2 :::"."::: )  (Set (Var "x")) ")" ))))))  ")" )))); 
 definitionlet "X" be    ($#m1_hidden :::"set"::: )  ; let "Y" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l2_struct_0 :::"ZeroStr"::: )  ; func  :::"FuncZero":::  "(" "X" "," "Y" ")"  ->    ($#m2_funct_2 :::"Element"::: )   "of" (Set   ($#k9_funct_2 :::"Funcs"::: )   "(" "X" "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "Y") ")" ) equals :: LOPBAN_1:def 3 (Set "X"  ($#k8_funcop_1 :::"-->"::: )  (Set  "("  ($#k4_struct_0 :::"0."::: )  "Y" ")" )); end; 






:: deftheorem    defines :::"FuncZero"::: LOPBAN_1:def 3 :  (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "Y")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l2_struct_0 :::"ZeroStr"::: )   "holds"  (Bool (Set   ($#k4_lopban_1 :::"FuncZero"::: )   "(" (Set (Var "X")) "," (Set (Var "Y")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set (Var "X"))  ($#k8_funcop_1 :::"-->"::: )  (Set  "("  ($#k4_struct_0 :::"0."::: )  (Set (Var "Y")) ")" ))))); 
 











theorem :: LOPBAN_1:1 (Bool  "for" (Set (Var "X")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "Y")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l2_algstr_0 :::"addLoopStr"::: )    (Bool  "for" (Set (Var "f")) "," (Set (Var "g")) "," (Set (Var "h")) "being"    ($#m2_funct_2 :::"Element"::: )   "of" (Set   ($#k9_funct_2 :::"Funcs"::: )   "(" (Set (Var "X")) "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "Y"))) ")" ) "holds"   (Bool  "("  (Bool (Set (Var "h"))  ($#r2_funct_2 :::"="::: )  (Set (Set  "("  ($#k2_lopban_1 :::"FuncAdd"::: )   "(" (Set (Var "X")) "," (Set (Var "Y")) ")"  ")" )  ($#k1_funcsdom :::"."::: )   "(" (Set (Var "f")) "," (Set (Var "g")) ")" )) "iff" (Bool  "for" (Set (Var "x")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Var "X")) "holds"  (Bool (Set (Set (Var "h"))  ($#k3_funct_2 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "f"))  ($#k3_funct_2 :::"."::: )  (Set (Var "x")) ")" )  ($#k1_algstr_0 :::"+"::: )  (Set  "(" (Set (Var "g"))  ($#k3_funct_2 :::"."::: )  (Set (Var "x")) ")" ))))  ")" )))) ; 
 




theorem :: LOPBAN_1:2 (Bool  "for" (Set (Var "X")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "Y")) "being"   ($#l1_rlvect_1 :::"RealLinearSpace":::)  (Bool  "for" (Set (Var "h")) "," (Set (Var "f")) "being"    ($#m2_funct_2 :::"Element"::: )   "of" (Set   ($#k9_funct_2 :::"Funcs"::: )   "(" (Set (Var "X")) "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "Y"))) ")" )  (Bool  "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Real":::) "holds"   (Bool  "("  (Bool (Set (Var "h"))  ($#r2_funct_2 :::"="::: )  (Set (Set  "("  ($#k3_lopban_1 :::"FuncExtMult"::: )   "(" (Set (Var "X")) "," (Set (Var "Y")) ")"  ")" )  ($#k2_funcsdom :::"."::: )  (Set  ($#k1_domain_1 :::"["::: ) (Set (Var "a")) "," (Set (Var "f")) ($#k1_domain_1 :::"]"::: ) ))) "iff" (Bool  "for" (Set (Var "x")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Var "X")) "holds"  (Bool (Set (Set (Var "h"))  ($#k3_funct_2 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "a"))  ($#k1_rlvect_1 :::"*"::: )  (Set  "(" (Set (Var "f"))  ($#k3_funct_2 :::"."::: )  (Set (Var "x")) ")" ))))  ")" ))))) ; 
 





theorem :: LOPBAN_1:3 (Bool  "for" (Set (Var "X")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "Y")) "being"   ($#l1_rlvect_1 :::"RealLinearSpace":::)  (Bool  "for" (Set (Var "f")) "," (Set (Var "g")) "being"    ($#m2_funct_2 :::"Element"::: )   "of" (Set   ($#k9_funct_2 :::"Funcs"::: )   "(" (Set (Var "X")) "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "Y"))) ")" ) "holds"  (Bool (Set (Set  "("  ($#k2_lopban_1 :::"FuncAdd"::: )   "(" (Set (Var "X")) "," (Set (Var "Y")) ")"  ")" )  ($#k1_funcsdom :::"."::: )   "(" (Set (Var "f")) "," (Set (Var "g")) ")" )  ($#r2_funct_2 :::"="::: )  (Set (Set  "("  ($#k2_lopban_1 :::"FuncAdd"::: )   "(" (Set (Var "X")) "," (Set (Var "Y")) ")"  ")" )  ($#k1_funcsdom :::"."::: )   "(" (Set (Var "g")) "," (Set (Var "f")) ")" ))))) ; 
 
theorem :: LOPBAN_1:4 (Bool  "for" (Set (Var "X")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "Y")) "being"   ($#l1_rlvect_1 :::"RealLinearSpace":::)  (Bool  "for" (Set (Var "f")) "," (Set (Var "g")) "," (Set (Var "h")) "being"    ($#m2_funct_2 :::"Element"::: )   "of" (Set   ($#k9_funct_2 :::"Funcs"::: )   "(" (Set (Var "X")) "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "Y"))) ")" ) "holds"  (Bool (Set (Set  "("  ($#k2_lopban_1 :::"FuncAdd"::: )   "(" (Set (Var "X")) "," (Set (Var "Y")) ")"  ")" )  ($#k1_funcsdom :::"."::: )   "(" (Set (Var "f")) "," (Set  "(" (Set  "("  ($#k2_lopban_1 :::"FuncAdd"::: )   "(" (Set (Var "X")) "," (Set (Var "Y")) ")"  ")" )  ($#k1_funcsdom :::"."::: )   "(" (Set (Var "g")) "," (Set (Var "h")) ")"  ")" ) ")" )  ($#r2_funct_2 :::"="::: )  (Set (Set  "("  ($#k2_lopban_1 :::"FuncAdd"::: )   "(" (Set (Var "X")) "," (Set (Var "Y")) ")"  ")" )  ($#k1_funcsdom :::"."::: )   "(" (Set  "(" (Set  "("  ($#k2_lopban_1 :::"FuncAdd"::: )   "(" (Set (Var "X")) "," (Set (Var "Y")) ")"  ")" )  ($#k1_funcsdom :::"."::: )   "(" (Set (Var "f")) "," (Set (Var "g")) ")"  ")" ) "," (Set (Var "h")) ")" ))))) ; 
 
theorem :: LOPBAN_1:5 (Bool  "for" (Set (Var "X")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "Y")) "being"   ($#l1_rlvect_1 :::"RealLinearSpace":::)  (Bool  "for" (Set (Var "f")) "being"    ($#m2_funct_2 :::"Element"::: )   "of" (Set   ($#k9_funct_2 :::"Funcs"::: )   "(" (Set (Var "X")) "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "Y"))) ")" ) "holds"  (Bool (Set (Set  "("  ($#k2_lopban_1 :::"FuncAdd"::: )   "(" (Set (Var "X")) "," (Set (Var "Y")) ")"  ")" )  ($#k1_funcsdom :::"."::: )   "(" (Set  "("  ($#k4_lopban_1 :::"FuncZero"::: )   "(" (Set (Var "X")) "," (Set (Var "Y")) ")"  ")" ) "," (Set (Var "f")) ")" )  ($#r2_funct_2 :::"="::: )  (Set (Var "f")))))) ; 
 
theorem :: LOPBAN_1:6 (Bool  "for" (Set (Var "X")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "Y")) "being"   ($#l1_rlvect_1 :::"RealLinearSpace":::)  (Bool  "for" (Set (Var "f")) "being"    ($#m2_funct_2 :::"Element"::: )   "of" (Set   ($#k9_funct_2 :::"Funcs"::: )   "(" (Set (Var "X")) "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "Y"))) ")" ) "holds"  (Bool (Set (Set  "("  ($#k2_lopban_1 :::"FuncAdd"::: )   "(" (Set (Var "X")) "," (Set (Var "Y")) ")"  ")" )  ($#k1_funcsdom :::"."::: )   "(" (Set (Var "f")) "," (Set  "(" (Set  "("  ($#k3_lopban_1 :::"FuncExtMult"::: )   "(" (Set (Var "X")) "," (Set (Var "Y")) ")"  ")" )  ($#k2_funcsdom :::"."::: )  (Set  ($#k1_domain_1 :::"["::: ) (Set  "("  ($#k1_real_1 :::"-"::: )  (Num 1) ")" ) "," (Set (Var "f")) ($#k1_domain_1 :::"]"::: ) ) ")" ) ")" )  ($#r2_funct_2 :::"="::: )  (Set   ($#k4_lopban_1 :::"FuncZero"::: )   "(" (Set (Var "X")) "," (Set (Var "Y")) ")" ))))) ; 
 
theorem :: LOPBAN_1:7 (Bool  "for" (Set (Var "X")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "Y")) "being"   ($#l1_rlvect_1 :::"RealLinearSpace":::)  (Bool  "for" (Set (Var "f")) "being"    ($#m2_funct_2 :::"Element"::: )   "of" (Set   ($#k9_funct_2 :::"Funcs"::: )   "(" (Set (Var "X")) "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "Y"))) ")" ) "holds"  (Bool (Set (Set  "("  ($#k3_lopban_1 :::"FuncExtMult"::: )   "(" (Set (Var "X")) "," (Set (Var "Y")) ")"  ")" )  ($#k1_funct_1 :::"."::: )  (Set  ($#k1_domain_1 :::"["::: ) (Num 1) "," (Set (Var "f")) ($#k1_domain_1 :::"]"::: ) ))  ($#r1_hidden :::"="::: )  (Set (Var "f")))))) ; 
 
theorem :: LOPBAN_1:8 (Bool  "for" (Set (Var "X")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "Y")) "being"   ($#l1_rlvect_1 :::"RealLinearSpace":::)  (Bool  "for" (Set (Var "f")) "being"    ($#m2_funct_2 :::"Element"::: )   "of" (Set   ($#k9_funct_2 :::"Funcs"::: )   "(" (Set (Var "X")) "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "Y"))) ")" )  (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_subset_1 :::"Real":::) "holds"  (Bool (Set (Set  "("  ($#k3_lopban_1 :::"FuncExtMult"::: )   "(" (Set (Var "X")) "," (Set (Var "Y")) ")"  ")" )  ($#k2_funcsdom :::"."::: )  (Set  ($#k1_domain_1 :::"["::: ) (Set (Var "a")) "," (Set  "(" (Set  "("  ($#k3_lopban_1 :::"FuncExtMult"::: )   "(" (Set (Var "X")) "," (Set (Var "Y")) ")"  ")" )  ($#k2_funcsdom :::"."::: )  (Set  ($#k1_domain_1 :::"["::: ) (Set (Var "b")) "," (Set (Var "f")) ($#k1_domain_1 :::"]"::: ) ) ")" ) ($#k1_domain_1 :::"]"::: ) ))  ($#r2_funct_2 :::"="::: )  (Set (Set  "("  ($#k3_lopban_1 :::"FuncExtMult"::: )   "(" (Set (Var "X")) "," (Set (Var "Y")) ")"  ")" )  ($#k2_funcsdom :::"."::: )  (Set  ($#k1_domain_1 :::"["::: ) (Set  "(" (Set (Var "a"))  ($#k8_real_1 :::"*"::: )  (Set (Var "b")) ")" ) "," (Set (Var "f")) ($#k1_domain_1 :::"]"::: ) ))))))) ; 
 
theorem :: LOPBAN_1:9 (Bool  "for" (Set (Var "X")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "Y")) "being"   ($#l1_rlvect_1 :::"RealLinearSpace":::)  (Bool  "for" (Set (Var "f")) "being"    ($#m2_funct_2 :::"Element"::: )   "of" (Set   ($#k9_funct_2 :::"Funcs"::: )   "(" (Set (Var "X")) "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "Y"))) ")" )  (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_subset_1 :::"Real":::) "holds"  (Bool (Set (Set  "("  ($#k2_lopban_1 :::"FuncAdd"::: )   "(" (Set (Var "X")) "," (Set (Var "Y")) ")"  ")" )  ($#k1_funcsdom :::"."::: )   "(" (Set  "(" (Set  "("  ($#k3_lopban_1 :::"FuncExtMult"::: )   "(" (Set (Var "X")) "," (Set (Var "Y")) ")"  ")" )  ($#k2_funcsdom :::"."::: )  (Set  ($#k1_domain_1 :::"["::: ) (Set (Var "a")) "," (Set (Var "f")) ($#k1_domain_1 :::"]"::: ) ) ")" ) "," (Set  "(" (Set  "("  ($#k3_lopban_1 :::"FuncExtMult"::: )   "(" (Set (Var "X")) "," (Set (Var "Y")) ")"  ")" )  ($#k2_funcsdom :::"."::: )  (Set  ($#k1_domain_1 :::"["::: ) (Set (Var "b")) "," (Set (Var "f")) ($#k1_domain_1 :::"]"::: ) ) ")" ) ")" )  ($#r2_funct_2 :::"="::: )  (Set (Set  "("  ($#k3_lopban_1 :::"FuncExtMult"::: )   "(" (Set (Var "X")) "," (Set (Var "Y")) ")"  ")" )  ($#k2_funcsdom :::"."::: )  (Set  ($#k1_domain_1 :::"["::: ) (Set  "(" (Set (Var "a"))  ($#k7_real_1 :::"+"::: )  (Set (Var "b")) ")" ) "," (Set (Var "f")) ($#k1_domain_1 :::"]"::: ) ))))))) ; 
 
theorem :: LOPBAN_1:10 (Bool  "for" (Set (Var "X")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "Y")) "being"   ($#l1_rlvect_1 :::"RealLinearSpace":::) "holds"  (Bool (Set   ($#g1_rlvect_1 :::"RLSStruct"::: )  "(#"  (Set  "("  ($#k9_funct_2 :::"Funcs"::: )   "(" (Set (Var "X")) "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "Y"))) ")"  ")" ) "," (Set  "("  ($#k4_lopban_1 :::"FuncZero"::: )   "(" (Set (Var "X")) "," (Set (Var "Y")) ")"  ")" ) "," (Set  "("  ($#k2_lopban_1 :::"FuncAdd"::: )   "(" (Set (Var "X")) "," (Set (Var "Y")) ")"  ")" ) "," (Set  "("  ($#k3_lopban_1 :::"FuncExtMult"::: )   "(" (Set (Var "X")) "," (Set (Var "Y")) ")"  ")" ) "#)" ) "is"   ($#l1_rlvect_1 :::"RealLinearSpace":::)))) ; 
 definitionlet "X" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )  ; let "Y" be   ($#l1_rlvect_1 :::"RealLinearSpace":::); func  :::"RealVectSpace":::  "(" "X" "," "Y" ")"  ->   ($#l1_rlvect_1 :::"RealLinearSpace":::) equals :: LOPBAN_1:def 4 (Set   ($#g1_rlvect_1 :::"RLSStruct"::: )  "(#"  (Set  "("  ($#k9_funct_2 :::"Funcs"::: )   "(" "X" "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "Y") ")"  ")" ) "," (Set  "("  ($#k4_lopban_1 :::"FuncZero"::: )   "(" "X" "," "Y" ")"  ")" ) "," (Set  "("  ($#k2_lopban_1 :::"FuncAdd"::: )   "(" "X" "," "Y" ")"  ")" ) "," (Set  "("  ($#k3_lopban_1 :::"FuncExtMult"::: )   "(" "X" "," "Y" ")"  ")" ) "#)" ); end; 






:: deftheorem    defines :::"RealVectSpace"::: LOPBAN_1:def 4 :  (Bool  "for" (Set (Var "X")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "Y")) "being"   ($#l1_rlvect_1 :::"RealLinearSpace":::) "holds"  (Bool (Set   ($#k5_lopban_1 :::"RealVectSpace"::: )   "(" (Set (Var "X")) "," (Set (Var "Y")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#g1_rlvect_1 :::"RLSStruct"::: )  "(#"  (Set  "("  ($#k9_funct_2 :::"Funcs"::: )   "(" (Set (Var "X")) "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "Y"))) ")"  ")" ) "," (Set  "("  ($#k4_lopban_1 :::"FuncZero"::: )   "(" (Set (Var "X")) "," (Set (Var "Y")) ")"  ")" ) "," (Set  "("  ($#k2_lopban_1 :::"FuncAdd"::: )   "(" (Set (Var "X")) "," (Set (Var "Y")) ")"  ")" ) "," (Set  "("  ($#k3_lopban_1 :::"FuncExtMult"::: )   "(" (Set (Var "X")) "," (Set (Var "Y")) ")"  ")" ) "#)" )))); 
 registrationlet "X" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )  ; let "Y" be   ($#l1_rlvect_1 :::"RealLinearSpace":::); 
cluster (Set   ($#k5_lopban_1 :::"RealVectSpace"::: )   "(" "X" "," "Y" ")" ) ->   ($#v1_rlvect_1 :::"strict"::: )   ; 
end; registrationlet "X" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )  ; let "Y" be   ($#l1_rlvect_1 :::"RealLinearSpace":::); 
cluster (Set   ($#k5_lopban_1 :::"RealVectSpace"::: )   "(" "X" "," "Y" ")" ) ->   ($#v1_monoid_0 :::"constituted-Functions"::: )   ; 
end; definitionlet "X" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )  ; let "Y" be   ($#l1_rlvect_1 :::"RealLinearSpace":::); let "f" be   ($#m1_subset_1 :::"VECTOR":::) "of" (Set  "("  ($#k5_lopban_1 :::"RealVectSpace"::: )   "(" (Set (Const "X")) "," (Set (Const "Y")) ")"  ")" ); let "x" be    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Const "X")); :: original: :::"."::: redefine func "f" :::"."::: "x" ->   ($#m1_subset_1 :::"VECTOR":::) "of" "Y"; end; 
theorem :: LOPBAN_1:11 (Bool  "for" (Set (Var "X")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "Y")) "being"   ($#l1_rlvect_1 :::"RealLinearSpace":::)  (Bool  "for" (Set (Var "f")) "," (Set (Var "g")) "," (Set (Var "h")) "being"   ($#m1_subset_1 :::"VECTOR":::) "of" (Set  "("  ($#k5_lopban_1 :::"RealVectSpace"::: )   "(" (Set (Var "X")) "," (Set (Var "Y")) ")"  ")" ) "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"))  ($#k6_lopban_1 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "f"))  ($#k6_lopban_1 :::"."::: )  (Set (Var "x")) ")" )  ($#k3_rlvect_1 :::"+"::: )  (Set  "(" (Set (Var "g"))  ($#k6_lopban_1 :::"."::: )  (Set (Var "x")) ")" ))))  ")" )))) ; 
 
theorem :: LOPBAN_1:12 (Bool  "for" (Set (Var "X")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "Y")) "being"   ($#l1_rlvect_1 :::"RealLinearSpace":::)  (Bool  "for" (Set (Var "f")) "," (Set (Var "h")) "being"   ($#m1_subset_1 :::"VECTOR":::) "of" (Set  "("  ($#k5_lopban_1 :::"RealVectSpace"::: )   "(" (Set (Var "X")) "," (Set (Var "Y")) ")"  ")" )  (Bool  "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Real":::) "holds"   (Bool  "("  (Bool (Set (Var "h"))  ($#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 "h"))  ($#k6_lopban_1 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "a"))  ($#k1_rlvect_1 :::"*"::: )  (Set  "(" (Set (Var "f"))  ($#k6_lopban_1 :::"."::: )  (Set (Var "x")) ")" ))))  ")" ))))) ; 
 
theorem :: LOPBAN_1:13 (Bool  "for" (Set (Var "X")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "Y")) "being"   ($#l1_rlvect_1 :::"RealLinearSpace":::) "holds"  (Bool (Set   ($#k4_struct_0 :::"0."::: )  (Set  "("  ($#k5_lopban_1 :::"RealVectSpace"::: )   "(" (Set (Var "X")) "," (Set (Var "Y")) ")"  ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "X"))  ($#k8_funcop_1 :::"-->"::: )  (Set  "("  ($#k4_struct_0 :::"0."::: )  (Set (Var "Y")) ")" ))))) ; 
 begin  definitionlet "X", "Y" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_rlvect_1 :::"RLSStruct"::: )  ; let "IT" be   ($#m1_subset_1 :::"Function":::) "of" (Set (Const "X")) "," (Set (Const "Y")); attr "IT" is  :::"homogeneous":::  means :: LOPBAN_1:def 5 (Bool  "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"VECTOR":::) "of" "X"  (Bool  "for" (Set (Var "r")) "being"   ($#m1_subset_1 :::"Real":::) "holds"  (Bool (Set "IT"  ($#k3_funct_2 :::"."::: )  (Set  "(" (Set (Var "r"))  ($#k1_rlvect_1 :::"*"::: )  (Set (Var "x")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "r"))  ($#k1_rlvect_1 :::"*"::: )  (Set  "(" "IT"  ($#k3_funct_2 :::"."::: )  (Set (Var "x")) ")" ))))); end; 






:: deftheorem    defines :::"homogeneous"::: LOPBAN_1:def 5 :  (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_rlvect_1 :::"RLSStruct"::: )    (Bool  "for" (Set (Var "IT")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "Y")) "holds"   (Bool  "("  (Bool (Set (Var "IT")) "is"   ($#v1_lopban_1 :::"homogeneous"::: )  ) "iff" (Bool  "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "X"))  (Bool  "for" (Set (Var "r")) "being"   ($#m1_subset_1 :::"Real":::) "holds"  (Bool (Set (Set (Var "IT"))  ($#k3_funct_2 :::"."::: )  (Set  "(" (Set (Var "r"))  ($#k1_rlvect_1 :::"*"::: )  (Set (Var "x")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "r"))  ($#k1_rlvect_1 :::"*"::: )  (Set  "(" (Set (Var "IT"))  ($#k3_funct_2 :::"."::: )  (Set (Var "x")) ")" )))))  ")" ))); 
 registrationlet "X" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_rlvect_1 :::"RLSStruct"::: )  ; let "Y" be   ($#l1_rlvect_1 :::"RealLinearSpace":::); 
cluster  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v1_relat_1 :::"Relation-like"::: )   (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "X")  ($#v4_relat_1 :::"-defined"::: )   (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "Y")  ($#v5_relat_1 :::"-valued"::: )     ($#v1_funct_1 :::"Function-like"::: )     ($#v1_partfun1 :::"total"::: )     ($#v1_funct_2 :::"quasi_total"::: )     ($#v13_vectsp_1 :::"additive"::: )     ($#v1_lopban_1 :::"homogeneous"::: )    for    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k1_zfmisc_1 :::"bool"::: )  (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "X") "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "Y") ($#k2_zfmisc_1 :::":]"::: ) )); 
end; definitionlet "X", "Y" be   ($#l1_rlvect_1 :::"RealLinearSpace":::); mode LinearOperator of "X" "," "Y" is   ($#v13_vectsp_1 :::"additive"::: )     ($#v1_lopban_1 :::"homogeneous"::: )    ($#m1_subset_1 :::"Function":::) "of" "X" "," "Y"; end; definitionlet "X", "Y" be   ($#l1_rlvect_1 :::"RealLinearSpace":::); func  :::"LinearOperators":::  "(" "X" "," "Y" ")"  ->   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k5_lopban_1 :::"RealVectSpace"::: )   "(" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "X") "," "Y" ")"  ")" ) means :: LOPBAN_1:def 6 (Bool  "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  it) "iff" (Bool (Set (Var "x")) "is"   ($#m1_subset_1 :::"LinearOperator":::) "of" "X" "," "Y")  ")" )); end; 






:: deftheorem    defines :::"LinearOperators"::: LOPBAN_1:def 6 :  (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "being"   ($#l1_rlvect_1 :::"RealLinearSpace":::)  (Bool  "for" (Set (Var "b3")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k5_lopban_1 :::"RealVectSpace"::: )   "(" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "X"))) "," (Set (Var "Y")) ")"  ")" ) "holds"   (Bool  "("  (Bool (Set (Var "b3"))  ($#r1_hidden :::"="::: )  (Set   ($#k7_lopban_1 :::"LinearOperators"::: )   "(" (Set (Var "X")) "," (Set (Var "Y")) ")" )) "iff" (Bool  "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "b3"))) "iff" (Bool (Set (Var "x")) "is"   ($#m1_subset_1 :::"LinearOperator":::) "of" (Set (Var "X")) "," (Set (Var "Y")))  ")" ))  ")" ))); 
 registrationlet "X", "Y" be   ($#l1_rlvect_1 :::"RealLinearSpace":::); 
cluster (Set   ($#k7_lopban_1 :::"LinearOperators"::: )   "(" "X" "," "Y" ")" ) ->  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v4_funct_1 :::"functional"::: )   ; 
end; 
theorem :: LOPBAN_1:14 (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "being"   ($#l1_rlvect_1 :::"RealLinearSpace":::) "holds"  (Bool (Set   ($#k7_lopban_1 :::"LinearOperators"::: )   "(" (Set (Var "X")) "," (Set (Var "Y")) ")" ) "is"   ($#v1_rlsub_1 :::"linearly-closed"::: )  )) ; 
 
theorem :: LOPBAN_1:15 (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "being"   ($#l1_rlvect_1 :::"RealLinearSpace":::) "holds"  (Bool (Set   ($#g1_rlvect_1 :::"RLSStruct"::: )  "(#"  (Set  "("  ($#k7_lopban_1 :::"LinearOperators"::: )   "(" (Set (Var "X")) "," (Set (Var "Y")) ")"  ")" ) "," (Set  "("  ($#k10_rsspace :::"Zero_"::: )   "(" (Set  "("  ($#k7_lopban_1 :::"LinearOperators"::: )   "(" (Set (Var "X")) "," (Set (Var "Y")) ")"  ")" ) "," (Set  "("  ($#k5_lopban_1 :::"RealVectSpace"::: )   "(" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "X"))) "," (Set (Var "Y")) ")"  ")" ) ")"  ")" ) "," (Set  "("  ($#k8_rsspace :::"Add_"::: )   "(" (Set  "("  ($#k7_lopban_1 :::"LinearOperators"::: )   "(" (Set (Var "X")) "," (Set (Var "Y")) ")"  ")" ) "," (Set  "("  ($#k5_lopban_1 :::"RealVectSpace"::: )   "(" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "X"))) "," (Set (Var "Y")) ")"  ")" ) ")"  ")" ) "," (Set  "("  ($#k9_rsspace :::"Mult_"::: )   "(" (Set  "("  ($#k7_lopban_1 :::"LinearOperators"::: )   "(" (Set (Var "X")) "," (Set (Var "Y")) ")"  ")" ) "," (Set  "("  ($#k5_lopban_1 :::"RealVectSpace"::: )   "(" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "X"))) "," (Set (Var "Y")) ")"  ")" ) ")"  ")" ) "#)" ) "is"    ($#m1_rlsub_1 :::"Subspace"::: )   "of" (Set   ($#k5_lopban_1 :::"RealVectSpace"::: )   "(" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "X"))) "," (Set (Var "Y")) ")" ))) ; 
 registrationlet "X", "Y" be   ($#l1_rlvect_1 :::"RealLinearSpace":::); 
cluster (Set   ($#g1_rlvect_1 :::"RLSStruct"::: )  "(#"  (Set  "("  ($#k7_lopban_1 :::"LinearOperators"::: )   "(" "X" "," "Y" ")"  ")" ) "," (Set  "("  ($#k10_rsspace :::"Zero_"::: )   "(" (Set  "("  ($#k7_lopban_1 :::"LinearOperators"::: )   "(" "X" "," "Y" ")"  ")" ) "," (Set  "("  ($#k5_lopban_1 :::"RealVectSpace"::: )   "(" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "X") "," "Y" ")"  ")" ) ")"  ")" ) "," (Set  "("  ($#k8_rsspace :::"Add_"::: )   "(" (Set  "("  ($#k7_lopban_1 :::"LinearOperators"::: )   "(" "X" "," "Y" ")"  ")" ) "," (Set  "("  ($#k5_lopban_1 :::"RealVectSpace"::: )   "(" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "X") "," "Y" ")"  ")" ) ")"  ")" ) "," (Set  "("  ($#k9_rsspace :::"Mult_"::: )   "(" (Set  "("  ($#k7_lopban_1 :::"LinearOperators"::: )   "(" "X" "," "Y" ")"  ")" ) "," (Set  "("  ($#k5_lopban_1 :::"RealVectSpace"::: )   "(" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "X") "," "Y" ")"  ")" ) ")"  ")" ) "#)" ) ->   ($#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"::: )   ; 
end; definitionlet "X", "Y" be   ($#l1_rlvect_1 :::"RealLinearSpace":::); func  :::"R_VectorSpace_of_LinearOperators":::  "(" "X" "," "Y" ")"  ->   ($#l1_rlvect_1 :::"RealLinearSpace":::) equals :: LOPBAN_1:def 7 (Set   ($#g1_rlvect_1 :::"RLSStruct"::: )  "(#"  (Set  "("  ($#k7_lopban_1 :::"LinearOperators"::: )   "(" "X" "," "Y" ")"  ")" ) "," (Set  "("  ($#k10_rsspace :::"Zero_"::: )   "(" (Set  "("  ($#k7_lopban_1 :::"LinearOperators"::: )   "(" "X" "," "Y" ")"  ")" ) "," (Set  "("  ($#k5_lopban_1 :::"RealVectSpace"::: )   "(" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "X") "," "Y" ")"  ")" ) ")"  ")" ) "," (Set  "("  ($#k8_rsspace :::"Add_"::: )   "(" (Set  "("  ($#k7_lopban_1 :::"LinearOperators"::: )   "(" "X" "," "Y" ")"  ")" ) "," (Set  "("  ($#k5_lopban_1 :::"RealVectSpace"::: )   "(" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "X") "," "Y" ")"  ")" ) ")"  ")" ) "," (Set  "("  ($#k9_rsspace :::"Mult_"::: )   "(" (Set  "("  ($#k7_lopban_1 :::"LinearOperators"::: )   "(" "X" "," "Y" ")"  ")" ) "," (Set  "("  ($#k5_lopban_1 :::"RealVectSpace"::: )   "(" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "X") "," "Y" ")"  ")" ) ")"  ")" ) "#)" ); end; 






:: deftheorem    defines :::"R_VectorSpace_of_LinearOperators"::: LOPBAN_1:def 7 :  (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "being"   ($#l1_rlvect_1 :::"RealLinearSpace":::) "holds"  (Bool (Set   ($#k8_lopban_1 :::"R_VectorSpace_of_LinearOperators"::: )   "(" (Set (Var "X")) "," (Set (Var "Y")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#g1_rlvect_1 :::"RLSStruct"::: )  "(#"  (Set  "("  ($#k7_lopban_1 :::"LinearOperators"::: )   "(" (Set (Var "X")) "," (Set (Var "Y")) ")"  ")" ) "," (Set  "("  ($#k10_rsspace :::"Zero_"::: )   "(" (Set  "("  ($#k7_lopban_1 :::"LinearOperators"::: )   "(" (Set (Var "X")) "," (Set (Var "Y")) ")"  ")" ) "," (Set  "("  ($#k5_lopban_1 :::"RealVectSpace"::: )   "(" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "X"))) "," (Set (Var "Y")) ")"  ")" ) ")"  ")" ) "," (Set  "("  ($#k8_rsspace :::"Add_"::: )   "(" (Set  "("  ($#k7_lopban_1 :::"LinearOperators"::: )   "(" (Set (Var "X")) "," (Set (Var "Y")) ")"  ")" ) "," (Set  "("  ($#k5_lopban_1 :::"RealVectSpace"::: )   "(" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "X"))) "," (Set (Var "Y")) ")"  ")" ) ")"  ")" ) "," (Set  "("  ($#k9_rsspace :::"Mult_"::: )   "(" (Set  "("  ($#k7_lopban_1 :::"LinearOperators"::: )   "(" (Set (Var "X")) "," (Set (Var "Y")) ")"  ")" ) "," (Set  "("  ($#k5_lopban_1 :::"RealVectSpace"::: )   "(" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "X"))) "," (Set (Var "Y")) ")"  ")" ) ")"  ")" ) "#)" ))); 
 registrationlet "X", "Y" be   ($#l1_rlvect_1 :::"RealLinearSpace":::); 
cluster (Set   ($#k8_lopban_1 :::"R_VectorSpace_of_LinearOperators"::: )   "(" "X" "," "Y" ")" ) ->   ($#v1_rlvect_1 :::"strict"::: )   ; 
end; registrationlet "X", "Y" be   ($#l1_rlvect_1 :::"RealLinearSpace":::); 
cluster (Set   ($#k8_lopban_1 :::"R_VectorSpace_of_LinearOperators"::: )   "(" "X" "," "Y" ")" ) ->   ($#v1_monoid_0 :::"constituted-Functions"::: )   ; 
end; definitionlet "X", "Y" be   ($#l1_rlvect_1 :::"RealLinearSpace":::); let "f" be   ($#m1_subset_1 :::"Element":::) "of" (Set  "("  ($#k8_lopban_1 :::"R_VectorSpace_of_LinearOperators"::: )   "(" (Set (Const "X")) "," (Set (Const "Y")) ")"  ")" ); let "v" be   ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Const "X")); :: original: :::"."::: redefine func "f" :::"."::: "v" ->   ($#m1_subset_1 :::"VECTOR":::) "of" "Y"; end; 
theorem :: LOPBAN_1:16 (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "being"   ($#l1_rlvect_1 :::"RealLinearSpace":::)  (Bool  "for" (Set (Var "f")) "," (Set (Var "g")) "," (Set (Var "h")) "being"   ($#m1_subset_1 :::"VECTOR":::) "of" (Set  "("  ($#k8_lopban_1 :::"R_VectorSpace_of_LinearOperators"::: )   "(" (Set (Var "X")) "," (Set (Var "Y")) ")"  ")" ) "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 :::"VECTOR":::) "of" (Set (Var "X")) "holds"  (Bool (Set (Set (Var "h"))  ($#k9_lopban_1 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "f"))  ($#k9_lopban_1 :::"."::: )  (Set (Var "x")) ")" )  ($#k3_rlvect_1 :::"+"::: )  (Set  "(" (Set (Var "g"))  ($#k9_lopban_1 :::"."::: )  (Set (Var "x")) ")" ))))  ")" ))) ; 
 
theorem :: LOPBAN_1:17 (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "being"   ($#l1_rlvect_1 :::"RealLinearSpace":::)  (Bool  "for" (Set (Var "f")) "," (Set (Var "h")) "being"   ($#m1_subset_1 :::"VECTOR":::) "of" (Set  "("  ($#k8_lopban_1 :::"R_VectorSpace_of_LinearOperators"::: )   "(" (Set (Var "X")) "," (Set (Var "Y")) ")"  ")" )  (Bool  "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Real":::) "holds"   (Bool  "("  (Bool (Set (Var "h"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "a"))  ($#k1_rlvect_1 :::"*"::: )  (Set (Var "f")))) "iff" (Bool  "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "X")) "holds"  (Bool (Set (Set (Var "h"))  ($#k9_lopban_1 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "a"))  ($#k1_rlvect_1 :::"*"::: )  (Set  "(" (Set (Var "f"))  ($#k9_lopban_1 :::"."::: )  (Set (Var "x")) ")" ))))  ")" )))) ; 
 
theorem :: LOPBAN_1:18 (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "being"   ($#l1_rlvect_1 :::"RealLinearSpace":::) "holds"  (Bool (Set   ($#k4_struct_0 :::"0."::: )  (Set  "("  ($#k8_lopban_1 :::"R_VectorSpace_of_LinearOperators"::: )   "(" (Set (Var "X")) "," (Set (Var "Y")) ")"  ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "X")))  ($#k8_funcop_1 :::"-->"::: )  (Set  "("  ($#k4_struct_0 :::"0."::: )  (Set (Var "Y")) ")" )))) ; 
 
theorem :: LOPBAN_1:19 (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "being"   ($#l1_rlvect_1 :::"RealLinearSpace":::) "holds"  (Bool (Set (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "X")))  ($#k8_funcop_1 :::"-->"::: )  (Set  "("  ($#k4_struct_0 :::"0."::: )  (Set (Var "Y")) ")" )) "is"   ($#m1_subset_1 :::"LinearOperator":::) "of" (Set (Var "X")) "," (Set (Var "Y")))) ; 
 begin  
theorem :: LOPBAN_1:20 (Bool  "for" (Set (Var "X")) "being"   ($#l1_normsp_1 :::"RealNormSpace":::)  (Bool  "for" (Set (Var "seq")) "being"   ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X"))  (Bool  "for" (Set (Var "g")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X"))  "st" (Bool (Bool (Set (Var "seq")) "is"   ($#v3_normsp_1 :::"convergent"::: )  ) & (Bool (Set   ($#k6_normsp_1 :::"lim"::: )  (Set (Var "seq")))  ($#r1_hidden :::"="::: )  (Set (Var "g")))) "holds"  (Bool  "("  (Bool (Set  ($#k4_normsp_0 :::"||."::: ) (Set (Var "seq")) ($#k4_normsp_0 :::".||"::: ) ) "is"   ($#v2_comseq_2 :::"convergent"::: )  ) & (Bool (Set   ($#k2_seq_2 :::"lim"::: )  (Set  ($#k4_normsp_0 :::"||."::: ) (Set (Var "seq")) ($#k4_normsp_0 :::".||"::: ) ))  ($#r1_hidden :::"="::: )  (Set  ($#k1_normsp_0 :::"||."::: ) (Set (Var "g")) ($#k1_normsp_0 :::".||"::: ) ))  ")" )))) ; 
 definitionlet "X", "Y" be   ($#l1_normsp_1 :::"RealNormSpace":::); let "IT" be   ($#m1_subset_1 :::"LinearOperator":::) "of" (Set (Const "X")) "," (Set (Const "Y")); attr "IT" is  :::"Lipschitzian":::  means :: LOPBAN_1:def 8 (Bool  "ex" (Set (Var "K")) "being"   ($#m1_subset_1 :::"Real":::) "st"  (Bool  "("  (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "K"))) & (Bool  "("   "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"VECTOR":::) "of" "X" "holds"  (Bool (Set  ($#k1_normsp_0 :::"||."::: ) (Set  "(" "IT"  ($#k3_funct_2 :::"."::: )  (Set (Var "x")) ")" ) ($#k1_normsp_0 :::".||"::: ) )  ($#r1_xxreal_0 :::"<="::: )  (Set (Set (Var "K"))  ($#k8_real_1 :::"*"::: )  (Set  ($#k1_normsp_0 :::"||."::: ) (Set (Var "x")) ($#k1_normsp_0 :::".||"::: ) )))  ")" )  ")" )); end; 






:: deftheorem    defines :::"Lipschitzian"::: LOPBAN_1:def 8 :  (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "being"   ($#l1_normsp_1 :::"RealNormSpace":::)  (Bool  "for" (Set (Var "IT")) "being"   ($#m1_subset_1 :::"LinearOperator":::) "of" (Set (Var "X")) "," (Set (Var "Y")) "holds"   (Bool  "("  (Bool (Set (Var "IT")) "is"   ($#v2_lopban_1 :::"Lipschitzian"::: )  ) "iff" (Bool  "ex" (Set (Var "K")) "being"   ($#m1_subset_1 :::"Real":::) "st"  (Bool  "("  (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "K"))) & (Bool  "("   "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "X")) "holds"  (Bool (Set  ($#k1_normsp_0 :::"||."::: ) (Set  "(" (Set (Var "IT"))  ($#k3_funct_2 :::"."::: )  (Set (Var "x")) ")" ) ($#k1_normsp_0 :::".||"::: ) )  ($#r1_xxreal_0 :::"<="::: )  (Set (Set (Var "K"))  ($#k8_real_1 :::"*"::: )  (Set  ($#k1_normsp_0 :::"||."::: ) (Set (Var "x")) ($#k1_normsp_0 :::".||"::: ) )))  ")" )  ")" ))  ")" ))); 
 
theorem :: LOPBAN_1:21 (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "being"   ($#l1_normsp_1 :::"RealNormSpace":::)  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"LinearOperator":::) "of" (Set (Var "X")) "," (Set (Var "Y"))  "st" (Bool (Bool  "("   "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "X")) "holds"  (Bool (Set (Set (Var "f"))  ($#k3_funct_2 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set   ($#k4_struct_0 :::"0."::: )  (Set (Var "Y"))))  ")" )) "holds"  (Bool (Set (Var "f")) "is"   ($#v2_lopban_1 :::"Lipschitzian"::: )  ))) ; 
 registrationlet "X", "Y" be   ($#l1_normsp_1 :::"RealNormSpace":::); 
cluster  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v1_relat_1 :::"Relation-like"::: )   (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "X")  ($#v4_relat_1 :::"-defined"::: )   (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "Y")  ($#v5_relat_1 :::"-valued"::: )     ($#v1_funct_1 :::"Function-like"::: )     ($#v1_partfun1 :::"total"::: )     ($#v1_funct_2 :::"quasi_total"::: )     ($#v13_vectsp_1 :::"additive"::: )     ($#v1_lopban_1 :::"homogeneous"::: )     ($#v2_lopban_1 :::"Lipschitzian"::: )    for    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k1_zfmisc_1 :::"bool"::: )  (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "X") "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "Y") ($#k2_zfmisc_1 :::":]"::: ) )); 
end; definitionlet "X", "Y" be   ($#l1_normsp_1 :::"RealNormSpace":::); func  :::"BoundedLinearOperators":::  "(" "X" "," "Y" ")"  ->   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k8_lopban_1 :::"R_VectorSpace_of_LinearOperators"::: )   "(" "X" "," "Y" ")"  ")" ) means :: LOPBAN_1:def 9 (Bool  "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  it) "iff" (Bool (Set (Var "x")) "is"   ($#v2_lopban_1 :::"Lipschitzian"::: )    ($#m1_subset_1 :::"LinearOperator":::) "of" "X" "," "Y")  ")" )); end; 






:: deftheorem    defines :::"BoundedLinearOperators"::: LOPBAN_1:def 9 :  (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "being"   ($#l1_normsp_1 :::"RealNormSpace":::)  (Bool  "for" (Set (Var "b3")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k8_lopban_1 :::"R_VectorSpace_of_LinearOperators"::: )   "(" (Set (Var "X")) "," (Set (Var "Y")) ")"  ")" ) "holds"   (Bool  "("  (Bool (Set (Var "b3"))  ($#r1_hidden :::"="::: )  (Set   ($#k10_lopban_1 :::"BoundedLinearOperators"::: )   "(" (Set (Var "X")) "," (Set (Var "Y")) ")" )) "iff" (Bool  "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "b3"))) "iff" (Bool (Set (Var "x")) "is"   ($#v2_lopban_1 :::"Lipschitzian"::: )    ($#m1_subset_1 :::"LinearOperator":::) "of" (Set (Var "X")) "," (Set (Var "Y")))  ")" ))  ")" ))); 
 registrationlet "X", "Y" be   ($#l1_normsp_1 :::"RealNormSpace":::); 
cluster (Set   ($#k10_lopban_1 :::"BoundedLinearOperators"::: )   "(" "X" "," "Y" ")" ) ->  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )  ; 
end; 
theorem :: LOPBAN_1:22 (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "being"   ($#l1_normsp_1 :::"RealNormSpace":::) "holds"  (Bool (Set   ($#k10_lopban_1 :::"BoundedLinearOperators"::: )   "(" (Set (Var "X")) "," (Set (Var "Y")) ")" ) "is"   ($#v1_rlsub_1 :::"linearly-closed"::: )  )) ; 
 
theorem :: LOPBAN_1:23 (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "being"   ($#l1_normsp_1 :::"RealNormSpace":::) "holds"  (Bool (Set   ($#g1_rlvect_1 :::"RLSStruct"::: )  "(#"  (Set  "("  ($#k10_lopban_1 :::"BoundedLinearOperators"::: )   "(" (Set (Var "X")) "," (Set (Var "Y")) ")"  ")" ) "," (Set  "("  ($#k10_rsspace :::"Zero_"::: )   "(" (Set  "("  ($#k10_lopban_1 :::"BoundedLinearOperators"::: )   "(" (Set (Var "X")) "," (Set (Var "Y")) ")"  ")" ) "," (Set  "("  ($#k8_lopban_1 :::"R_VectorSpace_of_LinearOperators"::: )   "(" (Set (Var "X")) "," (Set (Var "Y")) ")"  ")" ) ")"  ")" ) "," (Set  "("  ($#k8_rsspace :::"Add_"::: )   "(" (Set  "("  ($#k10_lopban_1 :::"BoundedLinearOperators"::: )   "(" (Set (Var "X")) "," (Set (Var "Y")) ")"  ")" ) "," (Set  "("  ($#k8_lopban_1 :::"R_VectorSpace_of_LinearOperators"::: )   "(" (Set (Var "X")) "," (Set (Var "Y")) ")"  ")" ) ")"  ")" ) "," (Set  "("  ($#k9_rsspace :::"Mult_"::: )   "(" (Set  "("  ($#k10_lopban_1 :::"BoundedLinearOperators"::: )   "(" (Set (Var "X")) "," (Set (Var "Y")) ")"  ")" ) "," (Set  "("  ($#k8_lopban_1 :::"R_VectorSpace_of_LinearOperators"::: )   "(" (Set (Var "X")) "," (Set (Var "Y")) ")"  ")" ) ")"  ")" ) "#)" ) "is"    ($#m1_rlsub_1 :::"Subspace"::: )   "of" (Set   ($#k8_lopban_1 :::"R_VectorSpace_of_LinearOperators"::: )   "(" (Set (Var "X")) "," (Set (Var "Y")) ")" ))) ; 
 registrationlet "X", "Y" be   ($#l1_normsp_1 :::"RealNormSpace":::); 
cluster (Set   ($#g1_rlvect_1 :::"RLSStruct"::: )  "(#"  (Set  "("  ($#k10_lopban_1 :::"BoundedLinearOperators"::: )   "(" "X" "," "Y" ")"  ")" ) "," (Set  "("  ($#k10_rsspace :::"Zero_"::: )   "(" (Set  "("  ($#k10_lopban_1 :::"BoundedLinearOperators"::: )   "(" "X" "," "Y" ")"  ")" ) "," (Set  "("  ($#k8_lopban_1 :::"R_VectorSpace_of_LinearOperators"::: )   "(" "X" "," "Y" ")"  ")" ) ")"  ")" ) "," (Set  "("  ($#k8_rsspace :::"Add_"::: )   "(" (Set  "("  ($#k10_lopban_1 :::"BoundedLinearOperators"::: )   "(" "X" "," "Y" ")"  ")" ) "," (Set  "("  ($#k8_lopban_1 :::"R_VectorSpace_of_LinearOperators"::: )   "(" "X" "," "Y" ")"  ")" ) ")"  ")" ) "," (Set  "("  ($#k9_rsspace :::"Mult_"::: )   "(" (Set  "("  ($#k10_lopban_1 :::"BoundedLinearOperators"::: )   "(" "X" "," "Y" ")"  ")" ) "," (Set  "("  ($#k8_lopban_1 :::"R_VectorSpace_of_LinearOperators"::: )   "(" "X" "," "Y" ")"  ")" ) ")"  ")" ) "#)" ) ->   ($#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"::: )   ; 
end; definitionlet "X", "Y" be   ($#l1_normsp_1 :::"RealNormSpace":::); func  :::"R_VectorSpace_of_BoundedLinearOperators":::  "(" "X" "," "Y" ")"  ->   ($#l1_rlvect_1 :::"RealLinearSpace":::) equals :: LOPBAN_1:def 10 (Set   ($#g1_rlvect_1 :::"RLSStruct"::: )  "(#"  (Set  "("  ($#k10_lopban_1 :::"BoundedLinearOperators"::: )   "(" "X" "," "Y" ")"  ")" ) "," (Set  "("  ($#k10_rsspace :::"Zero_"::: )   "(" (Set  "("  ($#k10_lopban_1 :::"BoundedLinearOperators"::: )   "(" "X" "," "Y" ")"  ")" ) "," (Set  "("  ($#k8_lopban_1 :::"R_VectorSpace_of_LinearOperators"::: )   "(" "X" "," "Y" ")"  ")" ) ")"  ")" ) "," (Set  "("  ($#k8_rsspace :::"Add_"::: )   "(" (Set  "("  ($#k10_lopban_1 :::"BoundedLinearOperators"::: )   "(" "X" "," "Y" ")"  ")" ) "," (Set  "("  ($#k8_lopban_1 :::"R_VectorSpace_of_LinearOperators"::: )   "(" "X" "," "Y" ")"  ")" ) ")"  ")" ) "," (Set  "("  ($#k9_rsspace :::"Mult_"::: )   "(" (Set  "("  ($#k10_lopban_1 :::"BoundedLinearOperators"::: )   "(" "X" "," "Y" ")"  ")" ) "," (Set  "("  ($#k8_lopban_1 :::"R_VectorSpace_of_LinearOperators"::: )   "(" "X" "," "Y" ")"  ")" ) ")"  ")" ) "#)" ); end; 






:: deftheorem    defines :::"R_VectorSpace_of_BoundedLinearOperators"::: LOPBAN_1:def 10 :  (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "being"   ($#l1_normsp_1 :::"RealNormSpace":::) "holds"  (Bool (Set   ($#k11_lopban_1 :::"R_VectorSpace_of_BoundedLinearOperators"::: )   "(" (Set (Var "X")) "," (Set (Var "Y")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#g1_rlvect_1 :::"RLSStruct"::: )  "(#"  (Set  "("  ($#k10_lopban_1 :::"BoundedLinearOperators"::: )   "(" (Set (Var "X")) "," (Set (Var "Y")) ")"  ")" ) "," (Set  "("  ($#k10_rsspace :::"Zero_"::: )   "(" (Set  "("  ($#k10_lopban_1 :::"BoundedLinearOperators"::: )   "(" (Set (Var "X")) "," (Set (Var "Y")) ")"  ")" ) "," (Set  "("  ($#k8_lopban_1 :::"R_VectorSpace_of_LinearOperators"::: )   "(" (Set (Var "X")) "," (Set (Var "Y")) ")"  ")" ) ")"  ")" ) "," (Set  "("  ($#k8_rsspace :::"Add_"::: )   "(" (Set  "("  ($#k10_lopban_1 :::"BoundedLinearOperators"::: )   "(" (Set (Var "X")) "," (Set (Var "Y")) ")"  ")" ) "," (Set  "("  ($#k8_lopban_1 :::"R_VectorSpace_of_LinearOperators"::: )   "(" (Set (Var "X")) "," (Set (Var "Y")) ")"  ")" ) ")"  ")" ) "," (Set  "("  ($#k9_rsspace :::"Mult_"::: )   "(" (Set  "("  ($#k10_lopban_1 :::"BoundedLinearOperators"::: )   "(" (Set (Var "X")) "," (Set (Var "Y")) ")"  ")" ) "," (Set  "("  ($#k8_lopban_1 :::"R_VectorSpace_of_LinearOperators"::: )   "(" (Set (Var "X")) "," (Set (Var "Y")) ")"  ")" ) ")"  ")" ) "#)" ))); 
 registrationlet "X", "Y" be   ($#l1_normsp_1 :::"RealNormSpace":::); 
cluster (Set   ($#k11_lopban_1 :::"R_VectorSpace_of_BoundedLinearOperators"::: )   "(" "X" "," "Y" ")" ) ->   ($#v1_rlvect_1 :::"strict"::: )   ; 
end; registrationlet "X", "Y" be   ($#l1_normsp_1 :::"RealNormSpace":::); 
cluster   ->   ($#v1_relat_1 :::"Relation-like"::: )     ($#v1_funct_1 :::"Function-like"::: )    for    ($#m1_subset_1 :::"Element"::: )   "of" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set  "("  ($#k11_lopban_1 :::"R_VectorSpace_of_BoundedLinearOperators"::: )   "(" "X" "," "Y" ")"  ")" )); 
end; definitionlet "X", "Y" be   ($#l1_normsp_1 :::"RealNormSpace":::); let "f" be   ($#m1_subset_1 :::"Element":::) "of" (Set  "("  ($#k11_lopban_1 :::"R_VectorSpace_of_BoundedLinearOperators"::: )   "(" (Set (Const "X")) "," (Set (Const "Y")) ")"  ")" ); let "v" be   ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Const "X")); :: original: :::"."::: redefine func "f" :::"."::: "v" ->   ($#m1_subset_1 :::"VECTOR":::) "of" "Y"; end; 
theorem :: LOPBAN_1:24 (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "being"   ($#l1_normsp_1 :::"RealNormSpace":::)  (Bool  "for" (Set (Var "f")) "," (Set (Var "g")) "," (Set (Var "h")) "being"   ($#m1_subset_1 :::"VECTOR":::) "of" (Set  "("  ($#k11_lopban_1 :::"R_VectorSpace_of_BoundedLinearOperators"::: )   "(" (Set (Var "X")) "," (Set (Var "Y")) ")"  ")" ) "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 :::"VECTOR":::) "of" (Set (Var "X")) "holds"  (Bool (Set (Set (Var "h"))  ($#k12_lopban_1 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "f"))  ($#k12_lopban_1 :::"."::: )  (Set (Var "x")) ")" )  ($#k3_rlvect_1 :::"+"::: )  (Set  "(" (Set (Var "g"))  ($#k12_lopban_1 :::"."::: )  (Set (Var "x")) ")" ))))  ")" ))) ; 
 
theorem :: LOPBAN_1:25 (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "being"   ($#l1_normsp_1 :::"RealNormSpace":::)  (Bool  "for" (Set (Var "f")) "," (Set (Var "h")) "being"   ($#m1_subset_1 :::"VECTOR":::) "of" (Set  "("  ($#k11_lopban_1 :::"R_VectorSpace_of_BoundedLinearOperators"::: )   "(" (Set (Var "X")) "," (Set (Var "Y")) ")"  ")" )  (Bool  "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Real":::) "holds"   (Bool  "("  (Bool (Set (Var "h"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "a"))  ($#k1_rlvect_1 :::"*"::: )  (Set (Var "f")))) "iff" (Bool  "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "X")) "holds"  (Bool (Set (Set (Var "h"))  ($#k12_lopban_1 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "a"))  ($#k1_rlvect_1 :::"*"::: )  (Set  "(" (Set (Var "f"))  ($#k12_lopban_1 :::"."::: )  (Set (Var "x")) ")" ))))  ")" )))) ; 
 
theorem :: LOPBAN_1:26 (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "being"   ($#l1_normsp_1 :::"RealNormSpace":::) "holds"  (Bool (Set   ($#k4_struct_0 :::"0."::: )  (Set  "("  ($#k11_lopban_1 :::"R_VectorSpace_of_BoundedLinearOperators"::: )   "(" (Set (Var "X")) "," (Set (Var "Y")) ")"  ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "X")))  ($#k8_funcop_1 :::"-->"::: )  (Set  "("  ($#k4_struct_0 :::"0."::: )  (Set (Var "Y")) ")" )))) ; 
 definitionlet "X", "Y" be   ($#l1_normsp_1 :::"RealNormSpace":::); let "f" be    ($#m1_hidden :::"set"::: )  ; assume 
(Bool (Set (Const "f"))  ($#r2_hidden :::"in"::: )  (Set   ($#k10_lopban_1 :::"BoundedLinearOperators"::: )   "(" (Set (Const "X")) "," (Set (Const "Y")) ")" ))
 ; func  :::"modetrans":::  "(" "f" "," "X" "," "Y" ")"  ->   ($#v2_lopban_1 :::"Lipschitzian"::: )    ($#m1_subset_1 :::"LinearOperator":::) "of" "X" "," "Y" equals :: LOPBAN_1:def 11 "f"; end; 








:: deftheorem    defines :::"modetrans"::: LOPBAN_1:def 11 :  (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "being"   ($#l1_normsp_1 :::"RealNormSpace":::)  (Bool  "for" (Set (Var "f")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "f"))  ($#r2_hidden :::"in"::: )  (Set   ($#k10_lopban_1 :::"BoundedLinearOperators"::: )   "(" (Set (Var "X")) "," (Set (Var "Y")) ")" ))) "holds"  (Bool (Set   ($#k13_lopban_1 :::"modetrans"::: )   "(" (Set (Var "f")) "," (Set (Var "X")) "," (Set (Var "Y")) ")" )  ($#r1_hidden :::"="::: )  (Set (Var "f"))))); 
 definitionlet "X", "Y" be   ($#l1_normsp_1 :::"RealNormSpace":::); let "u" be   ($#m1_subset_1 :::"LinearOperator":::) "of" (Set (Const "X")) "," (Set (Const "Y")); func  :::"PreNorms"::: "u" ->  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )   ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) ) equals :: LOPBAN_1:def 12  "{"  (Set  ($#k1_normsp_0 :::"||."::: ) (Set  "(" "u"  ($#k3_funct_2 :::"."::: )  (Set (Var "t")) ")" ) ($#k1_normsp_0 :::".||"::: ) ) where t "is"   ($#m1_subset_1 :::"VECTOR":::) "of" "X" : (Bool (Set  ($#k1_normsp_0 :::"||."::: ) (Set (Var "t")) ($#k1_normsp_0 :::".||"::: ) )  ($#r1_xxreal_0 :::"<="::: )  (Num 1))  "}"  ; end; 







:: deftheorem    defines :::"PreNorms"::: LOPBAN_1:def 12 :  (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "being"   ($#l1_normsp_1 :::"RealNormSpace":::)  (Bool  "for" (Set (Var "u")) "being"   ($#m1_subset_1 :::"LinearOperator":::) "of" (Set (Var "X")) "," (Set (Var "Y")) "holds"  (Bool (Set   ($#k14_lopban_1 :::"PreNorms"::: )  (Set (Var "u")))  ($#r1_hidden :::"="::: )   "{"  (Set  ($#k1_normsp_0 :::"||."::: ) (Set  "(" (Set (Var "u"))  ($#k3_funct_2 :::"."::: )  (Set (Var "t")) ")" ) ($#k1_normsp_0 :::".||"::: ) ) where t "is"   ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "X")) : (Bool (Set  ($#k1_normsp_0 :::"||."::: ) (Set (Var "t")) ($#k1_normsp_0 :::".||"::: ) )  ($#r1_xxreal_0 :::"<="::: )  (Num 1))  "}"  ))); 
 
theorem :: LOPBAN_1:27 (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "being"   ($#l1_normsp_1 :::"RealNormSpace":::)  (Bool  "for" (Set (Var "g")) "being"   ($#v2_lopban_1 :::"Lipschitzian"::: )    ($#m1_subset_1 :::"LinearOperator":::) "of" (Set (Var "X")) "," (Set (Var "Y")) "holds"  (Bool (Set   ($#k14_lopban_1 :::"PreNorms"::: )  (Set (Var "g"))) "is"   ($#v4_xxreal_2 :::"bounded_above"::: )  ))) ; 
 
theorem :: LOPBAN_1:28 (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "being"   ($#l1_normsp_1 :::"RealNormSpace":::)  (Bool  "for" (Set (Var "g")) "being"   ($#m1_subset_1 :::"LinearOperator":::) "of" (Set (Var "X")) "," (Set (Var "Y")) "holds"   (Bool  "("  (Bool (Set (Var "g")) "is"   ($#v2_lopban_1 :::"Lipschitzian"::: )  ) "iff" (Bool (Set   ($#k14_lopban_1 :::"PreNorms"::: )  (Set (Var "g"))) "is"   ($#v4_xxreal_2 :::"bounded_above"::: )  )  ")" ))) ; 
 definitionlet "X", "Y" be   ($#l1_normsp_1 :::"RealNormSpace":::); func  :::"BoundedLinearOperatorsNorm":::  "(" "X" "," "Y" ")"  ->   ($#m1_subset_1 :::"Function":::) "of" (Set  "("  ($#k10_lopban_1 :::"BoundedLinearOperators"::: )   "(" "X" "," "Y" ")"  ")" ) "," (Set  ($#k1_numbers :::"REAL"::: ) ) means :: LOPBAN_1:def 13 (Bool  "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set   ($#k10_lopban_1 :::"BoundedLinearOperators"::: )   "(" "X" "," "Y" ")" ))) "holds"  (Bool (Set it  ($#k1_seq_1 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set   ($#k4_seq_4 :::"upper_bound"::: )  (Set  "("  ($#k14_lopban_1 :::"PreNorms"::: )  (Set  "("  ($#k13_lopban_1 :::"modetrans"::: )   "(" (Set (Var "x")) "," "X" "," "Y" ")"  ")" ) ")" )))); end; 






:: deftheorem    defines :::"BoundedLinearOperatorsNorm"::: LOPBAN_1:def 13 :  (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "being"   ($#l1_normsp_1 :::"RealNormSpace":::)  (Bool  "for" (Set (Var "b3")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  "("  ($#k10_lopban_1 :::"BoundedLinearOperators"::: )   "(" (Set (Var "X")) "," (Set (Var "Y")) ")"  ")" ) "," (Set  ($#k1_numbers :::"REAL"::: ) ) "holds"   (Bool  "("  (Bool (Set (Var "b3"))  ($#r1_hidden :::"="::: )  (Set   ($#k15_lopban_1 :::"BoundedLinearOperatorsNorm"::: )   "(" (Set (Var "X")) "," (Set (Var "Y")) ")" )) "iff" (Bool  "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set   ($#k10_lopban_1 :::"BoundedLinearOperators"::: )   "(" (Set (Var "X")) "," (Set (Var "Y")) ")" ))) "holds"  (Bool (Set (Set (Var "b3"))  ($#k1_seq_1 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set   ($#k4_seq_4 :::"upper_bound"::: )  (Set  "("  ($#k14_lopban_1 :::"PreNorms"::: )  (Set  "("  ($#k13_lopban_1 :::"modetrans"::: )   "(" (Set (Var "x")) "," (Set (Var "X")) "," (Set (Var "Y")) ")"  ")" ) ")" ))))  ")" ))); 
 
theorem :: LOPBAN_1:29 (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "being"   ($#l1_normsp_1 :::"RealNormSpace":::)  (Bool  "for" (Set (Var "f")) "being"   ($#v2_lopban_1 :::"Lipschitzian"::: )    ($#m1_subset_1 :::"LinearOperator":::) "of" (Set (Var "X")) "," (Set (Var "Y")) "holds"  (Bool (Set   ($#k13_lopban_1 :::"modetrans"::: )   "(" (Set (Var "f")) "," (Set (Var "X")) "," (Set (Var "Y")) ")" )  ($#r2_funct_2 :::"="::: )  (Set (Var "f"))))) ; 
 
theorem :: LOPBAN_1:30 (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "being"   ($#l1_normsp_1 :::"RealNormSpace":::)  (Bool  "for" (Set (Var "f")) "being"   ($#v2_lopban_1 :::"Lipschitzian"::: )    ($#m1_subset_1 :::"LinearOperator":::) "of" (Set (Var "X")) "," (Set (Var "Y")) "holds"  (Bool (Set (Set  "("  ($#k15_lopban_1 :::"BoundedLinearOperatorsNorm"::: )   "(" (Set (Var "X")) "," (Set (Var "Y")) ")"  ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "f")))  ($#r1_hidden :::"="::: )  (Set   ($#k4_seq_4 :::"upper_bound"::: )  (Set  "("  ($#k14_lopban_1 :::"PreNorms"::: )  (Set (Var "f")) ")" ))))) ; 
 definitionlet "X", "Y" be   ($#l1_normsp_1 :::"RealNormSpace":::); func  :::"R_NormSpace_of_BoundedLinearOperators":::  "(" "X" "," "Y" ")"  ->  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_normsp_1 :::"NORMSTR"::: )   equals :: LOPBAN_1:def 14 (Set   ($#g1_normsp_1 :::"NORMSTR"::: )  "(#"  (Set  "("  ($#k10_lopban_1 :::"BoundedLinearOperators"::: )   "(" "X" "," "Y" ")"  ")" ) "," (Set  "("  ($#k10_rsspace :::"Zero_"::: )   "(" (Set  "("  ($#k10_lopban_1 :::"BoundedLinearOperators"::: )   "(" "X" "," "Y" ")"  ")" ) "," (Set  "("  ($#k8_lopban_1 :::"R_VectorSpace_of_LinearOperators"::: )   "(" "X" "," "Y" ")"  ")" ) ")"  ")" ) "," (Set  "("  ($#k8_rsspace :::"Add_"::: )   "(" (Set  "("  ($#k10_lopban_1 :::"BoundedLinearOperators"::: )   "(" "X" "," "Y" ")"  ")" ) "," (Set  "("  ($#k8_lopban_1 :::"R_VectorSpace_of_LinearOperators"::: )   "(" "X" "," "Y" ")"  ")" ) ")"  ")" ) "," (Set  "("  ($#k9_rsspace :::"Mult_"::: )   "(" (Set  "("  ($#k10_lopban_1 :::"BoundedLinearOperators"::: )   "(" "X" "," "Y" ")"  ")" ) "," (Set  "("  ($#k8_lopban_1 :::"R_VectorSpace_of_LinearOperators"::: )   "(" "X" "," "Y" ")"  ")" ) ")"  ")" ) "," (Set  "("  ($#k15_lopban_1 :::"BoundedLinearOperatorsNorm"::: )   "(" "X" "," "Y" ")"  ")" ) "#)" ); end; 






:: deftheorem    defines :::"R_NormSpace_of_BoundedLinearOperators"::: LOPBAN_1:def 14 :  (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "being"   ($#l1_normsp_1 :::"RealNormSpace":::) "holds"  (Bool (Set   ($#k16_lopban_1 :::"R_NormSpace_of_BoundedLinearOperators"::: )   "(" (Set (Var "X")) "," (Set (Var "Y")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#g1_normsp_1 :::"NORMSTR"::: )  "(#"  (Set  "("  ($#k10_lopban_1 :::"BoundedLinearOperators"::: )   "(" (Set (Var "X")) "," (Set (Var "Y")) ")"  ")" ) "," (Set  "("  ($#k10_rsspace :::"Zero_"::: )   "(" (Set  "("  ($#k10_lopban_1 :::"BoundedLinearOperators"::: )   "(" (Set (Var "X")) "," (Set (Var "Y")) ")"  ")" ) "," (Set  "("  ($#k8_lopban_1 :::"R_VectorSpace_of_LinearOperators"::: )   "(" (Set (Var "X")) "," (Set (Var "Y")) ")"  ")" ) ")"  ")" ) "," (Set  "("  ($#k8_rsspace :::"Add_"::: )   "(" (Set  "("  ($#k10_lopban_1 :::"BoundedLinearOperators"::: )   "(" (Set (Var "X")) "," (Set (Var "Y")) ")"  ")" ) "," (Set  "("  ($#k8_lopban_1 :::"R_VectorSpace_of_LinearOperators"::: )   "(" (Set (Var "X")) "," (Set (Var "Y")) ")"  ")" ) ")"  ")" ) "," (Set  "("  ($#k9_rsspace :::"Mult_"::: )   "(" (Set  "("  ($#k10_lopban_1 :::"BoundedLinearOperators"::: )   "(" (Set (Var "X")) "," (Set (Var "Y")) ")"  ")" ) "," (Set  "("  ($#k8_lopban_1 :::"R_VectorSpace_of_LinearOperators"::: )   "(" (Set (Var "X")) "," (Set (Var "Y")) ")"  ")" ) ")"  ")" ) "," (Set  "("  ($#k15_lopban_1 :::"BoundedLinearOperatorsNorm"::: )   "(" (Set (Var "X")) "," (Set (Var "Y")) ")"  ")" ) "#)" ))); 
 
theorem :: LOPBAN_1:31 (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "being"   ($#l1_normsp_1 :::"RealNormSpace":::) "holds"  (Bool (Set (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "X")))  ($#k8_funcop_1 :::"-->"::: )  (Set  "("  ($#k4_struct_0 :::"0."::: )  (Set (Var "Y")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k4_struct_0 :::"0."::: )  (Set  "("  ($#k16_lopban_1 :::"R_NormSpace_of_BoundedLinearOperators"::: )   "(" (Set (Var "X")) "," (Set (Var "Y")) ")"  ")" )))) ; 
 
theorem :: LOPBAN_1:32 (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "being"   ($#l1_normsp_1 :::"RealNormSpace":::)  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k16_lopban_1 :::"R_NormSpace_of_BoundedLinearOperators"::: )   "(" (Set (Var "X")) "," (Set (Var "Y")) ")"  ")" )  (Bool  "for" (Set (Var "g")) "being"   ($#v2_lopban_1 :::"Lipschitzian"::: )    ($#m1_subset_1 :::"LinearOperator":::) "of" (Set (Var "X")) "," (Set (Var "Y"))  "st" (Bool (Bool (Set (Var "g"))  ($#r1_hidden :::"="::: )  (Set (Var "f")))) "holds"  (Bool  "for" (Set (Var "t")) "being"   ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "X")) "holds"  (Bool (Set  ($#k1_normsp_0 :::"||."::: ) (Set  "(" (Set (Var "g"))  ($#k3_funct_2 :::"."::: )  (Set (Var "t")) ")" ) ($#k1_normsp_0 :::".||"::: ) )  ($#r1_xxreal_0 :::"<="::: )  (Set (Set  ($#k1_normsp_0 :::"||."::: ) (Set (Var "f")) ($#k1_normsp_0 :::".||"::: ) )  ($#k8_real_1 :::"*"::: )  (Set  ($#k1_normsp_0 :::"||."::: ) (Set (Var "t")) ($#k1_normsp_0 :::".||"::: ) ))))))) ; 
 
theorem :: LOPBAN_1:33 (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "being"   ($#l1_normsp_1 :::"RealNormSpace":::)  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k16_lopban_1 :::"R_NormSpace_of_BoundedLinearOperators"::: )   "(" (Set (Var "X")) "," (Set (Var "Y")) ")"  ")" ) "holds"  (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<="::: )  (Set  ($#k1_normsp_0 :::"||."::: ) (Set (Var "f")) ($#k1_normsp_0 :::".||"::: ) )))) ; 
 
theorem :: LOPBAN_1:34 (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "being"   ($#l1_normsp_1 :::"RealNormSpace":::)  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k16_lopban_1 :::"R_NormSpace_of_BoundedLinearOperators"::: )   "(" (Set (Var "X")) "," (Set (Var "Y")) ")"  ")" )  "st" (Bool (Bool (Set (Var "f"))  ($#r1_hidden :::"="::: )  (Set   ($#k4_struct_0 :::"0."::: )  (Set  "("  ($#k16_lopban_1 :::"R_NormSpace_of_BoundedLinearOperators"::: )   "(" (Set (Var "X")) "," (Set (Var "Y")) ")"  ")" )))) "holds"  (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_hidden :::"="::: )  (Set  ($#k1_normsp_0 :::"||."::: ) (Set (Var "f")) ($#k1_normsp_0 :::".||"::: ) )))) ; 
 registrationlet "X", "Y" be   ($#l1_normsp_1 :::"RealNormSpace":::); 
cluster   ->   ($#v1_relat_1 :::"Relation-like"::: )     ($#v1_funct_1 :::"Function-like"::: )    for    ($#m1_subset_1 :::"Element"::: )   "of" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set  "("  ($#k16_lopban_1 :::"R_NormSpace_of_BoundedLinearOperators"::: )   "(" "X" "," "Y" ")"  ")" )); 
end; definitionlet "X", "Y" be   ($#l1_normsp_1 :::"RealNormSpace":::); let "f" be   ($#m1_subset_1 :::"Element":::) "of" (Set  "("  ($#k16_lopban_1 :::"R_NormSpace_of_BoundedLinearOperators"::: )   "(" (Set (Const "X")) "," (Set (Const "Y")) ")"  ")" ); let "v" be   ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Const "X")); :: original: :::"."::: redefine func "f" :::"."::: "v" ->   ($#m1_subset_1 :::"VECTOR":::) "of" "Y"; end; 
theorem :: LOPBAN_1:35 (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "being"   ($#l1_normsp_1 :::"RealNormSpace":::)  (Bool  "for" (Set (Var "f")) "," (Set (Var "g")) "," (Set (Var "h")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k16_lopban_1 :::"R_NormSpace_of_BoundedLinearOperators"::: )   "(" (Set (Var "X")) "," (Set (Var "Y")) ")"  ")" ) "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 :::"VECTOR":::) "of" (Set (Var "X")) "holds"  (Bool (Set (Set (Var "h"))  ($#k17_lopban_1 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "f"))  ($#k17_lopban_1 :::"."::: )  (Set (Var "x")) ")" )  ($#k3_rlvect_1 :::"+"::: )  (Set  "(" (Set (Var "g"))  ($#k17_lopban_1 :::"."::: )  (Set (Var "x")) ")" ))))  ")" ))) ; 
 
theorem :: LOPBAN_1:36 (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "being"   ($#l1_normsp_1 :::"RealNormSpace":::)  (Bool  "for" (Set (Var "f")) "," (Set (Var "h")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k16_lopban_1 :::"R_NormSpace_of_BoundedLinearOperators"::: )   "(" (Set (Var "X")) "," (Set (Var "Y")) ")"  ")" )  (Bool  "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Real":::) "holds"   (Bool  "("  (Bool (Set (Var "h"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "a"))  ($#k1_rlvect_1 :::"*"::: )  (Set (Var "f")))) "iff" (Bool  "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "X")) "holds"  (Bool (Set (Set (Var "h"))  ($#k17_lopban_1 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "a"))  ($#k1_rlvect_1 :::"*"::: )  (Set  "(" (Set (Var "f"))  ($#k17_lopban_1 :::"."::: )  (Set (Var "x")) ")" ))))  ")" )))) ; 
 
theorem :: LOPBAN_1:37 (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "being"   ($#l1_normsp_1 :::"RealNormSpace":::)  (Bool  "for" (Set (Var "f")) "," (Set (Var "g")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k16_lopban_1 :::"R_NormSpace_of_BoundedLinearOperators"::: )   "(" (Set (Var "X")) "," (Set (Var "Y")) ")"  ")" )  (Bool  "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Real":::) "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  "("  ($#k16_lopban_1 :::"R_NormSpace_of_BoundedLinearOperators"::: )   "(" (Set (Var "X")) "," (Set (Var "Y")) ")"  ")" )))  ")"  &  "("  (Bool (Bool (Set (Var "f"))  ($#r1_hidden :::"="::: )  (Set   ($#k4_struct_0 :::"0."::: )  (Set  "("  ($#k16_lopban_1 :::"R_NormSpace_of_BoundedLinearOperators"::: )   "(" (Set (Var "X")) "," (Set (Var "Y")) ")"  ")" )))) "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 :: LOPBAN_1:38 (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "being"   ($#l1_normsp_1 :::"RealNormSpace":::) "holds"   (Bool  "("  (Bool (Set   ($#k16_lopban_1 :::"R_NormSpace_of_BoundedLinearOperators"::: )   "(" (Set (Var "X")) "," (Set (Var "Y")) ")" ) "is"   ($#v4_normsp_0 :::"reflexive"::: )  ) & (Bool (Set   ($#k16_lopban_1 :::"R_NormSpace_of_BoundedLinearOperators"::: )   "(" (Set (Var "X")) "," (Set (Var "Y")) ")" ) "is"   ($#v3_normsp_0 :::"discerning"::: )  ) & (Bool (Set   ($#k16_lopban_1 :::"R_NormSpace_of_BoundedLinearOperators"::: )   "(" (Set (Var "X")) "," (Set (Var "Y")) ")" ) "is"   ($#v2_normsp_1 :::"RealNormSpace-like"::: )  )  ")" )) ; 
 
theorem :: LOPBAN_1:39 (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "being"   ($#l1_normsp_1 :::"RealNormSpace":::) "holds"  (Bool (Set   ($#k16_lopban_1 :::"R_NormSpace_of_BoundedLinearOperators"::: )   "(" (Set (Var "X")) "," (Set (Var "Y")) ")" ) "is"   ($#l1_normsp_1 :::"RealNormSpace":::))) ; 
 registrationlet "X", "Y" be   ($#l1_normsp_1 :::"RealNormSpace":::); 
cluster (Set   ($#k16_lopban_1 :::"R_NormSpace_of_BoundedLinearOperators"::: )   "(" "X" "," "Y" ")" ) ->  ($#~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"::: )   ; 
end; 
theorem :: LOPBAN_1:40 (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "being"   ($#l1_normsp_1 :::"RealNormSpace":::)  (Bool  "for" (Set (Var "f")) "," (Set (Var "g")) "," (Set (Var "h")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k16_lopban_1 :::"R_NormSpace_of_BoundedLinearOperators"::: )   "(" (Set (Var "X")) "," (Set (Var "Y")) ")"  ")" ) "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 :::"VECTOR":::) "of" (Set (Var "X")) "holds"  (Bool (Set (Set (Var "h"))  ($#k17_lopban_1 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "f"))  ($#k17_lopban_1 :::"."::: )  (Set (Var "x")) ")" )  ($#k5_algstr_0 :::"-"::: )  (Set  "(" (Set (Var "g"))  ($#k17_lopban_1 :::"."::: )  (Set (Var "x")) ")" ))))  ")" ))) ; 
 begin  definitionlet "X" be   ($#l1_normsp_1 :::"RealNormSpace":::); attr "X" is  :::"complete":::  means :: LOPBAN_1:def 15 (Bool  "for" (Set (Var "seq")) "being"   ($#m1_subset_1 :::"sequence":::) "of" "X"  "st" (Bool (Bool (Set (Var "seq")) "is"   ($#v1_rsspace3 :::"Cauchy_sequence_by_Norm"::: )  )) "holds"  (Bool (Set (Var "seq")) "is"   ($#v3_normsp_1 :::"convergent"::: )  )); end; 




:: deftheorem    defines :::"complete"::: LOPBAN_1:def 15 :  (Bool  "for" (Set (Var "X")) "being"   ($#l1_normsp_1 :::"RealNormSpace":::) "holds"   (Bool  "("  (Bool (Set (Var "X")) "is"   ($#v3_lopban_1 :::"complete"::: )  ) "iff" (Bool  "for" (Set (Var "seq")) "being"   ($#m1_subset_1 :::"sequence":::) "of" (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"::: )  ))  ")" )); 
 registration
cluster  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v12_algstr_0 :::"left_complementable"::: )     ($#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"::: )   bbbadV9_RLVECT_1()   ($#v3_normsp_0 :::"discerning"::: )     ($#v4_normsp_0 :::"reflexive"::: )     ($#v2_normsp_1 :::"RealNormSpace-like"::: )     ($#v3_lopban_1 :::"complete"::: )    for    ($#l1_normsp_1 :::"NORMSTR"::: )  ; 
end; definitionmode RealBanachSpace is   ($#v3_lopban_1 :::"complete"::: )    ($#l1_normsp_1 :::"RealNormSpace":::); end; 
theorem :: LOPBAN_1:41 (Bool  "for" (Set (Var "X")) "being"   ($#l1_normsp_1 :::"RealNormSpace":::)  (Bool  "for" (Set (Var "seq")) "being"   ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X"))  "st" (Bool (Bool (Set (Var "seq")) "is"   ($#v3_normsp_1 :::"convergent"::: )  )) "holds"  (Bool  "("  (Bool (Set  ($#k4_normsp_0 :::"||."::: ) (Set (Var "seq")) ($#k4_normsp_0 :::".||"::: ) ) "is"   ($#v2_comseq_2 :::"convergent"::: )  ) & (Bool (Set   ($#k2_seq_2 :::"lim"::: )  (Set  ($#k4_normsp_0 :::"||."::: ) (Set (Var "seq")) ($#k4_normsp_0 :::".||"::: ) ))  ($#r1_hidden :::"="::: )  (Set  ($#k1_normsp_0 :::"||."::: ) (Set  "("  ($#k6_normsp_1 :::"lim"::: )  (Set (Var "seq")) ")" ) ($#k1_normsp_0 :::".||"::: ) ))  ")" ))) ; 
 
theorem :: LOPBAN_1:42 (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "being"   ($#l1_normsp_1 :::"RealNormSpace":::)  "st" (Bool (Bool (Set (Var "Y")) "is"   ($#v3_lopban_1 :::"complete"::: )  )) "holds"  (Bool  "for" (Set (Var "seq")) "being"   ($#m1_subset_1 :::"sequence":::) "of" (Set  "("  ($#k16_lopban_1 :::"R_NormSpace_of_BoundedLinearOperators"::: )   "(" (Set (Var "X")) "," (Set (Var "Y")) ")"  ")" )  "st" (Bool (Bool (Set (Var "seq")) "is"   ($#v1_rsspace3 :::"Cauchy_sequence_by_Norm"::: )  )) "holds"  (Bool (Set (Var "seq")) "is"   ($#v3_normsp_1 :::"convergent"::: )  ))) ; 
 
theorem :: LOPBAN_1:43 (Bool  "for" (Set (Var "X")) "being"   ($#l1_normsp_1 :::"RealNormSpace":::)  (Bool  "for" (Set (Var "Y")) "being"   ($#l1_normsp_1 :::"RealBanachSpace":::) "holds"  (Bool (Set   ($#k16_lopban_1 :::"R_NormSpace_of_BoundedLinearOperators"::: )   "(" (Set (Var "X")) "," (Set (Var "Y")) ")" ) "is"   ($#l1_normsp_1 :::"RealBanachSpace":::)))) ; 
 registrationlet "X" be   ($#l1_normsp_1 :::"RealNormSpace":::); let "Y" be   ($#l1_normsp_1 :::"RealBanachSpace":::); 
cluster (Set   ($#k16_lopban_1 :::"R_NormSpace_of_BoundedLinearOperators"::: )   "(" "X" "," "Y" ")" ) ->  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v3_lopban_1 :::"complete"::: )   ; 
end;