:: HAHNBAN1  semantic presentation begin  
theorem :: HAHNBAN1:1 canceled; 
 
theorem :: HAHNBAN1:2 (Bool  "for" (Set (Var "x1")) "," (Set (Var "y1")) "," (Set (Var "x2")) "," (Set (Var "y2")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set  "(" (Set (Var "x1"))  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" (Set (Var "y1"))  ($#k3_xcmplx_0 :::"*"::: )  (Set  ($#k7_complex1 :::"<i>"::: ) ) ")" ) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set  "(" (Set (Var "x2"))  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" (Set (Var "y2"))  ($#k3_xcmplx_0 :::"*"::: )  (Set  ($#k7_complex1 :::"<i>"::: ) ) ")" ) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set (Var "x1"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "x2")) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" (Set (Var "y1"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "y2")) ")" ) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" (Set  "(" (Set  "(" (Set (Var "x1"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "y2")) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" (Set (Var "x2"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "y1")) ")" ) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set  ($#k7_complex1 :::"<i>"::: ) ) ")" )))) ; 
 
theorem :: HAHNBAN1:3 (Bool  "for" (Set (Var "z")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k2_numbers :::"COMPLEX"::: )  ) "holds"  (Bool (Set (Set  ($#k17_complex1 :::"|."::: ) (Set (Var "z")) ($#k17_complex1 :::".|"::: ) )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" (Set  ($#k6_numbers :::"0"::: ) )  ($#k3_xcmplx_0 :::"*"::: )  (Set  ($#k7_complex1 :::"<i>"::: ) ) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set (Var "z"))  ($#k15_complex1 :::"*'"::: )  ")" )  ($#k13_complex1 :::"/"::: )  (Set  "(" (Set  ($#k17_complex1 :::"|."::: ) (Set (Var "z")) ($#k17_complex1 :::".|"::: ) )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" (Set  ($#k6_numbers :::"0"::: ) )  ($#k3_xcmplx_0 :::"*"::: )  (Set  ($#k7_complex1 :::"<i>"::: ) ) ")" ) ")" ) ")" )  ($#k9_complex1 :::"*"::: )  (Set (Var "z"))))) ; 
 begin  definitionlet "x", "y" be   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )  ; func :::"[**":::"x" "," "y":::"**]"::: ->   ($#m1_subset_1 :::"Element":::) "of" (Set  ($#k1_complfld :::"F_Complex"::: ) ) equals :: HAHNBAN1:def 1 (Set "x"  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" "y"  ($#k3_xcmplx_0 :::"*"::: )  (Set  ($#k7_complex1 :::"<i>"::: ) ) ")" )); end; 






:: deftheorem    defines :::"[**"::: HAHNBAN1:def 1 :  (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set  ($#k1_hahnban1 :::"[**"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k1_hahnban1 :::"**]"::: ) )  ($#r1_hidden :::"="::: )  (Set (Set (Var "x"))  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" (Set (Var "y"))  ($#k3_xcmplx_0 :::"*"::: )  (Set  ($#k7_complex1 :::"<i>"::: ) ) ")" )))); 
 definitionfunc  :::"i_FC":::  ->   ($#m1_subset_1 :::"Element":::) "of" (Set  ($#k1_complfld :::"F_Complex"::: ) ) equals :: HAHNBAN1:def 2 (Set   ($#k7_complex1 :::"<i>"::: )  ); end; 




:: deftheorem    defines :::"i_FC"::: HAHNBAN1:def 2 :  (Bool (Set   ($#k2_hahnban1 :::"i_FC"::: )  )  ($#r1_hidden :::"="::: )  (Set   ($#k7_complex1 :::"<i>"::: )  )); 
 
theorem :: HAHNBAN1:4 (Bool (Set (Set  ($#k2_hahnban1 :::"i_FC"::: ) )  ($#k8_group_1 :::"*"::: )  (Set  ($#k2_hahnban1 :::"i_FC"::: ) ))  ($#r1_hidden :::"="::: )  (Set   ($#k4_algstr_0 :::"-"::: )  (Set  "("  ($#k1_group_1 :::"1_"::: )  (Set  ($#k1_complfld :::"F_Complex"::: ) ) ")" ))) ; 
 
theorem :: HAHNBAN1:5 (Bool (Set (Set  "("  ($#k4_algstr_0 :::"-"::: )  (Set  "("  ($#k1_group_1 :::"1_"::: )  (Set  ($#k1_complfld :::"F_Complex"::: ) ) ")" ) ")" )  ($#k8_group_1 :::"*"::: )  (Set  "("  ($#k4_algstr_0 :::"-"::: )  (Set  "("  ($#k1_group_1 :::"1_"::: )  (Set  ($#k1_complfld :::"F_Complex"::: ) ) ")" ) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k1_group_1 :::"1_"::: )  (Set  ($#k1_complfld :::"F_Complex"::: ) ))) ; 
 
theorem :: HAHNBAN1:6 (Bool  "for" (Set (Var "x1")) "," (Set (Var "y1")) "," (Set (Var "x2")) "," (Set (Var "y2")) "being"   ($#m1_subset_1 :::"Real":::) "holds"  (Bool (Set (Set  ($#k1_hahnban1 :::"[**"::: ) (Set (Var "x1")) "," (Set (Var "y1")) ($#k1_hahnban1 :::"**]"::: ) )  ($#k3_rlvect_1 :::"+"::: )  (Set  ($#k1_hahnban1 :::"[**"::: ) (Set (Var "x2")) "," (Set (Var "y2")) ($#k1_hahnban1 :::"**]"::: ) ))  ($#r1_hidden :::"="::: )  (Set  ($#k1_hahnban1 :::"[**"::: ) (Set  "(" (Set (Var "x1"))  ($#k7_real_1 :::"+"::: )  (Set (Var "x2")) ")" ) "," (Set  "(" (Set (Var "y1"))  ($#k7_real_1 :::"+"::: )  (Set (Var "y2")) ")" ) ($#k1_hahnban1 :::"**]"::: ) ))) ; 
 
theorem :: HAHNBAN1:7 (Bool  "for" (Set (Var "x1")) "," (Set (Var "y1")) "," (Set (Var "x2")) "," (Set (Var "y2")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set  ($#k1_hahnban1 :::"[**"::: ) (Set (Var "x1")) "," (Set (Var "y1")) ($#k1_hahnban1 :::"**]"::: ) )  ($#k8_group_1 :::"*"::: )  (Set  ($#k1_hahnban1 :::"[**"::: ) (Set (Var "x2")) "," (Set (Var "y2")) ($#k1_hahnban1 :::"**]"::: ) ))  ($#r1_hidden :::"="::: )  (Set  ($#k1_hahnban1 :::"[**"::: ) (Set  "(" (Set  "(" (Set (Var "x1"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "x2")) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" (Set (Var "y1"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "y2")) ")" ) ")" ) "," (Set  "(" (Set  "(" (Set (Var "x1"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "y2")) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" (Set (Var "x2"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "y1")) ")" ) ")" ) ($#k1_hahnban1 :::"**]"::: ) ))) ; 
 
theorem :: HAHNBAN1:8 canceled; 
 
theorem :: HAHNBAN1:9 (Bool  "for" (Set (Var "r")) "being"   ($#m1_subset_1 :::"Real":::) "holds"  (Bool (Set  ($#k17_complex1 :::"|."::: ) (Set  ($#k1_hahnban1 :::"[**"::: ) (Set (Var "r")) "," (Set  ($#k6_numbers :::"0"::: ) ) ($#k1_hahnban1 :::"**]"::: ) ) ($#k17_complex1 :::".|"::: ) )  ($#r1_hidden :::"="::: )  (Set   ($#k18_complex1 :::"abs"::: )  (Set (Var "r"))))) ; 
 
theorem :: HAHNBAN1:10 (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set  ($#k1_complfld :::"F_Complex"::: ) ) "holds"   (Bool  "("  (Bool (Set   ($#k3_complex1 :::"Re"::: )  (Set  "(" (Set (Var "x"))  ($#k3_rlvect_1 :::"+"::: )  (Set (Var "y")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k3_complex1 :::"Re"::: )  (Set (Var "x")) ")" )  ($#k7_real_1 :::"+"::: )  (Set  "("  ($#k3_complex1 :::"Re"::: )  (Set (Var "y")) ")" ))) & (Bool (Set   ($#k4_complex1 :::"Im"::: )  (Set  "(" (Set (Var "x"))  ($#k3_rlvect_1 :::"+"::: )  (Set (Var "y")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k4_complex1 :::"Im"::: )  (Set (Var "x")) ")" )  ($#k7_real_1 :::"+"::: )  (Set  "("  ($#k4_complex1 :::"Im"::: )  (Set (Var "y")) ")" )))  ")" )) ; 
 
theorem :: HAHNBAN1:11 (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set  ($#k1_complfld :::"F_Complex"::: ) ) "holds"   (Bool  "("  (Bool (Set   ($#k3_complex1 :::"Re"::: )  (Set  "(" (Set (Var "x"))  ($#k8_group_1 :::"*"::: )  (Set (Var "y")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "("  ($#k3_complex1 :::"Re"::: )  (Set (Var "x")) ")" )  ($#k8_real_1 :::"*"::: )  (Set  "("  ($#k3_complex1 :::"Re"::: )  (Set (Var "y")) ")" ) ")" )  ($#k9_real_1 :::"-"::: )  (Set  "(" (Set  "("  ($#k4_complex1 :::"Im"::: )  (Set (Var "x")) ")" )  ($#k8_real_1 :::"*"::: )  (Set  "("  ($#k4_complex1 :::"Im"::: )  (Set (Var "y")) ")" ) ")" ))) & (Bool (Set   ($#k4_complex1 :::"Im"::: )  (Set  "(" (Set (Var "x"))  ($#k8_group_1 :::"*"::: )  (Set (Var "y")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "("  ($#k3_complex1 :::"Re"::: )  (Set (Var "x")) ")" )  ($#k8_real_1 :::"*"::: )  (Set  "("  ($#k4_complex1 :::"Im"::: )  (Set (Var "y")) ")" ) ")" )  ($#k7_real_1 :::"+"::: )  (Set  "(" (Set  "("  ($#k3_complex1 :::"Re"::: )  (Set (Var "y")) ")" )  ($#k8_real_1 :::"*"::: )  (Set  "("  ($#k4_complex1 :::"Im"::: )  (Set (Var "x")) ")" ) ")" )))  ")" )) ; 
 begin  definitionlet "K" be    ($#l1_struct_0 :::"1-sorted"::: )  ; let "V" be    ($#l1_vectsp_1 :::"VectSpStr"::: )   "over" (Set (Const "K")); mode Functional of "V" is   ($#m1_subset_1 :::"Function":::) "of" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "V") "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "K"); end; definitionlet "K" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l2_algstr_0 :::"addLoopStr"::: )  ; let "V" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_vectsp_1 :::"VectSpStr"::: )   "over" (Set (Const "K")); let "f", "g" be   ($#m1_subset_1 :::"Functional":::) "of" (Set (Const "V")); func "f" :::"+"::: "g" ->   ($#m1_subset_1 :::"Functional":::) "of" "V" means :: HAHNBAN1:def 3 (Bool  "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Element":::) "of" "V" "holds"  (Bool (Set it  ($#k3_funct_2 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" "f"  ($#k3_funct_2 :::"."::: )  (Set (Var "x")) ")" )  ($#k1_algstr_0 :::"+"::: )  (Set  "(" "g"  ($#k3_funct_2 :::"."::: )  (Set (Var "x")) ")" )))); end; 








:: deftheorem    defines :::"+"::: HAHNBAN1:def 3 :  (Bool  "for" (Set (Var "K")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l2_algstr_0 :::"addLoopStr"::: )    (Bool  "for" (Set (Var "V")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_vectsp_1 :::"VectSpStr"::: )   "over" (Set (Var "K"))  (Bool  "for" (Set (Var "f")) "," (Set (Var "g")) "," (Set (Var "b5")) "being"   ($#m1_subset_1 :::"Functional":::) "of" (Set (Var "V")) "holds"   (Bool  "("  (Bool (Set (Var "b5"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "f"))  ($#k3_hahnban1 :::"+"::: )  (Set (Var "g")))) "iff" (Bool  "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "V")) "holds"  (Bool (Set (Set (Var "b5"))  ($#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")) ")" ))))  ")" )))); 
 definitionlet "K" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l2_algstr_0 :::"addLoopStr"::: )  ; let "V" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_vectsp_1 :::"VectSpStr"::: )   "over" (Set (Const "K")); let "f" be   ($#m1_subset_1 :::"Functional":::) "of" (Set (Const "V")); func  :::"-"::: "f" ->   ($#m1_subset_1 :::"Functional":::) "of" "V" means :: HAHNBAN1:def 4 (Bool  "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Element":::) "of" "V" "holds"  (Bool (Set it  ($#k3_funct_2 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set   ($#k4_algstr_0 :::"-"::: )  (Set  "(" "f"  ($#k3_funct_2 :::"."::: )  (Set (Var "x")) ")" )))); end; 







:: deftheorem    defines :::"-"::: HAHNBAN1:def 4 :  (Bool  "for" (Set (Var "K")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l2_algstr_0 :::"addLoopStr"::: )    (Bool  "for" (Set (Var "V")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_vectsp_1 :::"VectSpStr"::: )   "over" (Set (Var "K"))  (Bool  "for" (Set (Var "f")) "," (Set (Var "b4")) "being"   ($#m1_subset_1 :::"Functional":::) "of" (Set (Var "V")) "holds"   (Bool  "("  (Bool (Set (Var "b4"))  ($#r1_hidden :::"="::: )  (Set   ($#k4_hahnban1 :::"-"::: )  (Set (Var "f")))) "iff" (Bool  "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "V")) "holds"  (Bool (Set (Set (Var "b4"))  ($#k3_funct_2 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set   ($#k4_algstr_0 :::"-"::: )  (Set  "(" (Set (Var "f"))  ($#k3_funct_2 :::"."::: )  (Set (Var "x")) ")" ))))  ")" )))); 
 definitionlet "K" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l2_algstr_0 :::"addLoopStr"::: )  ; let "V" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_vectsp_1 :::"VectSpStr"::: )   "over" (Set (Const "K")); let "f", "g" be   ($#m1_subset_1 :::"Functional":::) "of" (Set (Const "V")); func "f" :::"-"::: "g" ->   ($#m1_subset_1 :::"Functional":::) "of" "V" equals :: HAHNBAN1:def 5 (Set "f"  ($#k3_hahnban1 :::"+"::: )  (Set  "("  ($#k4_hahnban1 :::"-"::: )  "g" ")" )); end; 








:: deftheorem    defines :::"-"::: HAHNBAN1:def 5 :  (Bool  "for" (Set (Var "K")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l2_algstr_0 :::"addLoopStr"::: )    (Bool  "for" (Set (Var "V")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_vectsp_1 :::"VectSpStr"::: )   "over" (Set (Var "K"))  (Bool  "for" (Set (Var "f")) "," (Set (Var "g")) "being"   ($#m1_subset_1 :::"Functional":::) "of" (Set (Var "V")) "holds"  (Bool (Set (Set (Var "f"))  ($#k5_hahnban1 :::"-"::: )  (Set (Var "g")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "f"))  ($#k3_hahnban1 :::"+"::: )  (Set  "("  ($#k4_hahnban1 :::"-"::: )  (Set (Var "g")) ")" )))))); 
 definitionlet "K" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l3_algstr_0 :::"multMagma"::: )  ; let "V" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_vectsp_1 :::"VectSpStr"::: )   "over" (Set (Const "K")); let "v" be   ($#m1_subset_1 :::"Element":::) "of" (Set (Const "K")); let "f" be   ($#m1_subset_1 :::"Functional":::) "of" (Set (Const "V")); func "v" :::"*"::: "f" ->   ($#m1_subset_1 :::"Functional":::) "of" "V" means :: HAHNBAN1:def 6 (Bool  "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Element":::) "of" "V" "holds"  (Bool (Set it  ($#k3_funct_2 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set "v"  ($#k6_algstr_0 :::"*"::: )  (Set  "(" "f"  ($#k3_funct_2 :::"."::: )  (Set (Var "x")) ")" )))); end; 








:: deftheorem    defines :::"*"::: HAHNBAN1:def 6 :  (Bool  "for" (Set (Var "K")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l3_algstr_0 :::"multMagma"::: )    (Bool  "for" (Set (Var "V")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_vectsp_1 :::"VectSpStr"::: )   "over" (Set (Var "K"))  (Bool  "for" (Set (Var "v")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "K"))  (Bool  "for" (Set (Var "f")) "," (Set (Var "b5")) "being"   ($#m1_subset_1 :::"Functional":::) "of" (Set (Var "V")) "holds"   (Bool  "("  (Bool (Set (Var "b5"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "v"))  ($#k6_hahnban1 :::"*"::: )  (Set (Var "f")))) "iff" (Bool  "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "V")) "holds"  (Bool (Set (Set (Var "b5"))  ($#k3_funct_2 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "v"))  ($#k6_algstr_0 :::"*"::: )  (Set  "(" (Set (Var "f"))  ($#k3_funct_2 :::"."::: )  (Set (Var "x")) ")" ))))  ")" ))))); 
 definitionlet "K" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l2_struct_0 :::"ZeroStr"::: )  ; let "V" be    ($#l1_vectsp_1 :::"VectSpStr"::: )   "over" (Set (Const "K")); func  :::"0Functional"::: "V" ->   ($#m1_subset_1 :::"Functional":::) "of" "V" equals :: HAHNBAN1:def 7 (Set (Set  "("  ($#k2_struct_0 :::"[#]"::: )  "V" ")" )  ($#k8_funcop_1 :::"-->"::: )  (Set  "("  ($#k4_struct_0 :::"0."::: )  "K" ")" )); end; 






:: deftheorem    defines :::"0Functional"::: HAHNBAN1:def 7 :  (Bool  "for" (Set (Var "K")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l2_struct_0 :::"ZeroStr"::: )    (Bool  "for" (Set (Var "V")) "being"    ($#l1_vectsp_1 :::"VectSpStr"::: )   "over" (Set (Var "K")) "holds"  (Bool (Set   ($#k7_hahnban1 :::"0Functional"::: )  (Set (Var "V")))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k2_struct_0 :::"[#]"::: )  (Set (Var "V")) ")" )  ($#k8_funcop_1 :::"-->"::: )  (Set  "("  ($#k4_struct_0 :::"0."::: )  (Set (Var "K")) ")" ))))); 
 definitionlet "K" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l3_algstr_0 :::"multMagma"::: )  ; let "V" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_vectsp_1 :::"VectSpStr"::: )   "over" (Set (Const "K")); let "F" be   ($#m1_subset_1 :::"Functional":::) "of" (Set (Const "V")); attr "F" is  :::"homogeneous":::  means :: HAHNBAN1:def 8 (Bool  "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Vector":::) "of" "V"  (Bool  "for" (Set (Var "r")) "being"   ($#m1_subset_1 :::"Scalar":::) "of"  "holds"  (Bool (Set "F"  ($#k3_funct_2 :::"."::: )  (Set  "(" (Set (Var "r"))  ($#k4_vectsp_1 :::"*"::: )  (Set (Var "x")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "r"))  ($#k6_algstr_0 :::"*"::: )  (Set  "(" "F"  ($#k3_funct_2 :::"."::: )  (Set (Var "x")) ")" ))))); end; 






:: deftheorem    defines :::"homogeneous"::: HAHNBAN1:def 8 :  (Bool  "for" (Set (Var "K")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l3_algstr_0 :::"multMagma"::: )    (Bool  "for" (Set (Var "V")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_vectsp_1 :::"VectSpStr"::: )   "over" (Set (Var "K"))  (Bool  "for" (Set (Var "F")) "being"   ($#m1_subset_1 :::"Functional":::) "of" (Set (Var "V")) "holds"   (Bool  "("  (Bool (Set (Var "F")) "is"   ($#v1_hahnban1 :::"homogeneous"::: )  ) "iff" (Bool  "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Vector":::) "of" (Set (Var "V"))  (Bool  "for" (Set (Var "r")) "being"   ($#m1_subset_1 :::"Scalar":::) "of"  "holds"  (Bool (Set (Set (Var "F"))  ($#k3_funct_2 :::"."::: )  (Set  "(" (Set (Var "r"))  ($#k4_vectsp_1 :::"*"::: )  (Set (Var "x")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "r"))  ($#k6_algstr_0 :::"*"::: )  (Set  "(" (Set (Var "F"))  ($#k3_funct_2 :::"."::: )  (Set (Var "x")) ")" )))))  ")" )))); 
 definitionlet "K" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l2_struct_0 :::"ZeroStr"::: )  ; let "V" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_vectsp_1 :::"VectSpStr"::: )   "over" (Set (Const "K")); let "F" be   ($#m1_subset_1 :::"Functional":::) "of" (Set (Const "V")); attr "F" is  :::"0-preserving":::  means :: HAHNBAN1:def 9 (Bool (Set "F"  ($#k3_funct_2 :::"."::: )  (Set  "("  ($#k4_struct_0 :::"0."::: )  "V" ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k4_struct_0 :::"0."::: )  "K")); end; 






:: deftheorem    defines :::"0-preserving"::: HAHNBAN1:def 9 :  (Bool  "for" (Set (Var "K")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l2_struct_0 :::"ZeroStr"::: )    (Bool  "for" (Set (Var "V")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_vectsp_1 :::"VectSpStr"::: )   "over" (Set (Var "K"))  (Bool  "for" (Set (Var "F")) "being"   ($#m1_subset_1 :::"Functional":::) "of" (Set (Var "V")) "holds"   (Bool  "("  (Bool (Set (Var "F")) "is"   ($#v2_hahnban1 :::"0-preserving"::: )  ) "iff" (Bool (Set (Set (Var "F"))  ($#k3_funct_2 :::"."::: )  (Set  "("  ($#k4_struct_0 :::"0."::: )  (Set (Var "V")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k4_struct_0 :::"0."::: )  (Set (Var "K"))))  ")" )))); 
 registrationlet "K" be  ($#~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"::: )     ($#v3_group_1 :::"associative"::: )     ($#v4_vectsp_1 :::"well-unital"::: )     ($#v5_vectsp_1 :::"distributive"::: )     ($#l6_algstr_0 :::"doubleLoopStr"::: )  ; let "V" be   ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Const "K")); 
cluster   ($#v1_funct_1 :::"Function-like"::: )   bbbadV1_FUNCT_2((Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "V") "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "K"))   ($#v1_hahnban1 :::"homogeneous"::: )    ->   ($#v2_hahnban1 :::"0-preserving"::: )    for    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k1_zfmisc_1 :::"bool"::: )  (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "V") "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "K") ($#k2_zfmisc_1 :::":]"::: ) )); 
end; registrationlet "K" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v4_rlvect_1 :::"right_zeroed"::: )     ($#l2_algstr_0 :::"addLoopStr"::: )  ; let "V" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_vectsp_1 :::"VectSpStr"::: )   "over" (Set (Const "K")); 
cluster (Set   ($#k7_hahnban1 :::"0Functional"::: )  "V") ->   ($#v13_vectsp_1 :::"additive"::: )   ; 
end; registrationlet "K" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v13_algstr_0 :::"right_complementable"::: )     ($#v3_rlvect_1 :::"add-associative"::: )     ($#v4_rlvect_1 :::"right_zeroed"::: )     ($#v1_vectsp_1 :::"right-distributive"::: )     ($#l6_algstr_0 :::"doubleLoopStr"::: )  ; let "V" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_vectsp_1 :::"VectSpStr"::: )   "over" (Set (Const "K")); 
cluster (Set   ($#k7_hahnban1 :::"0Functional"::: )  "V") ->   ($#v1_hahnban1 :::"homogeneous"::: )   ; 
end; registrationlet "K" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l2_struct_0 :::"ZeroStr"::: )  ; let "V" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_vectsp_1 :::"VectSpStr"::: )   "over" (Set (Const "K")); 
cluster (Set   ($#k7_hahnban1 :::"0Functional"::: )  "V") ->   ($#v2_hahnban1 :::"0-preserving"::: )   ; 
end; registrationlet "K" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v13_algstr_0 :::"right_complementable"::: )     ($#v3_rlvect_1 :::"add-associative"::: )     ($#v4_rlvect_1 :::"right_zeroed"::: )     ($#v1_vectsp_1 :::"right-distributive"::: )     ($#l6_algstr_0 :::"doubleLoopStr"::: )  ; let "V" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_vectsp_1 :::"VectSpStr"::: )   "over" (Set (Const "K")); 
cluster bbbadV1_RELAT_1() bbbadV4_RELAT_1((Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "V")) bbbadV5_RELAT_1((Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "K"))   ($#v1_funct_1 :::"Function-like"::: )   bbbadV1_FUNCT_2((Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "V") "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "K"))   ($#v13_vectsp_1 :::"additive"::: )     ($#v1_hahnban1 :::"homogeneous"::: )     ($#v2_hahnban1 :::"0-preserving"::: )    for    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k1_zfmisc_1 :::"bool"::: )  (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "V") "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "K") ($#k2_zfmisc_1 :::":]"::: ) )); 
end; 
theorem :: HAHNBAN1:12 (Bool  "for" (Set (Var "K")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v2_rlvect_1 :::"Abelian"::: )     ($#l2_algstr_0 :::"addLoopStr"::: )    (Bool  "for" (Set (Var "V")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_vectsp_1 :::"VectSpStr"::: )   "over" (Set (Var "K"))  (Bool  "for" (Set (Var "f")) "," (Set (Var "g")) "being"   ($#m1_subset_1 :::"Functional":::) "of" (Set (Var "V")) "holds"  (Bool (Set (Set (Var "f"))  ($#k3_hahnban1 :::"+"::: )  (Set (Var "g")))  ($#r2_relset_1 :::"="::: )  (Set (Set (Var "g"))  ($#k3_hahnban1 :::"+"::: )  (Set (Var "f"))))))) ; 
 
theorem :: HAHNBAN1:13 (Bool  "for" (Set (Var "K")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v3_rlvect_1 :::"add-associative"::: )     ($#l2_algstr_0 :::"addLoopStr"::: )    (Bool  "for" (Set (Var "V")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_vectsp_1 :::"VectSpStr"::: )   "over" (Set (Var "K"))  (Bool  "for" (Set (Var "f")) "," (Set (Var "g")) "," (Set (Var "h")) "being"   ($#m1_subset_1 :::"Functional":::) "of" (Set (Var "V")) "holds"  (Bool (Set (Set  "(" (Set (Var "f"))  ($#k3_hahnban1 :::"+"::: )  (Set (Var "g")) ")" )  ($#k3_hahnban1 :::"+"::: )  (Set (Var "h")))  ($#r2_relset_1 :::"="::: )  (Set (Set (Var "f"))  ($#k3_hahnban1 :::"+"::: )  (Set  "(" (Set (Var "g"))  ($#k3_hahnban1 :::"+"::: )  (Set (Var "h")) ")" )))))) ; 
 
theorem :: HAHNBAN1:14 (Bool  "for" (Set (Var "K")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l2_struct_0 :::"ZeroStr"::: )    (Bool  "for" (Set (Var "V")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_vectsp_1 :::"VectSpStr"::: )   "over" (Set (Var "K"))  (Bool  "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "V")) "holds"  (Bool (Set (Set  "("  ($#k7_hahnban1 :::"0Functional"::: )  (Set (Var "V")) ")" )  ($#k3_funct_2 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set   ($#k4_struct_0 :::"0."::: )  (Set (Var "K"))))))) ; 
 
theorem :: HAHNBAN1:15 (Bool  "for" (Set (Var "K")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v4_rlvect_1 :::"right_zeroed"::: )     ($#l2_algstr_0 :::"addLoopStr"::: )    (Bool  "for" (Set (Var "V")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_vectsp_1 :::"VectSpStr"::: )   "over" (Set (Var "K"))  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Functional":::) "of" (Set (Var "V")) "holds"  (Bool (Set (Set (Var "f"))  ($#k3_hahnban1 :::"+"::: )  (Set  "("  ($#k7_hahnban1 :::"0Functional"::: )  (Set (Var "V")) ")" ))  ($#r2_relset_1 :::"="::: )  (Set (Var "f")))))) ; 
 
theorem :: HAHNBAN1:16 (Bool  "for" (Set (Var "K")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v13_algstr_0 :::"right_complementable"::: )     ($#v3_rlvect_1 :::"add-associative"::: )     ($#v4_rlvect_1 :::"right_zeroed"::: )     ($#l2_algstr_0 :::"addLoopStr"::: )    (Bool  "for" (Set (Var "V")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_vectsp_1 :::"VectSpStr"::: )   "over" (Set (Var "K"))  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Functional":::) "of" (Set (Var "V")) "holds"  (Bool (Set (Set (Var "f"))  ($#k5_hahnban1 :::"-"::: )  (Set (Var "f")))  ($#r2_relset_1 :::"="::: )  (Set   ($#k7_hahnban1 :::"0Functional"::: )  (Set (Var "V"))))))) ; 
 
theorem :: HAHNBAN1:17 (Bool  "for" (Set (Var "K")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v1_vectsp_1 :::"right-distributive"::: )     ($#l6_algstr_0 :::"doubleLoopStr"::: )    (Bool  "for" (Set (Var "V")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_vectsp_1 :::"VectSpStr"::: )   "over" (Set (Var "K"))  (Bool  "for" (Set (Var "r")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "K"))  (Bool  "for" (Set (Var "f")) "," (Set (Var "g")) "being"   ($#m1_subset_1 :::"Functional":::) "of" (Set (Var "V")) "holds"  (Bool (Set (Set (Var "r"))  ($#k6_hahnban1 :::"*"::: )  (Set  "(" (Set (Var "f"))  ($#k3_hahnban1 :::"+"::: )  (Set (Var "g")) ")" ))  ($#r2_relset_1 :::"="::: )  (Set (Set  "(" (Set (Var "r"))  ($#k6_hahnban1 :::"*"::: )  (Set (Var "f")) ")" )  ($#k3_hahnban1 :::"+"::: )  (Set  "(" (Set (Var "r"))  ($#k6_hahnban1 :::"*"::: )  (Set (Var "g")) ")" ))))))) ; 
 
theorem :: HAHNBAN1:18 (Bool  "for" (Set (Var "K")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v2_vectsp_1 :::"left-distributive"::: )     ($#l6_algstr_0 :::"doubleLoopStr"::: )    (Bool  "for" (Set (Var "V")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_vectsp_1 :::"VectSpStr"::: )   "over" (Set (Var "K"))  (Bool  "for" (Set (Var "r")) "," (Set (Var "s")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "K"))  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Functional":::) "of" (Set (Var "V")) "holds"  (Bool (Set (Set  "(" (Set (Var "r"))  ($#k1_algstr_0 :::"+"::: )  (Set (Var "s")) ")" )  ($#k6_hahnban1 :::"*"::: )  (Set (Var "f")))  ($#r2_relset_1 :::"="::: )  (Set (Set  "(" (Set (Var "r"))  ($#k6_hahnban1 :::"*"::: )  (Set (Var "f")) ")" )  ($#k3_hahnban1 :::"+"::: )  (Set  "(" (Set (Var "s"))  ($#k6_hahnban1 :::"*"::: )  (Set (Var "f")) ")" ))))))) ; 
 
theorem :: HAHNBAN1:19 (Bool  "for" (Set (Var "K")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v3_group_1 :::"associative"::: )     ($#l3_algstr_0 :::"multMagma"::: )    (Bool  "for" (Set (Var "V")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_vectsp_1 :::"VectSpStr"::: )   "over" (Set (Var "K"))  (Bool  "for" (Set (Var "r")) "," (Set (Var "s")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "K"))  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Functional":::) "of" (Set (Var "V")) "holds"  (Bool (Set (Set  "(" (Set (Var "r"))  ($#k6_algstr_0 :::"*"::: )  (Set (Var "s")) ")" )  ($#k6_hahnban1 :::"*"::: )  (Set (Var "f")))  ($#r2_relset_1 :::"="::: )  (Set (Set (Var "r"))  ($#k6_hahnban1 :::"*"::: )  (Set  "(" (Set (Var "s"))  ($#k6_hahnban1 :::"*"::: )  (Set (Var "f")) ")" ))))))) ; 
 
theorem :: HAHNBAN1:20 (Bool  "for" (Set (Var "K")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v6_vectsp_1 :::"left_unital"::: )     ($#l6_algstr_0 :::"doubleLoopStr"::: )    (Bool  "for" (Set (Var "V")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_vectsp_1 :::"VectSpStr"::: )   "over" (Set (Var "K"))  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Functional":::) "of" (Set (Var "V")) "holds"  (Bool (Set (Set  "("  ($#k5_struct_0 :::"1."::: )  (Set (Var "K")) ")" )  ($#k6_hahnban1 :::"*"::: )  (Set (Var "f")))  ($#r2_relset_1 :::"="::: )  (Set (Var "f")))))) ; 
 registrationlet "K" be  ($#~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"::: )     ($#v1_vectsp_1 :::"right-distributive"::: )     ($#l6_algstr_0 :::"doubleLoopStr"::: )  ; let "V" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_vectsp_1 :::"VectSpStr"::: )   "over" (Set (Const "K")); let "f", "g" be   ($#v13_vectsp_1 :::"additive"::: )    ($#m1_subset_1 :::"Functional":::) "of" (Set (Const "V")); 
cluster (Set "f"  ($#k3_hahnban1 :::"+"::: )  "g") ->   ($#v13_vectsp_1 :::"additive"::: )   ; 
end; registrationlet "K" be  ($#~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"::: )     ($#v1_vectsp_1 :::"right-distributive"::: )     ($#l6_algstr_0 :::"doubleLoopStr"::: )  ; let "V" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_vectsp_1 :::"VectSpStr"::: )   "over" (Set (Const "K")); let "f" be   ($#v13_vectsp_1 :::"additive"::: )    ($#m1_subset_1 :::"Functional":::) "of" (Set (Const "V")); 
cluster (Set   ($#k4_hahnban1 :::"-"::: )  "f") ->   ($#v13_vectsp_1 :::"additive"::: )   ; 
end; registrationlet "K" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v13_algstr_0 :::"right_complementable"::: )     ($#v3_rlvect_1 :::"add-associative"::: )     ($#v4_rlvect_1 :::"right_zeroed"::: )     ($#v1_vectsp_1 :::"right-distributive"::: )     ($#l6_algstr_0 :::"doubleLoopStr"::: )  ; let "V" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_vectsp_1 :::"VectSpStr"::: )   "over" (Set (Const "K")); let "v" be   ($#m1_subset_1 :::"Element":::) "of" (Set (Const "K")); let "f" be   ($#v13_vectsp_1 :::"additive"::: )    ($#m1_subset_1 :::"Functional":::) "of" (Set (Const "V")); 
cluster (Set "v"  ($#k6_hahnban1 :::"*"::: )  "f") ->   ($#v13_vectsp_1 :::"additive"::: )   ; 
end; registrationlet "K" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v13_algstr_0 :::"right_complementable"::: )     ($#v3_rlvect_1 :::"add-associative"::: )     ($#v4_rlvect_1 :::"right_zeroed"::: )     ($#v1_vectsp_1 :::"right-distributive"::: )     ($#l6_algstr_0 :::"doubleLoopStr"::: )  ; let "V" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_vectsp_1 :::"VectSpStr"::: )   "over" (Set (Const "K")); let "f", "g" be   ($#v1_hahnban1 :::"homogeneous"::: )    ($#m1_subset_1 :::"Functional":::) "of" (Set (Const "V")); 
cluster (Set "f"  ($#k3_hahnban1 :::"+"::: )  "g") ->   ($#v1_hahnban1 :::"homogeneous"::: )   ; 
end; registrationlet "K" be  ($#~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"::: )     ($#v1_vectsp_1 :::"right-distributive"::: )     ($#l6_algstr_0 :::"doubleLoopStr"::: )  ; let "V" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_vectsp_1 :::"VectSpStr"::: )   "over" (Set (Const "K")); let "f" be   ($#v1_hahnban1 :::"homogeneous"::: )    ($#m1_subset_1 :::"Functional":::) "of" (Set (Const "V")); 
cluster (Set   ($#k4_hahnban1 :::"-"::: )  "f") ->   ($#v1_hahnban1 :::"homogeneous"::: )   ; 
end; registrationlet "K" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v13_algstr_0 :::"right_complementable"::: )     ($#v3_rlvect_1 :::"add-associative"::: )     ($#v4_rlvect_1 :::"right_zeroed"::: )     ($#v3_group_1 :::"associative"::: )     ($#v5_group_1 :::"commutative"::: )     ($#v1_vectsp_1 :::"right-distributive"::: )     ($#l6_algstr_0 :::"doubleLoopStr"::: )  ; let "V" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_vectsp_1 :::"VectSpStr"::: )   "over" (Set (Const "K")); let "v" be   ($#m1_subset_1 :::"Element":::) "of" (Set (Const "K")); let "f" be   ($#v1_hahnban1 :::"homogeneous"::: )    ($#m1_subset_1 :::"Functional":::) "of" (Set (Const "V")); 
cluster (Set "v"  ($#k6_hahnban1 :::"*"::: )  "f") ->   ($#v1_hahnban1 :::"homogeneous"::: )   ; 
end; definitionlet "K" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v13_algstr_0 :::"right_complementable"::: )     ($#v3_rlvect_1 :::"add-associative"::: )     ($#v4_rlvect_1 :::"right_zeroed"::: )     ($#v1_vectsp_1 :::"right-distributive"::: )     ($#l6_algstr_0 :::"doubleLoopStr"::: )  ; let "V" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_vectsp_1 :::"VectSpStr"::: )   "over" (Set (Const "K")); mode linear-Functional of "V" is   ($#v13_vectsp_1 :::"additive"::: )     ($#v1_hahnban1 :::"homogeneous"::: )    ($#m1_subset_1 :::"Functional":::) "of" "V"; end; begin  definitionlet "K" be  ($#~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"::: )     ($#v3_group_1 :::"associative"::: )     ($#v5_group_1 :::"commutative"::: )     ($#v1_vectsp_1 :::"right-distributive"::: )     ($#l6_algstr_0 :::"doubleLoopStr"::: )  ; let "V" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_vectsp_1 :::"VectSpStr"::: )   "over" (Set (Const "K")); func "V" :::"*'":::  ->  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v7_vectsp_1 :::"strict"::: )     ($#l1_vectsp_1 :::"VectSpStr"::: )   "over" "K" means :: HAHNBAN1:def 10 (Bool  "("  (Bool  "("   "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" it)) "iff" (Bool (Set (Var "x")) "is"   ($#m1_subset_1 :::"linear-Functional":::) "of" "V")  ")" )  ")" ) & (Bool  "("   "for" (Set (Var "f")) "," (Set (Var "g")) "being"   ($#m1_subset_1 :::"linear-Functional":::) "of" "V" "holds"  (Bool (Set (Set  "the"  ($#u1_algstr_0 :::"addF"::: )  "of" it)  ($#k1_binop_1 :::"."::: )   "(" (Set (Var "f")) "," (Set (Var "g")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set (Var "f"))  ($#k3_hahnban1 :::"+"::: )  (Set (Var "g"))))  ")" ) & (Bool (Set   ($#k4_struct_0 :::"0."::: )  it)  ($#r1_hidden :::"="::: )  (Set   ($#k7_hahnban1 :::"0Functional"::: )  "V")) & (Bool  "("   "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"linear-Functional":::) "of" "V"  (Bool  "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Element":::) "of" "K" "holds"  (Bool (Set (Set  "the"  ($#u1_vectsp_1 :::"lmult"::: )  "of" it)  ($#k1_binop_1 :::"."::: )   "(" (Set (Var "x")) "," (Set (Var "f")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set (Var "x"))  ($#k6_hahnban1 :::"*"::: )  (Set (Var "f")))))  ")" )  ")" ); end; 






:: deftheorem    defines :::"*'"::: HAHNBAN1:def 10 :  (Bool  "for" (Set (Var "K")) "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"::: )     ($#v3_group_1 :::"associative"::: )     ($#v5_group_1 :::"commutative"::: )     ($#v1_vectsp_1 :::"right-distributive"::: )     ($#l6_algstr_0 :::"doubleLoopStr"::: )    (Bool  "for" (Set (Var "V")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_vectsp_1 :::"VectSpStr"::: )   "over" (Set (Var "K"))  (Bool  "for" (Set (Var "b3")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v7_vectsp_1 :::"strict"::: )     ($#l1_vectsp_1 :::"VectSpStr"::: )   "over" (Set (Var "K")) "holds"   (Bool  "("  (Bool (Set (Var "b3"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "V"))  ($#k8_hahnban1 :::"*'"::: )  )) "iff" (Bool  "("  (Bool  "("   "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "b3")))) "iff" (Bool (Set (Var "x")) "is"   ($#m1_subset_1 :::"linear-Functional":::) "of" (Set (Var "V")))  ")" )  ")" ) & (Bool  "("   "for" (Set (Var "f")) "," (Set (Var "g")) "being"   ($#m1_subset_1 :::"linear-Functional":::) "of" (Set (Var "V")) "holds"  (Bool (Set (Set  "the"  ($#u1_algstr_0 :::"addF"::: )  "of" (Set (Var "b3")))  ($#k1_binop_1 :::"."::: )   "(" (Set (Var "f")) "," (Set (Var "g")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set (Var "f"))  ($#k3_hahnban1 :::"+"::: )  (Set (Var "g"))))  ")" ) & (Bool (Set   ($#k4_struct_0 :::"0."::: )  (Set (Var "b3")))  ($#r1_hidden :::"="::: )  (Set   ($#k7_hahnban1 :::"0Functional"::: )  (Set (Var "V")))) & (Bool  "("   "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"linear-Functional":::) "of" (Set (Var "V"))  (Bool  "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "K")) "holds"  (Bool (Set (Set  "the"  ($#u1_vectsp_1 :::"lmult"::: )  "of" (Set (Var "b3")))  ($#k1_binop_1 :::"."::: )   "(" (Set (Var "x")) "," (Set (Var "f")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set (Var "x"))  ($#k6_hahnban1 :::"*"::: )  (Set (Var "f")))))  ")" )  ")" )  ")" )))); 
 registrationlet "K" be  ($#~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"::: )     ($#v3_group_1 :::"associative"::: )     ($#v5_group_1 :::"commutative"::: )     ($#v1_vectsp_1 :::"right-distributive"::: )     ($#l6_algstr_0 :::"doubleLoopStr"::: )  ; let "V" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_vectsp_1 :::"VectSpStr"::: )   "over" (Set (Const "K")); 
cluster (Set "V"  ($#k8_hahnban1 :::"*'"::: )  ) ->  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v2_rlvect_1 :::"Abelian"::: )     ($#v7_vectsp_1 :::"strict"::: )   ; 
end; registrationlet "K" be  ($#~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"::: )     ($#v3_group_1 :::"associative"::: )     ($#v5_group_1 :::"commutative"::: )     ($#v1_vectsp_1 :::"right-distributive"::: )     ($#l6_algstr_0 :::"doubleLoopStr"::: )  ; let "V" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_vectsp_1 :::"VectSpStr"::: )   "over" (Set (Const "K")); 
cluster (Set "V"  ($#k8_hahnban1 :::"*'"::: )  ) ->  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v3_rlvect_1 :::"add-associative"::: )     ($#v7_vectsp_1 :::"strict"::: )   ; 

cluster (Set "V"  ($#k8_hahnban1 :::"*'"::: )  ) ->  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v4_rlvect_1 :::"right_zeroed"::: )     ($#v7_vectsp_1 :::"strict"::: )   ; 

cluster (Set "V"  ($#k8_hahnban1 :::"*'"::: )  ) ->  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v13_algstr_0 :::"right_complementable"::: )     ($#v7_vectsp_1 :::"strict"::: )   ; 
end; registrationlet "K" be  ($#~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"::: )     ($#v3_group_1 :::"associative"::: )     ($#v5_group_1 :::"commutative"::: )     ($#v5_vectsp_1 :::"distributive"::: )     ($#v6_vectsp_1 :::"left_unital"::: )     ($#l6_algstr_0 :::"doubleLoopStr"::: )  ; let "V" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_vectsp_1 :::"VectSpStr"::: )   "over" (Set (Const "K")); 
cluster (Set "V"  ($#k8_hahnban1 :::"*'"::: )  ) ->  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v7_vectsp_1 :::"strict"::: )     ($#v8_vectsp_1 :::"vector-distributive"::: )     ($#v9_vectsp_1 :::"scalar-distributive"::: )     ($#v10_vectsp_1 :::"scalar-associative"::: )     ($#v11_vectsp_1 :::"scalar-unital"::: )   ; 
end; begin  definitionlet "K" be    ($#l1_struct_0 :::"1-sorted"::: )  ; let "V" be    ($#l1_vectsp_1 :::"VectSpStr"::: )   "over" (Set (Const "K")); mode RFunctional of "V" is   ($#m1_subset_1 :::"Function":::) "of" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "V") "," (Set  ($#k1_numbers :::"REAL"::: ) ); end; definitionlet "K" be    ($#l1_struct_0 :::"1-sorted"::: )  ; let "V" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_vectsp_1 :::"VectSpStr"::: )   "over" (Set (Const "K")); let "F" be   ($#m1_subset_1 :::"RFunctional":::) "of" (Set (Const "V")); attr "F" is  :::"subadditive":::  means :: HAHNBAN1:def 11 (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#m1_subset_1 :::"Vector":::) "of" "V" "holds"  (Bool (Set "F"  ($#k3_funct_2 :::"."::: )  (Set  "(" (Set (Var "x"))  ($#k1_algstr_0 :::"+"::: )  (Set (Var "y")) ")" ))  ($#r1_xxreal_0 :::"<="::: )  (Set (Set  "(" "F"  ($#k3_funct_2 :::"."::: )  (Set (Var "x")) ")" )  ($#k7_real_1 :::"+"::: )  (Set  "(" "F"  ($#k3_funct_2 :::"."::: )  (Set (Var "y")) ")" )))); end; 






:: deftheorem    defines :::"subadditive"::: HAHNBAN1:def 11 :  (Bool  "for" (Set (Var "K")) "being"    ($#l1_struct_0 :::"1-sorted"::: )    (Bool  "for" (Set (Var "V")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_vectsp_1 :::"VectSpStr"::: )   "over" (Set (Var "K"))  (Bool  "for" (Set (Var "F")) "being"   ($#m1_subset_1 :::"RFunctional":::) "of" (Set (Var "V")) "holds"   (Bool  "("  (Bool (Set (Var "F")) "is"   ($#v3_hahnban1 :::"subadditive"::: )  ) "iff" (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#m1_subset_1 :::"Vector":::) "of" (Set (Var "V")) "holds"  (Bool (Set (Set (Var "F"))  ($#k3_funct_2 :::"."::: )  (Set  "(" (Set (Var "x"))  ($#k1_algstr_0 :::"+"::: )  (Set (Var "y")) ")" ))  ($#r1_xxreal_0 :::"<="::: )  (Set (Set  "(" (Set (Var "F"))  ($#k3_funct_2 :::"."::: )  (Set (Var "x")) ")" )  ($#k7_real_1 :::"+"::: )  (Set  "(" (Set (Var "F"))  ($#k3_funct_2 :::"."::: )  (Set (Var "y")) ")" ))))  ")" )))); 
 definitionlet "K" be    ($#l1_struct_0 :::"1-sorted"::: )  ; let "V" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_vectsp_1 :::"VectSpStr"::: )   "over" (Set (Const "K")); let "F" be   ($#m1_subset_1 :::"RFunctional":::) "of" (Set (Const "V")); attr "F" is  :::"additive":::  means :: HAHNBAN1:def 12 (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#m1_subset_1 :::"Vector":::) "of" "V" "holds"  (Bool (Set "F"  ($#k3_funct_2 :::"."::: )  (Set  "(" (Set (Var "x"))  ($#k1_algstr_0 :::"+"::: )  (Set (Var "y")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" "F"  ($#k3_funct_2 :::"."::: )  (Set (Var "x")) ")" )  ($#k7_real_1 :::"+"::: )  (Set  "(" "F"  ($#k3_funct_2 :::"."::: )  (Set (Var "y")) ")" )))); end; 






:: deftheorem    defines :::"additive"::: HAHNBAN1:def 12 :  (Bool  "for" (Set (Var "K")) "being"    ($#l1_struct_0 :::"1-sorted"::: )    (Bool  "for" (Set (Var "V")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_vectsp_1 :::"VectSpStr"::: )   "over" (Set (Var "K"))  (Bool  "for" (Set (Var "F")) "being"   ($#m1_subset_1 :::"RFunctional":::) "of" (Set (Var "V")) "holds"   (Bool  "("  (Bool (Set (Var "F")) "is"   ($#v4_hahnban1 :::"additive"::: )  ) "iff" (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#m1_subset_1 :::"Vector":::) "of" (Set (Var "V")) "holds"  (Bool (Set (Set (Var "F"))  ($#k3_funct_2 :::"."::: )  (Set  "(" (Set (Var "x"))  ($#k1_algstr_0 :::"+"::: )  (Set (Var "y")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "F"))  ($#k3_funct_2 :::"."::: )  (Set (Var "x")) ")" )  ($#k7_real_1 :::"+"::: )  (Set  "(" (Set (Var "F"))  ($#k3_funct_2 :::"."::: )  (Set (Var "y")) ")" ))))  ")" )))); 
 definitionlet "V" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_vectsp_1 :::"VectSpStr"::: )   "over" (Set   ($#k1_complfld :::"F_Complex"::: )  ); let "F" be   ($#m1_subset_1 :::"RFunctional":::) "of" (Set (Const "V")); attr "F" is  :::"Real_homogeneous":::  means :: HAHNBAN1:def 13 (Bool  "for" (Set (Var "v")) "being"   ($#m1_subset_1 :::"Vector":::) "of" "V"  (Bool  "for" (Set (Var "r")) "being"   ($#m1_subset_1 :::"Real":::) "holds"  (Bool (Set "F"  ($#k3_funct_2 :::"."::: )  (Set  "(" (Set  ($#k1_hahnban1 :::"[**"::: ) (Set (Var "r")) "," (Set  ($#k6_numbers :::"0"::: ) ) ($#k1_hahnban1 :::"**]"::: ) )  ($#k4_vectsp_1 :::"*"::: )  (Set (Var "v")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "r"))  ($#k8_real_1 :::"*"::: )  (Set  "(" "F"  ($#k3_funct_2 :::"."::: )  (Set (Var "v")) ")" ))))); end; 





:: deftheorem    defines :::"Real_homogeneous"::: HAHNBAN1:def 13 :  (Bool  "for" (Set (Var "V")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_vectsp_1 :::"VectSpStr"::: )   "over" (Set   ($#k1_complfld :::"F_Complex"::: )  )  (Bool  "for" (Set (Var "F")) "being"   ($#m1_subset_1 :::"RFunctional":::) "of" (Set (Var "V")) "holds"   (Bool  "("  (Bool (Set (Var "F")) "is"   ($#v5_hahnban1 :::"Real_homogeneous"::: )  ) "iff" (Bool  "for" (Set (Var "v")) "being"   ($#m1_subset_1 :::"Vector":::) "of" (Set (Var "V"))  (Bool  "for" (Set (Var "r")) "being"   ($#m1_subset_1 :::"Real":::) "holds"  (Bool (Set (Set (Var "F"))  ($#k3_funct_2 :::"."::: )  (Set  "(" (Set  ($#k1_hahnban1 :::"[**"::: ) (Set (Var "r")) "," (Set  ($#k6_numbers :::"0"::: ) ) ($#k1_hahnban1 :::"**]"::: ) )  ($#k4_vectsp_1 :::"*"::: )  (Set (Var "v")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "r"))  ($#k8_real_1 :::"*"::: )  (Set  "(" (Set (Var "F"))  ($#k3_funct_2 :::"."::: )  (Set (Var "v")) ")" )))))  ")" ))); 
 
theorem :: HAHNBAN1:21 (Bool  "for" (Set (Var "V")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v8_vectsp_1 :::"vector-distributive"::: )     ($#v9_vectsp_1 :::"scalar-distributive"::: )     ($#v10_vectsp_1 :::"scalar-associative"::: )     ($#v11_vectsp_1 :::"scalar-unital"::: )     ($#l1_vectsp_1 :::"VectSpStr"::: )   "over" (Set   ($#k1_complfld :::"F_Complex"::: )  )  (Bool  "for" (Set (Var "F")) "being"   ($#m1_subset_1 :::"RFunctional":::) "of" (Set (Var "V"))  "st" (Bool (Bool (Set (Var "F")) "is"   ($#v5_hahnban1 :::"Real_homogeneous"::: )  )) "holds"  (Bool  "for" (Set (Var "v")) "being"   ($#m1_subset_1 :::"Vector":::) "of" (Set (Var "V"))  (Bool  "for" (Set (Var "r")) "being"   ($#m1_subset_1 :::"Real":::) "holds"  (Bool (Set (Set (Var "F"))  ($#k3_funct_2 :::"."::: )  (Set  "(" (Set  ($#k1_hahnban1 :::"[**"::: ) (Set  ($#k6_numbers :::"0"::: ) ) "," (Set (Var "r")) ($#k1_hahnban1 :::"**]"::: ) )  ($#k4_vectsp_1 :::"*"::: )  (Set (Var "v")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "r"))  ($#k8_real_1 :::"*"::: )  (Set  "(" (Set (Var "F"))  ($#k3_funct_2 :::"."::: )  (Set  "(" (Set  ($#k2_hahnban1 :::"i_FC"::: ) )  ($#k4_vectsp_1 :::"*"::: )  (Set (Var "v")) ")" ) ")" ))))))) ; 
 definitionlet "V" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_vectsp_1 :::"VectSpStr"::: )   "over" (Set   ($#k1_complfld :::"F_Complex"::: )  ); let "F" be   ($#m1_subset_1 :::"RFunctional":::) "of" (Set (Const "V")); attr "F" is  :::"homogeneous":::  means :: HAHNBAN1:def 14 (Bool  "for" (Set (Var "v")) "being"   ($#m1_subset_1 :::"Vector":::) "of" "V"  (Bool  "for" (Set (Var "r")) "being"   ($#m1_subset_1 :::"Scalar":::) "of"  "holds"  (Bool (Set "F"  ($#k3_funct_2 :::"."::: )  (Set  "(" (Set (Var "r"))  ($#k4_vectsp_1 :::"*"::: )  (Set (Var "v")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  ($#k17_complex1 :::"|."::: ) (Set (Var "r")) ($#k17_complex1 :::".|"::: ) )  ($#k8_real_1 :::"*"::: )  (Set  "(" "F"  ($#k3_funct_2 :::"."::: )  (Set (Var "v")) ")" ))))); end; 





:: deftheorem    defines :::"homogeneous"::: HAHNBAN1:def 14 :  (Bool  "for" (Set (Var "V")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_vectsp_1 :::"VectSpStr"::: )   "over" (Set   ($#k1_complfld :::"F_Complex"::: )  )  (Bool  "for" (Set (Var "F")) "being"   ($#m1_subset_1 :::"RFunctional":::) "of" (Set (Var "V")) "holds"   (Bool  "("  (Bool (Set (Var "F")) "is"   ($#v6_hahnban1 :::"homogeneous"::: )  ) "iff" (Bool  "for" (Set (Var "v")) "being"   ($#m1_subset_1 :::"Vector":::) "of" (Set (Var "V"))  (Bool  "for" (Set (Var "r")) "being"   ($#m1_subset_1 :::"Scalar":::) "of"  "holds"  (Bool (Set (Set (Var "F"))  ($#k3_funct_2 :::"."::: )  (Set  "(" (Set (Var "r"))  ($#k4_vectsp_1 :::"*"::: )  (Set (Var "v")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  ($#k17_complex1 :::"|."::: ) (Set (Var "r")) ($#k17_complex1 :::".|"::: ) )  ($#k8_real_1 :::"*"::: )  (Set  "(" (Set (Var "F"))  ($#k3_funct_2 :::"."::: )  (Set (Var "v")) ")" )))))  ")" ))); 
 definitionlet "K" be    ($#l1_struct_0 :::"1-sorted"::: )  ; let "V" be    ($#l1_vectsp_1 :::"VectSpStr"::: )   "over" (Set (Const "K")); let "F" be   ($#m1_subset_1 :::"RFunctional":::) "of" (Set (Const "V")); attr "F" is  :::"0-preserving":::  means :: HAHNBAN1:def 15 (Bool (Set "F"  ($#k1_funct_1 :::"."::: )  (Set  "("  ($#k4_struct_0 :::"0."::: )  "V" ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  )); end; 






:: deftheorem    defines :::"0-preserving"::: HAHNBAN1:def 15 :  (Bool  "for" (Set (Var "K")) "being"    ($#l1_struct_0 :::"1-sorted"::: )    (Bool  "for" (Set (Var "V")) "being"    ($#l1_vectsp_1 :::"VectSpStr"::: )   "over" (Set (Var "K"))  (Bool  "for" (Set (Var "F")) "being"   ($#m1_subset_1 :::"RFunctional":::) "of" (Set (Var "V")) "holds"   (Bool  "("  (Bool (Set (Var "F")) "is"   ($#v7_hahnban1 :::"0-preserving"::: )  ) "iff" (Bool (Set (Set (Var "F"))  ($#k1_funct_1 :::"."::: )  (Set  "("  ($#k4_struct_0 :::"0."::: )  (Set (Var "V")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")" )))); 
 registrationlet "K" be    ($#l1_struct_0 :::"1-sorted"::: )  ; let "V" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_vectsp_1 :::"VectSpStr"::: )   "over" (Set (Const "K")); 
cluster   ($#v1_funct_1 :::"Function-like"::: )   bbbadV1_FUNCT_2((Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "V") "," (Set   ($#k1_numbers :::"REAL"::: )  ))   ($#v4_hahnban1 :::"additive"::: )    ->   ($#v3_hahnban1 :::"subadditive"::: )    for    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k1_zfmisc_1 :::"bool"::: )  (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "V") "," (Set  ($#k1_numbers :::"REAL"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) )); 
end; registrationlet "V" be   ($#l1_vectsp_1 :::"VectSp":::) "of" (Set   ($#k1_complfld :::"F_Complex"::: )  ); 
cluster   ($#v1_funct_1 :::"Function-like"::: )   bbbadV1_FUNCT_2((Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "V") "," (Set   ($#k1_numbers :::"REAL"::: )  ))   ($#v5_hahnban1 :::"Real_homogeneous"::: )    ->   ($#v7_hahnban1 :::"0-preserving"::: )    for    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k1_zfmisc_1 :::"bool"::: )  (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "V") "," (Set  ($#k1_numbers :::"REAL"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) )); 
end; definitionlet "K" be    ($#l1_struct_0 :::"1-sorted"::: )  ; let "V" be    ($#l1_vectsp_1 :::"VectSpStr"::: )   "over" (Set (Const "K")); func  :::"0RFunctional"::: "V" ->   ($#m1_subset_1 :::"RFunctional":::) "of" "V" equals :: HAHNBAN1:def 16 (Set (Set  "("  ($#k2_struct_0 :::"[#]"::: )  "V" ")" )  ($#k8_funcop_1 :::"-->"::: )  (Set  ($#k6_numbers :::"0"::: ) )); end; 






:: deftheorem    defines :::"0RFunctional"::: HAHNBAN1:def 16 :  (Bool  "for" (Set (Var "K")) "being"    ($#l1_struct_0 :::"1-sorted"::: )    (Bool  "for" (Set (Var "V")) "being"    ($#l1_vectsp_1 :::"VectSpStr"::: )   "over" (Set (Var "K")) "holds"  (Bool (Set   ($#k9_hahnban1 :::"0RFunctional"::: )  (Set (Var "V")))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k2_struct_0 :::"[#]"::: )  (Set (Var "V")) ")" )  ($#k8_funcop_1 :::"-->"::: )  (Set  ($#k6_numbers :::"0"::: ) ))))); 
 registrationlet "K" be    ($#l1_struct_0 :::"1-sorted"::: )  ; let "V" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_vectsp_1 :::"VectSpStr"::: )   "over" (Set (Const "K")); 
cluster (Set   ($#k9_hahnban1 :::"0RFunctional"::: )  "V") ->   ($#v4_hahnban1 :::"additive"::: )   ; 

cluster (Set   ($#k9_hahnban1 :::"0RFunctional"::: )  "V") ->   ($#v7_hahnban1 :::"0-preserving"::: )   ; 
end; registrationlet "V" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_vectsp_1 :::"VectSpStr"::: )   "over" (Set   ($#k1_complfld :::"F_Complex"::: )  ); 
cluster (Set   ($#k9_hahnban1 :::"0RFunctional"::: )  "V") ->   ($#v5_hahnban1 :::"Real_homogeneous"::: )   ; 

cluster (Set   ($#k9_hahnban1 :::"0RFunctional"::: )  "V") ->   ($#v6_hahnban1 :::"homogeneous"::: )   ; 
end; registrationlet "K" be    ($#l1_struct_0 :::"1-sorted"::: )  ; let "V" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_vectsp_1 :::"VectSpStr"::: )   "over" (Set (Const "K")); 
cluster bbbadV1_RELAT_1() bbbadV4_RELAT_1((Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "V")) bbbadV5_RELAT_1((Set   ($#k1_numbers :::"REAL"::: )  ))   ($#v1_funct_1 :::"Function-like"::: )   bbbadV1_FUNCT_2((Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "V") "," (Set   ($#k1_numbers :::"REAL"::: )  ))   ($#v4_hahnban1 :::"additive"::: )     ($#v7_hahnban1 :::"0-preserving"::: )    for    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k1_zfmisc_1 :::"bool"::: )  (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "V") "," (Set  ($#k1_numbers :::"REAL"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) )); 
end; registrationlet "V" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_vectsp_1 :::"VectSpStr"::: )   "over" (Set   ($#k1_complfld :::"F_Complex"::: )  ); 
cluster bbbadV1_RELAT_1() bbbadV4_RELAT_1((Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "V")) bbbadV5_RELAT_1((Set   ($#k1_numbers :::"REAL"::: )  ))   ($#v1_funct_1 :::"Function-like"::: )   bbbadV1_FUNCT_2((Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "V") "," (Set   ($#k1_numbers :::"REAL"::: )  ))   ($#v4_hahnban1 :::"additive"::: )     ($#v5_hahnban1 :::"Real_homogeneous"::: )     ($#v6_hahnban1 :::"homogeneous"::: )    for    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k1_zfmisc_1 :::"bool"::: )  (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "V") "," (Set  ($#k1_numbers :::"REAL"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) )); 
end; definitionlet "V" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_vectsp_1 :::"VectSpStr"::: )   "over" (Set   ($#k1_complfld :::"F_Complex"::: )  ); mode Semi-Norm of "V" is   ($#v3_hahnban1 :::"subadditive"::: )     ($#v6_hahnban1 :::"homogeneous"::: )    ($#m1_subset_1 :::"RFunctional":::) "of" "V"; end; begin  definitionlet "V" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_vectsp_1 :::"VectSpStr"::: )   "over" (Set   ($#k1_complfld :::"F_Complex"::: )  ); func  :::"RealVS"::: "V" ->   ($#v1_rlvect_1 :::"strict"::: )     ($#l1_rlvect_1 :::"RLSStruct"::: )   means :: HAHNBAN1:def 17 (Bool  "("  (Bool (Set   ($#g2_algstr_0 :::"addLoopStr"::: )  "(#"  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" it) "," (Set  "the"  ($#u1_algstr_0 :::"addF"::: )  "of" it) "," (Set  "the"  ($#u2_struct_0 :::"ZeroF"::: )  "of" it) "#)" )  ($#r1_hidden :::"="::: )  (Set   ($#g2_algstr_0 :::"addLoopStr"::: )  "(#"  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "V") "," (Set  "the"  ($#u1_algstr_0 :::"addF"::: )  "of" "V") "," (Set  "the"  ($#u2_struct_0 :::"ZeroF"::: )  "of" "V") "#)" )) & (Bool  "("   "for" (Set (Var "r")) "being"   ($#m1_subset_1 :::"Real":::)  (Bool  "for" (Set (Var "v")) "being"   ($#m1_subset_1 :::"Vector":::) "of" "V" "holds"  (Bool (Set (Set  "the"  ($#u1_rlvect_1 :::"Mult"::: )  "of" it)  ($#k1_binop_1 :::"."::: )   "(" (Set (Var "r")) "," (Set (Var "v")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set  ($#k1_hahnban1 :::"[**"::: ) (Set (Var "r")) "," (Set  ($#k6_numbers :::"0"::: ) ) ($#k1_hahnban1 :::"**]"::: ) )  ($#k4_vectsp_1 :::"*"::: )  (Set (Var "v")))))  ")" )  ")" ); end; 





:: deftheorem    defines :::"RealVS"::: HAHNBAN1:def 17 :  (Bool  "for" (Set (Var "V")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_vectsp_1 :::"VectSpStr"::: )   "over" (Set   ($#k1_complfld :::"F_Complex"::: )  )  (Bool  "for" (Set (Var "b2")) "being"   ($#v1_rlvect_1 :::"strict"::: )     ($#l1_rlvect_1 :::"RLSStruct"::: )   "holds"   (Bool  "("  (Bool (Set (Var "b2"))  ($#r1_hidden :::"="::: )  (Set   ($#k10_hahnban1 :::"RealVS"::: )  (Set (Var "V")))) "iff" (Bool  "("  (Bool (Set   ($#g2_algstr_0 :::"addLoopStr"::: )  "(#"  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "b2"))) "," (Set  "the"  ($#u1_algstr_0 :::"addF"::: )  "of" (Set (Var "b2"))) "," (Set  "the"  ($#u2_struct_0 :::"ZeroF"::: )  "of" (Set (Var "b2"))) "#)" )  ($#r1_hidden :::"="::: )  (Set   ($#g2_algstr_0 :::"addLoopStr"::: )  "(#"  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "V"))) "," (Set  "the"  ($#u1_algstr_0 :::"addF"::: )  "of" (Set (Var "V"))) "," (Set  "the"  ($#u2_struct_0 :::"ZeroF"::: )  "of" (Set (Var "V"))) "#)" )) & (Bool  "("   "for" (Set (Var "r")) "being"   ($#m1_subset_1 :::"Real":::)  (Bool  "for" (Set (Var "v")) "being"   ($#m1_subset_1 :::"Vector":::) "of" (Set (Var "V")) "holds"  (Bool (Set (Set  "the"  ($#u1_rlvect_1 :::"Mult"::: )  "of" (Set (Var "b2")))  ($#k1_binop_1 :::"."::: )   "(" (Set (Var "r")) "," (Set (Var "v")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set  ($#k1_hahnban1 :::"[**"::: ) (Set (Var "r")) "," (Set  ($#k6_numbers :::"0"::: ) ) ($#k1_hahnban1 :::"**]"::: ) )  ($#k4_vectsp_1 :::"*"::: )  (Set (Var "v")))))  ")" )  ")" )  ")" ))); 
 registrationlet "V" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_vectsp_1 :::"VectSpStr"::: )   "over" (Set   ($#k1_complfld :::"F_Complex"::: )  ); 
cluster (Set   ($#k10_hahnban1 :::"RealVS"::: )  "V") ->  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v1_rlvect_1 :::"strict"::: )   ; 
end; registrationlet "V" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v2_rlvect_1 :::"Abelian"::: )     ($#l1_vectsp_1 :::"VectSpStr"::: )   "over" (Set   ($#k1_complfld :::"F_Complex"::: )  ); 
cluster (Set   ($#k10_hahnban1 :::"RealVS"::: )  "V") ->   ($#v1_rlvect_1 :::"strict"::: )     ($#v2_rlvect_1 :::"Abelian"::: )   ; 
end; registrationlet "V" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v3_rlvect_1 :::"add-associative"::: )     ($#l1_vectsp_1 :::"VectSpStr"::: )   "over" (Set   ($#k1_complfld :::"F_Complex"::: )  ); 
cluster (Set   ($#k10_hahnban1 :::"RealVS"::: )  "V") ->   ($#v1_rlvect_1 :::"strict"::: )     ($#v3_rlvect_1 :::"add-associative"::: )   ; 
end; registrationlet "V" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v4_rlvect_1 :::"right_zeroed"::: )     ($#l1_vectsp_1 :::"VectSpStr"::: )   "over" (Set   ($#k1_complfld :::"F_Complex"::: )  ); 
cluster (Set   ($#k10_hahnban1 :::"RealVS"::: )  "V") ->   ($#v1_rlvect_1 :::"strict"::: )     ($#v4_rlvect_1 :::"right_zeroed"::: )   ; 
end; registrationlet "V" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v13_algstr_0 :::"right_complementable"::: )     ($#l1_vectsp_1 :::"VectSpStr"::: )   "over" (Set   ($#k1_complfld :::"F_Complex"::: )  ); 
cluster (Set   ($#k10_hahnban1 :::"RealVS"::: )  "V") ->   ($#v13_algstr_0 :::"right_complementable"::: )     ($#v1_rlvect_1 :::"strict"::: )   ; 
end; registrationlet "V" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v8_vectsp_1 :::"vector-distributive"::: )     ($#v9_vectsp_1 :::"scalar-distributive"::: )     ($#v10_vectsp_1 :::"scalar-associative"::: )     ($#v11_vectsp_1 :::"scalar-unital"::: )     ($#l1_vectsp_1 :::"VectSpStr"::: )   "over" (Set   ($#k1_complfld :::"F_Complex"::: )  ); 
cluster (Set   ($#k10_hahnban1 :::"RealVS"::: )  "V") ->   ($#v1_rlvect_1 :::"strict"::: )     ($#v5_rlvect_1 :::"vector-distributive"::: )     ($#v6_rlvect_1 :::"scalar-distributive"::: )     ($#v7_rlvect_1 :::"scalar-associative"::: )     ($#v8_rlvect_1 :::"scalar-unital"::: )   ; 
end; 
theorem :: HAHNBAN1:22 (Bool  "for" (Set (Var "V")) "being"   ($#l1_vectsp_1 :::"VectSp":::) "of" (Set   ($#k1_complfld :::"F_Complex"::: )  )  (Bool  "for" (Set (Var "M")) "being"    ($#m1_vectsp_4 :::"Subspace"::: )   "of" (Set (Var "V")) "holds"  (Bool (Set   ($#k10_hahnban1 :::"RealVS"::: )  (Set (Var "M"))) "is"    ($#m1_rlsub_1 :::"Subspace"::: )   "of" (Set   ($#k10_hahnban1 :::"RealVS"::: )  (Set (Var "V")))))) ; 
 
theorem :: HAHNBAN1:23 (Bool  "for" (Set (Var "V")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_vectsp_1 :::"VectSpStr"::: )   "over" (Set   ($#k1_complfld :::"F_Complex"::: )  )  (Bool  "for" (Set (Var "p")) "being"   ($#m1_subset_1 :::"RFunctional":::) "of" (Set (Var "V")) "holds"  (Bool (Set (Var "p")) "is"   ($#m1_subset_1 :::"Functional":::) "of" (Set  "("  ($#k10_hahnban1 :::"RealVS"::: )  (Set (Var "V")) ")" )))) ; 
 
theorem :: HAHNBAN1:24 (Bool  "for" (Set (Var "V")) "being"   ($#l1_vectsp_1 :::"VectSp":::) "of" (Set   ($#k1_complfld :::"F_Complex"::: )  )  (Bool  "for" (Set (Var "p")) "being"   ($#m1_subset_1 :::"Semi-Norm":::) "of" (Set (Var "V")) "holds"  (Bool (Set (Var "p")) "is"   ($#m1_subset_1 :::"Banach-Functional":::) "of" (Set  "("  ($#k10_hahnban1 :::"RealVS"::: )  (Set (Var "V")) ")" )))) ; 
 definitionlet "V" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_vectsp_1 :::"VectSpStr"::: )   "over" (Set   ($#k1_complfld :::"F_Complex"::: )  ); let "l" be   ($#m1_subset_1 :::"Functional":::) "of" (Set (Const "V")); func  :::"projRe"::: "l" ->   ($#m1_subset_1 :::"Functional":::) "of" (Set  "("  ($#k10_hahnban1 :::"RealVS"::: )  "V" ")" ) means :: HAHNBAN1:def 18 (Bool  "for" (Set (Var "i")) "being"   ($#m1_subset_1 :::"Element":::) "of" "V" "holds"  (Bool (Set it  ($#k1_funct_1 :::"."::: )  (Set (Var "i")))  ($#r1_hidden :::"="::: )  (Set   ($#k3_complex1 :::"Re"::: )  (Set  "(" "l"  ($#k3_funct_2 :::"."::: )  (Set (Var "i")) ")" )))); end; 






:: deftheorem    defines :::"projRe"::: HAHNBAN1:def 18 :  (Bool  "for" (Set (Var "V")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_vectsp_1 :::"VectSpStr"::: )   "over" (Set   ($#k1_complfld :::"F_Complex"::: )  )  (Bool  "for" (Set (Var "l")) "being"   ($#m1_subset_1 :::"Functional":::) "of" (Set (Var "V"))  (Bool  "for" (Set (Var "b3")) "being"   ($#m1_subset_1 :::"Functional":::) "of" (Set  "("  ($#k10_hahnban1 :::"RealVS"::: )  (Set (Var "V")) ")" ) "holds"   (Bool  "("  (Bool (Set (Var "b3"))  ($#r1_hidden :::"="::: )  (Set   ($#k11_hahnban1 :::"projRe"::: )  (Set (Var "l")))) "iff" (Bool  "for" (Set (Var "i")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "V")) "holds"  (Bool (Set (Set (Var "b3"))  ($#k1_funct_1 :::"."::: )  (Set (Var "i")))  ($#r1_hidden :::"="::: )  (Set   ($#k3_complex1 :::"Re"::: )  (Set  "(" (Set (Var "l"))  ($#k3_funct_2 :::"."::: )  (Set (Var "i")) ")" ))))  ")" )))); 
 definitionlet "V" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_vectsp_1 :::"VectSpStr"::: )   "over" (Set   ($#k1_complfld :::"F_Complex"::: )  ); let "l" be   ($#m1_subset_1 :::"Functional":::) "of" (Set (Const "V")); func  :::"projIm"::: "l" ->   ($#m1_subset_1 :::"Functional":::) "of" (Set  "("  ($#k10_hahnban1 :::"RealVS"::: )  "V" ")" ) means :: HAHNBAN1:def 19 (Bool  "for" (Set (Var "i")) "being"   ($#m1_subset_1 :::"Element":::) "of" "V" "holds"  (Bool (Set it  ($#k1_funct_1 :::"."::: )  (Set (Var "i")))  ($#r1_hidden :::"="::: )  (Set   ($#k4_complex1 :::"Im"::: )  (Set  "(" "l"  ($#k3_funct_2 :::"."::: )  (Set (Var "i")) ")" )))); end; 






:: deftheorem    defines :::"projIm"::: HAHNBAN1:def 19 :  (Bool  "for" (Set (Var "V")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_vectsp_1 :::"VectSpStr"::: )   "over" (Set   ($#k1_complfld :::"F_Complex"::: )  )  (Bool  "for" (Set (Var "l")) "being"   ($#m1_subset_1 :::"Functional":::) "of" (Set (Var "V"))  (Bool  "for" (Set (Var "b3")) "being"   ($#m1_subset_1 :::"Functional":::) "of" (Set  "("  ($#k10_hahnban1 :::"RealVS"::: )  (Set (Var "V")) ")" ) "holds"   (Bool  "("  (Bool (Set (Var "b3"))  ($#r1_hidden :::"="::: )  (Set   ($#k12_hahnban1 :::"projIm"::: )  (Set (Var "l")))) "iff" (Bool  "for" (Set (Var "i")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "V")) "holds"  (Bool (Set (Set (Var "b3"))  ($#k1_funct_1 :::"."::: )  (Set (Var "i")))  ($#r1_hidden :::"="::: )  (Set   ($#k4_complex1 :::"Im"::: )  (Set  "(" (Set (Var "l"))  ($#k3_funct_2 :::"."::: )  (Set (Var "i")) ")" ))))  ")" )))); 
 definitionlet "V" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_vectsp_1 :::"VectSpStr"::: )   "over" (Set   ($#k1_complfld :::"F_Complex"::: )  ); let "l" be   ($#m1_subset_1 :::"Functional":::) "of" (Set  "("  ($#k10_hahnban1 :::"RealVS"::: )  (Set (Const "V")) ")" ); func  :::"RtoC"::: "l" ->   ($#m1_subset_1 :::"RFunctional":::) "of" "V" equals :: HAHNBAN1:def 20 "l"; end; 






:: deftheorem    defines :::"RtoC"::: HAHNBAN1:def 20 :  (Bool  "for" (Set (Var "V")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_vectsp_1 :::"VectSpStr"::: )   "over" (Set   ($#k1_complfld :::"F_Complex"::: )  )  (Bool  "for" (Set (Var "l")) "being"   ($#m1_subset_1 :::"Functional":::) "of" (Set  "("  ($#k10_hahnban1 :::"RealVS"::: )  (Set (Var "V")) ")" ) "holds"  (Bool (Set   ($#k13_hahnban1 :::"RtoC"::: )  (Set (Var "l")))  ($#r1_hidden :::"="::: )  (Set (Var "l"))))); 
 definitionlet "V" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_vectsp_1 :::"VectSpStr"::: )   "over" (Set   ($#k1_complfld :::"F_Complex"::: )  ); let "l" be   ($#m1_subset_1 :::"RFunctional":::) "of" (Set (Const "V")); func  :::"CtoR"::: "l" ->   ($#m1_subset_1 :::"Functional":::) "of" (Set  "("  ($#k10_hahnban1 :::"RealVS"::: )  "V" ")" ) equals :: HAHNBAN1:def 21 "l"; end; 






:: deftheorem    defines :::"CtoR"::: HAHNBAN1:def 21 :  (Bool  "for" (Set (Var "V")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_vectsp_1 :::"VectSpStr"::: )   "over" (Set   ($#k1_complfld :::"F_Complex"::: )  )  (Bool  "for" (Set (Var "l")) "being"   ($#m1_subset_1 :::"RFunctional":::) "of" (Set (Var "V")) "holds"  (Bool (Set   ($#k14_hahnban1 :::"CtoR"::: )  (Set (Var "l")))  ($#r1_hidden :::"="::: )  (Set (Var "l"))))); 
 registrationlet "V" be   ($#l1_vectsp_1 :::"VectSp":::) "of" (Set   ($#k1_complfld :::"F_Complex"::: )  ); let "l" be   ($#v2_hahnban :::"additive"::: )    ($#m1_subset_1 :::"Functional":::) "of" (Set  "("  ($#k10_hahnban1 :::"RealVS"::: )  (Set (Const "V")) ")" ); 
cluster (Set   ($#k13_hahnban1 :::"RtoC"::: )  "l") ->   ($#v4_hahnban1 :::"additive"::: )   ; 
end; registrationlet "V" be   ($#l1_vectsp_1 :::"VectSp":::) "of" (Set   ($#k1_complfld :::"F_Complex"::: )  ); let "l" be   ($#v4_hahnban1 :::"additive"::: )    ($#m1_subset_1 :::"RFunctional":::) "of" (Set (Const "V")); 
cluster (Set   ($#k14_hahnban1 :::"CtoR"::: )  "l") ->   ($#v2_hahnban :::"additive"::: )   ; 
end; registrationlet "V" be   ($#l1_vectsp_1 :::"VectSp":::) "of" (Set   ($#k1_complfld :::"F_Complex"::: )  ); let "l" be   ($#v3_hahnban :::"homogeneous"::: )    ($#m1_subset_1 :::"Functional":::) "of" (Set  "("  ($#k10_hahnban1 :::"RealVS"::: )  (Set (Const "V")) ")" ); 
cluster (Set   ($#k13_hahnban1 :::"RtoC"::: )  "l") ->   ($#v5_hahnban1 :::"Real_homogeneous"::: )   ; 
end; registrationlet "V" be   ($#l1_vectsp_1 :::"VectSp":::) "of" (Set   ($#k1_complfld :::"F_Complex"::: )  ); let "l" be   ($#v5_hahnban1 :::"Real_homogeneous"::: )    ($#m1_subset_1 :::"RFunctional":::) "of" (Set (Const "V")); 
cluster (Set   ($#k14_hahnban1 :::"CtoR"::: )  "l") ->   ($#v3_hahnban :::"homogeneous"::: )   ; 
end; definitionlet "V" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_vectsp_1 :::"VectSpStr"::: )   "over" (Set   ($#k1_complfld :::"F_Complex"::: )  ); let "l" be   ($#m1_subset_1 :::"RFunctional":::) "of" (Set (Const "V")); func  :::"i-shift"::: "l" ->   ($#m1_subset_1 :::"RFunctional":::) "of" "V" means :: HAHNBAN1:def 22 (Bool  "for" (Set (Var "v")) "being"   ($#m1_subset_1 :::"Element":::) "of" "V" "holds"  (Bool (Set it  ($#k3_funct_2 :::"."::: )  (Set (Var "v")))  ($#r1_hidden :::"="::: )  (Set "l"  ($#k3_funct_2 :::"."::: )  (Set  "(" (Set  ($#k2_hahnban1 :::"i_FC"::: ) )  ($#k4_vectsp_1 :::"*"::: )  (Set (Var "v")) ")" )))); end; 






:: deftheorem    defines :::"i-shift"::: HAHNBAN1:def 22 :  (Bool  "for" (Set (Var "V")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_vectsp_1 :::"VectSpStr"::: )   "over" (Set   ($#k1_complfld :::"F_Complex"::: )  )  (Bool  "for" (Set (Var "l")) "," (Set (Var "b3")) "being"   ($#m1_subset_1 :::"RFunctional":::) "of" (Set (Var "V")) "holds"   (Bool  "("  (Bool (Set (Var "b3"))  ($#r1_hidden :::"="::: )  (Set   ($#k15_hahnban1 :::"i-shift"::: )  (Set (Var "l")))) "iff" (Bool  "for" (Set (Var "v")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "V")) "holds"  (Bool (Set (Set (Var "b3"))  ($#k3_funct_2 :::"."::: )  (Set (Var "v")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "l"))  ($#k3_funct_2 :::"."::: )  (Set  "(" (Set  ($#k2_hahnban1 :::"i_FC"::: ) )  ($#k4_vectsp_1 :::"*"::: )  (Set (Var "v")) ")" ))))  ")" ))); 
 definitionlet "V" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_vectsp_1 :::"VectSpStr"::: )   "over" (Set   ($#k1_complfld :::"F_Complex"::: )  ); let "l" be   ($#m1_subset_1 :::"Functional":::) "of" (Set  "("  ($#k10_hahnban1 :::"RealVS"::: )  (Set (Const "V")) ")" ); func  :::"prodReIm"::: "l" ->   ($#m1_subset_1 :::"Functional":::) "of" "V" means :: HAHNBAN1:def 23 (Bool  "for" (Set (Var "v")) "being"   ($#m1_subset_1 :::"Element":::) "of" "V" "holds"  (Bool (Set it  ($#k3_funct_2 :::"."::: )  (Set (Var "v")))  ($#r1_hidden :::"="::: )  (Set  ($#k1_hahnban1 :::"[**"::: ) (Set  "(" (Set  "("  ($#k13_hahnban1 :::"RtoC"::: )  "l" ")" )  ($#k3_funct_2 :::"."::: )  (Set (Var "v")) ")" ) "," (Set  "("  ($#k1_real_1 :::"-"::: )  (Set  "(" (Set  "("  ($#k15_hahnban1 :::"i-shift"::: )  (Set  "("  ($#k13_hahnban1 :::"RtoC"::: )  "l" ")" ) ")" )  ($#k3_funct_2 :::"."::: )  (Set (Var "v")) ")" ) ")" ) ($#k1_hahnban1 :::"**]"::: ) ))); end; 






:: deftheorem    defines :::"prodReIm"::: HAHNBAN1:def 23 :  (Bool  "for" (Set (Var "V")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_vectsp_1 :::"VectSpStr"::: )   "over" (Set   ($#k1_complfld :::"F_Complex"::: )  )  (Bool  "for" (Set (Var "l")) "being"   ($#m1_subset_1 :::"Functional":::) "of" (Set  "("  ($#k10_hahnban1 :::"RealVS"::: )  (Set (Var "V")) ")" )  (Bool  "for" (Set (Var "b3")) "being"   ($#m1_subset_1 :::"Functional":::) "of" (Set (Var "V")) "holds"   (Bool  "("  (Bool (Set (Var "b3"))  ($#r1_hidden :::"="::: )  (Set   ($#k16_hahnban1 :::"prodReIm"::: )  (Set (Var "l")))) "iff" (Bool  "for" (Set (Var "v")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "V")) "holds"  (Bool (Set (Set (Var "b3"))  ($#k3_funct_2 :::"."::: )  (Set (Var "v")))  ($#r1_hidden :::"="::: )  (Set  ($#k1_hahnban1 :::"[**"::: ) (Set  "(" (Set  "("  ($#k13_hahnban1 :::"RtoC"::: )  (Set (Var "l")) ")" )  ($#k3_funct_2 :::"."::: )  (Set (Var "v")) ")" ) "," (Set  "("  ($#k1_real_1 :::"-"::: )  (Set  "(" (Set  "("  ($#k15_hahnban1 :::"i-shift"::: )  (Set  "("  ($#k13_hahnban1 :::"RtoC"::: )  (Set (Var "l")) ")" ) ")" )  ($#k3_funct_2 :::"."::: )  (Set (Var "v")) ")" ) ")" ) ($#k1_hahnban1 :::"**]"::: ) )))  ")" )))); 
 
theorem :: HAHNBAN1:25 (Bool  "for" (Set (Var "V")) "being"   ($#l1_vectsp_1 :::"VectSp":::) "of" (Set   ($#k1_complfld :::"F_Complex"::: )  )  (Bool  "for" (Set (Var "l")) "being"   ($#m1_subset_1 :::"linear-Functional":::) "of" (Set (Var "V")) "holds"  (Bool (Set   ($#k11_hahnban1 :::"projRe"::: )  (Set (Var "l"))) "is"   ($#m1_subset_1 :::"linear-Functional":::) "of" (Set  "("  ($#k10_hahnban1 :::"RealVS"::: )  (Set (Var "V")) ")" )))) ; 
 
theorem :: HAHNBAN1:26 (Bool  "for" (Set (Var "V")) "being"   ($#l1_vectsp_1 :::"VectSp":::) "of" (Set   ($#k1_complfld :::"F_Complex"::: )  )  (Bool  "for" (Set (Var "l")) "being"   ($#m1_subset_1 :::"linear-Functional":::) "of" (Set (Var "V")) "holds"  (Bool (Set   ($#k12_hahnban1 :::"projIm"::: )  (Set (Var "l"))) "is"   ($#m1_subset_1 :::"linear-Functional":::) "of" (Set  "("  ($#k10_hahnban1 :::"RealVS"::: )  (Set (Var "V")) ")" )))) ; 
 
theorem :: HAHNBAN1:27 (Bool  "for" (Set (Var "V")) "being"   ($#l1_vectsp_1 :::"VectSp":::) "of" (Set   ($#k1_complfld :::"F_Complex"::: )  )  (Bool  "for" (Set (Var "l")) "being"   ($#m1_subset_1 :::"linear-Functional":::) "of" (Set  "("  ($#k10_hahnban1 :::"RealVS"::: )  (Set (Var "V")) ")" ) "holds"  (Bool (Set   ($#k16_hahnban1 :::"prodReIm"::: )  (Set (Var "l"))) "is"   ($#m1_subset_1 :::"linear-Functional":::) "of" (Set (Var "V"))))) ; 
 
theorem :: HAHNBAN1:28 (Bool  "for" (Set (Var "V")) "being"   ($#l1_vectsp_1 :::"VectSp":::) "of" (Set   ($#k1_complfld :::"F_Complex"::: )  )  (Bool  "for" (Set (Var "p")) "being"   ($#m1_subset_1 :::"Semi-Norm":::) "of" (Set (Var "V"))  (Bool  "for" (Set (Var "M")) "being"    ($#m1_vectsp_4 :::"Subspace"::: )   "of" (Set (Var "V"))  (Bool  "for" (Set (Var "l")) "being"   ($#m1_subset_1 :::"linear-Functional":::) "of" (Set (Var "M"))  "st" (Bool (Bool  "("   "for" (Set (Var "e")) "being"   ($#m1_subset_1 :::"Vector":::) "of" (Set (Var "M"))  (Bool  "for" (Set (Var "v")) "being"   ($#m1_subset_1 :::"Vector":::) "of" (Set (Var "V"))  "st" (Bool (Bool (Set (Var "v"))  ($#r1_hidden :::"="::: )  (Set (Var "e")))) "holds"  (Bool (Set  ($#k17_complex1 :::"|."::: ) (Set  "(" (Set (Var "l"))  ($#k3_funct_2 :::"."::: )  (Set (Var "e")) ")" ) ($#k17_complex1 :::".|"::: ) )  ($#r1_xxreal_0 :::"<="::: )  (Set (Set (Var "p"))  ($#k3_funct_2 :::"."::: )  (Set (Var "v")))))  ")" )) "holds"  (Bool  "ex" (Set (Var "L")) "being"   ($#m1_subset_1 :::"linear-Functional":::) "of" (Set (Var "V")) "st"  (Bool  "("  (Bool (Set (Set (Var "L"))  ($#k5_relset_1 :::"|"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "M"))))  ($#r1_hidden :::"="::: )  (Set (Var "l"))) & (Bool  "("   "for" (Set (Var "e")) "being"   ($#m1_subset_1 :::"Vector":::) "of" (Set (Var "V")) "holds"  (Bool (Set  ($#k17_complex1 :::"|."::: ) (Set  "(" (Set (Var "L"))  ($#k3_funct_2 :::"."::: )  (Set (Var "e")) ")" ) ($#k17_complex1 :::".|"::: ) )  ($#r1_xxreal_0 :::"<="::: )  (Set (Set (Var "p"))  ($#k3_funct_2 :::"."::: )  (Set (Var "e"))))  ")" )  ")" )))))) ; 
 begin  
theorem :: HAHNBAN1:29 (Bool  "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Set (Var "x"))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool  "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"  (Bool (Set (Set  "("  ($#k4_group_1 :::"power"::: )  (Set  ($#k1_complfld :::"F_Complex"::: ) ) ")" )  ($#k1_binop_1 :::"."::: )   "(" (Set  ($#k1_hahnban1 :::"[**"::: ) (Set (Var "x")) "," (Set  ($#k6_numbers :::"0"::: ) ) ($#k1_hahnban1 :::"**]"::: ) ) "," (Set (Var "n")) ")" )  ($#r1_hidden :::"="::: )  (Set  ($#k1_hahnban1 :::"[**"::: ) (Set  "(" (Set (Var "x"))  ($#k3_power :::"to_power"::: )  (Set (Var "n")) ")" ) "," (Set  ($#k6_numbers :::"0"::: ) ) ($#k1_hahnban1 :::"**]"::: ) )))) ;