:: HERMITAN  semantic presentation begin  
theorem :: HERMITAN:1 (Bool  "for" (Set (Var "a")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "a"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "a"))  ($#k15_complex1 :::"*'"::: )  ))) "holds"  (Bool (Set   ($#k4_complex1 :::"Im"::: )  (Set (Var "a")))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))) ; 
 
theorem :: HERMITAN:2 (Bool  "for" (Set (Var "a")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k2_numbers :::"COMPLEX"::: )  )  "st" (Bool (Bool (Set (Var "a"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k5_complex1 :::"0c"::: )  ))) "holds"  (Bool  "("  (Bool (Set  ($#k17_complex1 :::"|."::: ) (Set  "(" (Set  "(" (Set  "("  ($#k3_complex1 :::"Re"::: )  (Set (Var "a")) ")" )  ($#k13_complex1 :::"/"::: )  (Set  ($#k17_complex1 :::"|."::: ) (Set (Var "a")) ($#k17_complex1 :::".|"::: ) ) ")" )  ($#k8_complex1 :::"+"::: )  (Set  "(" (Set  "(" (Set  "("  ($#k1_real_1 :::"-"::: )  (Set  "("  ($#k4_complex1 :::"Im"::: )  (Set (Var "a")) ")" ) ")" )  ($#k13_complex1 :::"/"::: )  (Set  ($#k17_complex1 :::"|."::: ) (Set (Var "a")) ($#k17_complex1 :::".|"::: ) ) ")" )  ($#k9_complex1 :::"*"::: )  (Set  ($#k7_complex1 :::"<i>"::: ) ) ")" ) ")" ) ($#k17_complex1 :::".|"::: ) )  ($#r1_hidden :::"="::: )  (Num 1)) & (Bool (Set   ($#k3_complex1 :::"Re"::: )  (Set  "(" (Set  "(" (Set  "(" (Set  "("  ($#k3_complex1 :::"Re"::: )  (Set (Var "a")) ")" )  ($#k13_complex1 :::"/"::: )  (Set  ($#k17_complex1 :::"|."::: ) (Set (Var "a")) ($#k17_complex1 :::".|"::: ) ) ")" )  ($#k8_complex1 :::"+"::: )  (Set  "(" (Set  "(" (Set  "("  ($#k1_real_1 :::"-"::: )  (Set  "("  ($#k4_complex1 :::"Im"::: )  (Set (Var "a")) ")" ) ")" )  ($#k13_complex1 :::"/"::: )  (Set  ($#k17_complex1 :::"|."::: ) (Set (Var "a")) ($#k17_complex1 :::".|"::: ) ) ")" )  ($#k9_complex1 :::"*"::: )  (Set  ($#k7_complex1 :::"<i>"::: ) ) ")" ) ")" )  ($#k9_complex1 :::"*"::: )  (Set (Var "a")) ")" ))  ($#r1_hidden :::"="::: )  (Set  ($#k17_complex1 :::"|."::: ) (Set (Var "a")) ($#k17_complex1 :::".|"::: ) )) & (Bool (Set   ($#k4_complex1 :::"Im"::: )  (Set  "(" (Set  "(" (Set  "(" (Set  "("  ($#k3_complex1 :::"Re"::: )  (Set (Var "a")) ")" )  ($#k13_complex1 :::"/"::: )  (Set  ($#k17_complex1 :::"|."::: ) (Set (Var "a")) ($#k17_complex1 :::".|"::: ) ) ")" )  ($#k8_complex1 :::"+"::: )  (Set  "(" (Set  "(" (Set  "("  ($#k1_real_1 :::"-"::: )  (Set  "("  ($#k4_complex1 :::"Im"::: )  (Set (Var "a")) ")" ) ")" )  ($#k13_complex1 :::"/"::: )  (Set  ($#k17_complex1 :::"|."::: ) (Set (Var "a")) ($#k17_complex1 :::".|"::: ) ) ")" )  ($#k9_complex1 :::"*"::: )  (Set  ($#k7_complex1 :::"<i>"::: ) ) ")" ) ")" )  ($#k9_complex1 :::"*"::: )  (Set (Var "a")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")" )) ; 
 
theorem :: HERMITAN:3 (Bool  "for" (Set (Var "a")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k2_numbers :::"COMPLEX"::: )  ) (Bool  "ex" (Set (Var "b")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k2_numbers :::"COMPLEX"::: )  ) "st"  (Bool  "("  (Bool (Set  ($#k17_complex1 :::"|."::: ) (Set (Var "b")) ($#k17_complex1 :::".|"::: ) )  ($#r1_hidden :::"="::: )  (Num 1)) & (Bool (Set   ($#k3_complex1 :::"Re"::: )  (Set  "(" (Set (Var "b"))  ($#k9_complex1 :::"*"::: )  (Set (Var "a")) ")" ))  ($#r1_hidden :::"="::: )  (Set  ($#k17_complex1 :::"|."::: ) (Set (Var "a")) ($#k17_complex1 :::".|"::: ) )) & (Bool (Set   ($#k4_complex1 :::"Im"::: )  (Set  "(" (Set (Var "b"))  ($#k9_complex1 :::"*"::: )  (Set (Var "a")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")" ))) ; 
 
theorem :: HERMITAN:4 (Bool  "for" (Set (Var "a")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k2_numbers :::"COMPLEX"::: )  ) "holds"  (Bool (Set (Set (Var "a"))  ($#k9_complex1 :::"*"::: )  (Set  "(" (Set (Var "a"))  ($#k15_complex1 :::"*'"::: )  ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  ($#k17_complex1 :::"|."::: ) (Set (Var "a")) ($#k17_complex1 :::".|"::: ) )  ($#k5_square_1 :::"^2"::: )  ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" (Set  ($#k6_numbers :::"0"::: ) )  ($#k3_xcmplx_0 :::"*"::: )  (Set  ($#k7_complex1 :::"<i>"::: ) ) ")" )))) ; 
 
theorem :: HERMITAN:5 (Bool  "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set  ($#k1_complfld :::"F_Complex"::: ) )  "st" (Bool (Bool (Set (Var "a"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "a"))  ($#k2_complfld :::"*'"::: )  ))) "holds"  (Bool (Set   ($#k4_complex1 :::"Im"::: )  (Set (Var "a")))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))) ; 
 
theorem :: HERMITAN:6 (Bool (Set (Set  ($#k2_hahnban1 :::"i_FC"::: ) )  ($#k8_group_1 :::"*"::: )  (Set  "(" (Set  ($#k2_hahnban1 :::"i_FC"::: ) )  ($#k2_complfld :::"*'"::: )  ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k1_group_1 :::"1_"::: )  (Set  ($#k1_complfld :::"F_Complex"::: ) ))) ; 
 
theorem :: HERMITAN:7 (Bool  "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set  ($#k1_complfld :::"F_Complex"::: ) )  "st" (Bool (Bool (Set (Var "a"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k4_struct_0 :::"0."::: )  (Set  ($#k1_complfld :::"F_Complex"::: ) )))) "holds"  (Bool  "("  (Bool (Set  ($#k17_complex1 :::"|."::: ) (Set  ($#k1_hahnban1 :::"[**"::: ) (Set  "(" (Set  "("  ($#k3_complex1 :::"Re"::: )  (Set (Var "a")) ")" )  ($#k13_complex1 :::"/"::: )  (Set  ($#k17_complex1 :::"|."::: ) (Set (Var "a")) ($#k17_complex1 :::".|"::: ) ) ")" ) "," (Set  "(" (Set  "("  ($#k1_real_1 :::"-"::: )  (Set  "("  ($#k4_complex1 :::"Im"::: )  (Set (Var "a")) ")" ) ")" )  ($#k13_complex1 :::"/"::: )  (Set  ($#k17_complex1 :::"|."::: ) (Set (Var "a")) ($#k17_complex1 :::".|"::: ) ) ")" ) ($#k1_hahnban1 :::"**]"::: ) ) ($#k17_complex1 :::".|"::: ) )  ($#r1_hidden :::"="::: )  (Num 1)) & (Bool (Set   ($#k3_complex1 :::"Re"::: )  (Set  "(" (Set  ($#k1_hahnban1 :::"[**"::: ) (Set  "(" (Set  "("  ($#k3_complex1 :::"Re"::: )  (Set (Var "a")) ")" )  ($#k13_complex1 :::"/"::: )  (Set  ($#k17_complex1 :::"|."::: ) (Set (Var "a")) ($#k17_complex1 :::".|"::: ) ) ")" ) "," (Set  "(" (Set  "("  ($#k1_real_1 :::"-"::: )  (Set  "("  ($#k4_complex1 :::"Im"::: )  (Set (Var "a")) ")" ) ")" )  ($#k13_complex1 :::"/"::: )  (Set  ($#k17_complex1 :::"|."::: ) (Set (Var "a")) ($#k17_complex1 :::".|"::: ) ) ")" ) ($#k1_hahnban1 :::"**]"::: ) )  ($#k8_group_1 :::"*"::: )  (Set (Var "a")) ")" ))  ($#r1_hidden :::"="::: )  (Set  ($#k17_complex1 :::"|."::: ) (Set (Var "a")) ($#k17_complex1 :::".|"::: ) )) & (Bool (Set   ($#k4_complex1 :::"Im"::: )  (Set  "(" (Set  ($#k1_hahnban1 :::"[**"::: ) (Set  "(" (Set  "("  ($#k3_complex1 :::"Re"::: )  (Set (Var "a")) ")" )  ($#k13_complex1 :::"/"::: )  (Set  ($#k17_complex1 :::"|."::: ) (Set (Var "a")) ($#k17_complex1 :::".|"::: ) ) ")" ) "," (Set  "(" (Set  "("  ($#k1_real_1 :::"-"::: )  (Set  "("  ($#k4_complex1 :::"Im"::: )  (Set (Var "a")) ")" ) ")" )  ($#k13_complex1 :::"/"::: )  (Set  ($#k17_complex1 :::"|."::: ) (Set (Var "a")) ($#k17_complex1 :::".|"::: ) ) ")" ) ($#k1_hahnban1 :::"**]"::: ) )  ($#k8_group_1 :::"*"::: )  (Set (Var "a")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")" )) ; 
 
theorem :: HERMITAN:8 (Bool  "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set  ($#k1_complfld :::"F_Complex"::: ) ) (Bool  "ex" (Set (Var "b")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set  ($#k1_complfld :::"F_Complex"::: ) ) "st"  (Bool  "("  (Bool (Set  ($#k17_complex1 :::"|."::: ) (Set (Var "b")) ($#k17_complex1 :::".|"::: ) )  ($#r1_hidden :::"="::: )  (Num 1)) & (Bool (Set   ($#k3_complex1 :::"Re"::: )  (Set  "(" (Set (Var "b"))  ($#k8_group_1 :::"*"::: )  (Set (Var "a")) ")" ))  ($#r1_hidden :::"="::: )  (Set  ($#k17_complex1 :::"|."::: ) (Set (Var "a")) ($#k17_complex1 :::".|"::: ) )) & (Bool (Set   ($#k4_complex1 :::"Im"::: )  (Set  "(" (Set (Var "b"))  ($#k8_group_1 :::"*"::: )  (Set (Var "a")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")" ))) ; 
 
theorem :: HERMITAN:9 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set  ($#k1_complfld :::"F_Complex"::: ) ) "holds"   (Bool  "("  (Bool (Set   ($#k3_complex1 :::"Re"::: )  (Set  "(" (Set (Var "a"))  ($#k5_algstr_0 :::"-"::: )  (Set (Var "b")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k3_complex1 :::"Re"::: )  (Set (Var "a")) ")" )  ($#k9_real_1 :::"-"::: )  (Set  "("  ($#k3_complex1 :::"Re"::: )  (Set (Var "b")) ")" ))) & (Bool (Set   ($#k4_complex1 :::"Im"::: )  (Set  "(" (Set (Var "a"))  ($#k5_algstr_0 :::"-"::: )  (Set (Var "b")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k4_complex1 :::"Im"::: )  (Set (Var "a")) ")" )  ($#k9_real_1 :::"-"::: )  (Set  "("  ($#k4_complex1 :::"Im"::: )  (Set (Var "b")) ")" )))  ")" )) ; 
 
theorem :: HERMITAN:10 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set  ($#k1_complfld :::"F_Complex"::: ) )  "st" (Bool (Bool (Set   ($#k4_complex1 :::"Im"::: )  (Set (Var "a")))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool  "("  (Bool (Set   ($#k3_complex1 :::"Re"::: )  (Set  "(" (Set (Var "a"))  ($#k8_group_1 :::"*"::: )  (Set (Var "b")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k3_complex1 :::"Re"::: )  (Set (Var "a")) ")" )  ($#k8_real_1 :::"*"::: )  (Set  "("  ($#k3_complex1 :::"Re"::: )  (Set (Var "b")) ")" ))) & (Bool (Set   ($#k4_complex1 :::"Im"::: )  (Set  "(" (Set (Var "a"))  ($#k8_group_1 :::"*"::: )  (Set (Var "b")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k3_complex1 :::"Re"::: )  (Set (Var "a")) ")" )  ($#k8_real_1 :::"*"::: )  (Set  "("  ($#k4_complex1 :::"Im"::: )  (Set (Var "b")) ")" )))  ")" )) ; 
 
theorem :: HERMITAN:11 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set  ($#k1_complfld :::"F_Complex"::: ) )  "st" (Bool (Bool (Set   ($#k4_complex1 :::"Im"::: )  (Set (Var "a")))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set   ($#k4_complex1 :::"Im"::: )  (Set (Var "b")))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set   ($#k4_complex1 :::"Im"::: )  (Set  "(" (Set (Var "a"))  ($#k8_group_1 :::"*"::: )  (Set (Var "b")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))) ; 
 
theorem :: HERMITAN:12 (Bool  "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set  ($#k1_complfld :::"F_Complex"::: ) )  "st" (Bool (Bool (Set   ($#k4_complex1 :::"Im"::: )  (Set (Var "a")))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set (Var "a"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "a"))  ($#k2_complfld :::"*'"::: )  ))) ; 
 
theorem :: HERMITAN:13 (Bool  "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set  ($#k1_complfld :::"F_Complex"::: ) ) "holds"  (Bool (Set (Set (Var "a"))  ($#k8_group_1 :::"*"::: )  (Set  "(" (Set (Var "a"))  ($#k2_complfld :::"*'"::: )  ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  ($#k17_complex1 :::"|."::: ) (Set (Var "a")) ($#k17_complex1 :::".|"::: ) )  ($#k5_square_1 :::"^2"::: )  ))) ; 
 
theorem :: HERMITAN:14 (Bool  "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set  ($#k1_complfld :::"F_Complex"::: ) )  "st" (Bool (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k3_complex1 :::"Re"::: )  (Set (Var "a")))) & (Bool (Set   ($#k4_complex1 :::"Im"::: )  (Set (Var "a")))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set  ($#k17_complex1 :::"|."::: ) (Set (Var "a")) ($#k17_complex1 :::".|"::: ) )  ($#r1_hidden :::"="::: )  (Set   ($#k3_complex1 :::"Re"::: )  (Set (Var "a"))))) ; 
 
theorem :: HERMITAN:15 (Bool  "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set  ($#k1_complfld :::"F_Complex"::: ) ) "holds"  (Bool (Set (Set  "("  ($#k3_complex1 :::"Re"::: )  (Set (Var "a")) ")" )  ($#k7_real_1 :::"+"::: )  (Set  "("  ($#k3_complex1 :::"Re"::: )  (Set  "(" (Set (Var "a"))  ($#k2_complfld :::"*'"::: )  ")" ) ")" ))  ($#r1_hidden :::"="::: )  (Set (Num 2)  ($#k8_real_1 :::"*"::: )  (Set  "("  ($#k3_complex1 :::"Re"::: )  (Set (Var "a")) ")" )))) ; 
 begin  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 :::"Functional":::) "of" (Set (Const "V")); attr "f" is  :::"cmplxhomogeneous":::  means :: HERMITAN:def 1 (Bool  "for" (Set (Var "v")) "being"   ($#m1_subset_1 :::"Vector":::) "of" "V"  (Bool  "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Scalar":::) "of"  "holds"  (Bool (Set "f"  ($#k3_funct_2 :::"."::: )  (Set  "(" (Set (Var "a"))  ($#k4_vectsp_1 :::"*"::: )  (Set (Var "v")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "a"))  ($#k2_complfld :::"*'"::: )  ")" )  ($#k8_group_1 :::"*"::: )  (Set  "(" "f"  ($#k3_funct_2 :::"."::: )  (Set (Var "v")) ")" ))))); end; 





:: deftheorem    defines :::"cmplxhomogeneous"::: HERMITAN:def 1 :  (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 :::"Functional":::) "of" (Set (Var "V")) "holds"   (Bool  "("  (Bool (Set (Var "f")) "is"   ($#v1_hermitan :::"cmplxhomogeneous"::: )  ) "iff" (Bool  "for" (Set (Var "v")) "being"   ($#m1_subset_1 :::"Vector":::) "of" (Set (Var "V"))  (Bool  "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Scalar":::) "of"  "holds"  (Bool (Set (Set (Var "f"))  ($#k3_funct_2 :::"."::: )  (Set  "(" (Set (Var "a"))  ($#k4_vectsp_1 :::"*"::: )  (Set (Var "v")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "a"))  ($#k2_complfld :::"*'"::: )  ")" )  ($#k8_group_1 :::"*"::: )  (Set  "(" (Set (Var "f"))  ($#k3_funct_2 :::"."::: )  (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   ($#k7_hahnban1 :::"0Functional"::: )  "V") ->   ($#v1_hermitan :::"cmplxhomogeneous"::: )   ; 
end; registrationlet "V" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v13_algstr_0 :::"right_complementable"::: )     ($#v3_rlvect_1 :::"add-associative"::: )     ($#v4_rlvect_1 :::"right_zeroed"::: )     ($#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   ($#v1_funct_1 :::"Function-like"::: )   bbbadV1_FUNCT_2((Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "V") "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set  ($#k1_complfld :::"F_Complex"::: ) )))   ($#v1_hermitan :::"cmplxhomogeneous"::: )    ->   ($#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" (Set  ($#k1_complfld :::"F_Complex"::: ) )) ($#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  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set  ($#k1_complfld :::"F_Complex"::: ) )))   ($#v1_funct_1 :::"Function-like"::: )   bbbadV1_FUNCT_2((Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "V") "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set  ($#k1_complfld :::"F_Complex"::: ) )))   ($#v13_vectsp_1 :::"additive"::: )     ($#v2_hahnban1 :::"0-preserving"::: )     ($#v1_hermitan :::"cmplxhomogeneous"::: )    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" (Set  ($#k1_complfld :::"F_Complex"::: ) )) ($#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 antilinear-Functional of "V" is   ($#v13_vectsp_1 :::"additive"::: )     ($#v1_hermitan :::"cmplxhomogeneous"::: )    ($#m1_subset_1 :::"Functional":::) "of" "V"; end; registrationlet "V" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_vectsp_1 :::"VectSpStr"::: )   "over" (Set   ($#k1_complfld :::"F_Complex"::: )  ); let "f", "g" be   ($#v1_hermitan :::"cmplxhomogeneous"::: )    ($#m1_subset_1 :::"Functional":::) "of" (Set (Const "V")); 
cluster (Set "f"  ($#k3_hahnban1 :::"+"::: )  "g") ->   ($#v1_hermitan :::"cmplxhomogeneous"::: )   ; 
end; registrationlet "V" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_vectsp_1 :::"VectSpStr"::: )   "over" (Set   ($#k1_complfld :::"F_Complex"::: )  ); let "f" be   ($#v1_hermitan :::"cmplxhomogeneous"::: )    ($#m1_subset_1 :::"Functional":::) "of" (Set (Const "V")); 
cluster (Set   ($#k4_hahnban1 :::"-"::: )  "f") ->   ($#v1_hermitan :::"cmplxhomogeneous"::: )   ; 
end; registrationlet "V" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_vectsp_1 :::"VectSpStr"::: )   "over" (Set   ($#k1_complfld :::"F_Complex"::: )  ); let "a" be   ($#m1_subset_1 :::"Scalar":::) "of" ; let "f" be   ($#v1_hermitan :::"cmplxhomogeneous"::: )    ($#m1_subset_1 :::"Functional":::) "of" (Set (Const "V")); 
cluster (Set "a"  ($#k6_hahnban1 :::"*"::: )  "f") ->   ($#v1_hermitan :::"cmplxhomogeneous"::: )   ; 
end; registrationlet "V" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_vectsp_1 :::"VectSpStr"::: )   "over" (Set   ($#k1_complfld :::"F_Complex"::: )  ); let "f", "g" be   ($#v1_hermitan :::"cmplxhomogeneous"::: )    ($#m1_subset_1 :::"Functional":::) "of" (Set (Const "V")); 
cluster (Set "f"  ($#k5_hahnban1 :::"-"::: )  "g") ->   ($#v1_hermitan :::"cmplxhomogeneous"::: )   ; 
end; 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 :::"Functional":::) "of" (Set (Const "V")); func "f" :::"*'":::  ->   ($#m1_subset_1 :::"Functional":::) "of" "V" means :: HERMITAN:def 2 (Bool  "for" (Set (Var "v")) "being"   ($#m1_subset_1 :::"Vector":::) "of" "V" "holds"  (Bool (Set it  ($#k3_funct_2 :::"."::: )  (Set (Var "v")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" "f"  ($#k3_funct_2 :::"."::: )  (Set (Var "v")) ")" )  ($#k2_complfld :::"*'"::: )  ))); end; 






:: deftheorem    defines :::"*'"::: HERMITAN:def 2 :  (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")) "," (Set (Var "b3")) "being"   ($#m1_subset_1 :::"Functional":::) "of" (Set (Var "V")) "holds"   (Bool  "("  (Bool (Set (Var "b3"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "f"))  ($#k1_hermitan :::"*'"::: )  )) "iff" (Bool  "for" (Set (Var "v")) "being"   ($#m1_subset_1 :::"Vector":::) "of" (Set (Var "V")) "holds"  (Bool (Set (Set (Var "b3"))  ($#k3_funct_2 :::"."::: )  (Set (Var "v")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "f"))  ($#k3_funct_2 :::"."::: )  (Set (Var "v")) ")" )  ($#k2_complfld :::"*'"::: )  )))  ")" ))); 
 registrationlet "V" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_vectsp_1 :::"VectSpStr"::: )   "over" (Set   ($#k1_complfld :::"F_Complex"::: )  ); let "f" be   ($#v13_vectsp_1 :::"additive"::: )    ($#m1_subset_1 :::"Functional":::) "of" (Set (Const "V")); 
cluster (Set "f"  ($#k1_hermitan :::"*'"::: )  ) ->   ($#v13_vectsp_1 :::"additive"::: )   ; 
end; registrationlet "V" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_vectsp_1 :::"VectSpStr"::: )   "over" (Set   ($#k1_complfld :::"F_Complex"::: )  ); let "f" be   ($#v1_hahnban1 :::"homogeneous"::: )    ($#m1_subset_1 :::"Functional":::) "of" (Set (Const "V")); 
cluster (Set "f"  ($#k1_hermitan :::"*'"::: )  ) ->   ($#v1_hermitan :::"cmplxhomogeneous"::: )   ; 
end; registrationlet "V" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_vectsp_1 :::"VectSpStr"::: )   "over" (Set   ($#k1_complfld :::"F_Complex"::: )  ); let "f" be   ($#v1_hermitan :::"cmplxhomogeneous"::: )    ($#m1_subset_1 :::"Functional":::) "of" (Set (Const "V")); 
cluster (Set "f"  ($#k1_hermitan :::"*'"::: )  ) ->   ($#v1_hahnban1 :::"homogeneous"::: )   ; 
end; registrationlet "V" be  ($#~v7_struct_0  "non"   ($#v7_struct_0 :::"trivial"::: )   )   ($#l1_vectsp_1 :::"VectSp":::) "of" (Set   ($#k1_complfld :::"F_Complex"::: )  ); let "f" be  ($#~v3_funct_1  "non"   ($#v3_funct_1 :::"constant"::: )   )   ($#m1_subset_1 :::"Functional":::) "of" (Set (Const "V")); 
cluster (Set "f"  ($#k1_hermitan :::"*'"::: )  ) ->  ($#~v3_funct_1  "non"   ($#v3_funct_1 :::"constant"::: )   )  ; 
end; registrationlet "V" be  ($#~v7_struct_0  "non"   ($#v7_struct_0 :::"trivial"::: )   )   ($#l1_vectsp_1 :::"VectSp":::) "of" (Set   ($#k1_complfld :::"F_Complex"::: )  ); 
cluster  ($#~v1_zfmisc_1  "non"   ($#v1_zfmisc_1 :::"trivial"::: )   )  bbbadV1_RELAT_1() bbbadV4_RELAT_1((Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "V")) bbbadV5_RELAT_1((Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set  ($#k1_complfld :::"F_Complex"::: ) )))   ($#v1_funct_1 :::"Function-like"::: )    ($#~v3_funct_1  "non"   ($#v3_funct_1 :::"constant"::: )   )  bbbadV1_FUNCT_2((Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "V") "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set  ($#k1_complfld :::"F_Complex"::: ) )))   ($#v13_vectsp_1 :::"additive"::: )     ($#v1_hermitan :::"cmplxhomogeneous"::: )    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" (Set  ($#k1_complfld :::"F_Complex"::: ) )) ($#k2_zfmisc_1 :::":]"::: ) )); 
end; 
theorem :: HERMITAN:16 (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 :::"Functional":::) "of" (Set (Var "V")) "holds"  (Bool (Set (Set  "(" (Set (Var "f"))  ($#k1_hermitan :::"*'"::: )  ")" )  ($#k1_hermitan :::"*'"::: )  )  ($#r2_funct_2 :::"="::: )  (Set (Var "f"))))) ; 
 
theorem :: HERMITAN: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"::: )  ) "holds"  (Bool (Set (Set  "("  ($#k7_hahnban1 :::"0Functional"::: )  (Set (Var "V")) ")" )  ($#k1_hermitan :::"*'"::: )  )  ($#r2_funct_2 :::"="::: )  (Set   ($#k7_hahnban1 :::"0Functional"::: )  (Set (Var "V"))))) ; 
 
theorem :: HERMITAN: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 "f")) "," (Set (Var "g")) "being"   ($#m1_subset_1 :::"Functional":::) "of" (Set (Var "V")) "holds"  (Bool (Set (Set  "(" (Set (Var "f"))  ($#k3_hahnban1 :::"+"::: )  (Set (Var "g")) ")" )  ($#k1_hermitan :::"*'"::: )  )  ($#r2_funct_2 :::"="::: )  (Set (Set  "(" (Set (Var "f"))  ($#k1_hermitan :::"*'"::: )  ")" )  ($#k3_hahnban1 :::"+"::: )  (Set  "(" (Set (Var "g"))  ($#k1_hermitan :::"*'"::: )  ")" ))))) ; 
 
theorem :: HERMITAN: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 "f")) "being"   ($#m1_subset_1 :::"Functional":::) "of" (Set (Var "V")) "holds"  (Bool (Set (Set  "("  ($#k4_hahnban1 :::"-"::: )  (Set (Var "f")) ")" )  ($#k1_hermitan :::"*'"::: )  )  ($#r2_funct_2 :::"="::: )  (Set   ($#k4_hahnban1 :::"-"::: )  (Set  "(" (Set (Var "f"))  ($#k1_hermitan :::"*'"::: )  ")" ))))) ; 
 
theorem :: HERMITAN: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 "f")) "being"   ($#m1_subset_1 :::"Functional":::) "of" (Set (Var "V"))  (Bool  "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Scalar":::) "of"  "holds"  (Bool (Set (Set  "(" (Set (Var "a"))  ($#k6_hahnban1 :::"*"::: )  (Set (Var "f")) ")" )  ($#k1_hermitan :::"*'"::: )  )  ($#r2_funct_2 :::"="::: )  (Set (Set  "(" (Set (Var "a"))  ($#k2_complfld :::"*'"::: )  ")" )  ($#k6_hahnban1 :::"*"::: )  (Set  "(" (Set (Var "f"))  ($#k1_hermitan :::"*'"::: )  ")" )))))) ; 
 
theorem :: HERMITAN: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 "f")) "," (Set (Var "g")) "being"   ($#m1_subset_1 :::"Functional":::) "of" (Set (Var "V")) "holds"  (Bool (Set (Set  "(" (Set (Var "f"))  ($#k5_hahnban1 :::"-"::: )  (Set (Var "g")) ")" )  ($#k1_hermitan :::"*'"::: )  )  ($#r2_funct_2 :::"="::: )  (Set (Set  "(" (Set (Var "f"))  ($#k1_hermitan :::"*'"::: )  ")" )  ($#k5_hahnban1 :::"-"::: )  (Set  "(" (Set (Var "g"))  ($#k1_hermitan :::"*'"::: )  ")" ))))) ; 
 
theorem :: HERMITAN: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 "f")) "being"   ($#m1_subset_1 :::"Functional":::) "of" (Set (Var "V"))  (Bool  "for" (Set (Var "v")) "being"   ($#m1_subset_1 :::"Vector":::) "of" (Set (Var "V")) "holds"   (Bool  "("  (Bool (Set (Set (Var "f"))  ($#k3_funct_2 :::"."::: )  (Set (Var "v")))  ($#r1_hidden :::"="::: )  (Set   ($#k4_struct_0 :::"0."::: )  (Set  ($#k1_complfld :::"F_Complex"::: ) ))) "iff" (Bool (Set (Set  "(" (Set (Var "f"))  ($#k1_hermitan :::"*'"::: )  ")" )  ($#k3_funct_2 :::"."::: )  (Set (Var "v")))  ($#r1_hidden :::"="::: )  (Set   ($#k4_struct_0 :::"0."::: )  (Set  ($#k1_complfld :::"F_Complex"::: ) )))  ")" )))) ; 
 
theorem :: HERMITAN: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 "f")) "being"   ($#m1_subset_1 :::"Functional":::) "of" (Set (Var "V")) "holds"  (Bool (Set   ($#k8_vectsp10 :::"ker"::: )  (Set (Var "f")))  ($#r1_hidden :::"="::: )  (Set   ($#k8_vectsp10 :::"ker"::: )  (Set  "(" (Set (Var "f"))  ($#k1_hermitan :::"*'"::: )  ")" ))))) ; 
 
theorem :: HERMITAN:24 (Bool  "for" (Set (Var "V")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v13_algstr_0 :::"right_complementable"::: )     ($#v3_rlvect_1 :::"add-associative"::: )     ($#v4_rlvect_1 :::"right_zeroed"::: )     ($#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 :::"antilinear-Functional":::) "of" (Set (Var "V")) "holds"  (Bool (Set   ($#k8_vectsp10 :::"ker"::: )  (Set (Var "f"))) "is"   ($#v1_vectsp_4 :::"linearly-closed"::: )  ))) ; 
 
theorem :: HERMITAN:25 (Bool  "for" (Set (Var "V")) "being"   ($#l1_vectsp_1 :::"VectSp":::) "of" (Set   ($#k1_complfld :::"F_Complex"::: )  )  (Bool  "for" (Set (Var "W")) "being"    ($#m1_vectsp_4 :::"Subspace"::: )   "of" (Set (Var "V"))  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"antilinear-Functional":::) "of" (Set (Var "V"))  "st" (Bool (Bool (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "W")))  ($#r1_tarski :::"c="::: )  (Set   ($#k8_vectsp10 :::"ker"::: )  (Set  "(" (Set (Var "f"))  ($#k1_hermitan :::"*'"::: )  ")" )))) "holds"  (Bool (Set   ($#k10_vectsp10 :::"QFunctional"::: )   "(" (Set (Var "f")) "," (Set (Var "W")) ")" ) "is"   ($#v1_hermitan :::"cmplxhomogeneous"::: )  )))) ; 
 definitionlet "V" be   ($#l1_vectsp_1 :::"VectSp":::) "of" (Set   ($#k1_complfld :::"F_Complex"::: )  ); let "f" be   ($#m1_subset_1 :::"antilinear-Functional":::) "of" (Set (Const "V")); func  :::"QcFunctional"::: "f" ->   ($#m1_subset_1 :::"antilinear-Functional":::) "of" (Set  "("  ($#k6_vectsp10 :::"VectQuot"::: )   "(" "V" "," (Set  "("  ($#k9_vectsp10 :::"Ker"::: )  (Set  "(" "f"  ($#k1_hermitan :::"*'"::: )  ")" ) ")" ) ")"  ")" ) equals :: HERMITAN:def 3 (Set   ($#k10_vectsp10 :::"QFunctional"::: )   "(" "f" "," (Set  "("  ($#k9_vectsp10 :::"Ker"::: )  (Set  "(" "f"  ($#k1_hermitan :::"*'"::: )  ")" ) ")" ) ")" ); end; 






:: deftheorem    defines :::"QcFunctional"::: HERMITAN:def 3 :  (Bool  "for" (Set (Var "V")) "being"   ($#l1_vectsp_1 :::"VectSp":::) "of" (Set   ($#k1_complfld :::"F_Complex"::: )  )  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"antilinear-Functional":::) "of" (Set (Var "V")) "holds"  (Bool (Set   ($#k2_hermitan :::"QcFunctional"::: )  (Set (Var "f")))  ($#r1_hidden :::"="::: )  (Set   ($#k10_vectsp10 :::"QFunctional"::: )   "(" (Set (Var "f")) "," (Set  "("  ($#k9_vectsp10 :::"Ker"::: )  (Set  "(" (Set (Var "f"))  ($#k1_hermitan :::"*'"::: )  ")" ) ")" ) ")" )))); 
 
theorem :: HERMITAN:26 (Bool  "for" (Set (Var "V")) "being"   ($#l1_vectsp_1 :::"VectSp":::) "of" (Set   ($#k1_complfld :::"F_Complex"::: )  )  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"antilinear-Functional":::) "of" (Set (Var "V"))  (Bool  "for" (Set (Var "A")) "being"   ($#m1_subset_1 :::"Vector":::) "of" (Set  "("  ($#k6_vectsp10 :::"VectQuot"::: )   "(" (Set (Var "V")) "," (Set  "("  ($#k9_vectsp10 :::"Ker"::: )  (Set  "(" (Set (Var "f"))  ($#k1_hermitan :::"*'"::: )  ")" ) ")" ) ")"  ")" )  (Bool  "for" (Set (Var "v")) "being"   ($#m1_subset_1 :::"Vector":::) "of" (Set (Var "V"))  "st" (Bool (Bool (Set (Var "A"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "v"))  ($#k3_vectsp_4 :::"+"::: )  (Set  "("  ($#k9_vectsp10 :::"Ker"::: )  (Set  "(" (Set (Var "f"))  ($#k1_hermitan :::"*'"::: )  ")" ) ")" )))) "holds"  (Bool (Set (Set  "("  ($#k2_hermitan :::"QcFunctional"::: )  (Set (Var "f")) ")" )  ($#k3_funct_2 :::"."::: )  (Set (Var "A")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "f"))  ($#k3_funct_2 :::"."::: )  (Set (Var "v")))))))) ; 
 registrationlet "V" be  ($#~v7_struct_0  "non"   ($#v7_struct_0 :::"trivial"::: )   )   ($#l1_vectsp_1 :::"VectSp":::) "of" (Set   ($#k1_complfld :::"F_Complex"::: )  ); let "f" be bbbadV3_FUNCT_1()  ($#m1_subset_1 :::"antilinear-Functional":::) "of" (Set (Const "V")); 
cluster (Set   ($#k2_hermitan :::"QcFunctional"::: )  "f") -> bbbadV3_FUNCT_1() ; 
end; registrationlet "V" be   ($#l1_vectsp_1 :::"VectSp":::) "of" (Set   ($#k1_complfld :::"F_Complex"::: )  ); let "f" be   ($#m1_subset_1 :::"antilinear-Functional":::) "of" (Set (Const "V")); 
cluster (Set   ($#k2_hermitan :::"QcFunctional"::: )  "f") ->  ($#~v2_vectsp10  "non"   ($#v2_vectsp10 :::"degenerated"::: )   )  ; 
end; begin  definitionlet "V", "W" 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 :::"Form":::) "of" (Set (Const "V")) "," (Set (Const "W")); attr "f" is  :::"cmplxhomogeneousFAF":::  means :: HERMITAN:def 4 (Bool  "for" (Set (Var "v")) "being"   ($#m1_subset_1 :::"Vector":::) "of" "V" "holds"  (Bool (Set   ($#k7_bilinear :::"FunctionalFAF"::: )   "(" "f" "," (Set (Var "v")) ")" ) "is"   ($#v1_hermitan :::"cmplxhomogeneous"::: )  )); end; 






:: deftheorem    defines :::"cmplxhomogeneousFAF"::: HERMITAN:def 4 :  (Bool  "for" (Set (Var "V")) "," (Set (Var "W")) "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 :::"Form":::) "of" (Set (Var "V")) "," (Set (Var "W")) "holds"   (Bool  "("  (Bool (Set (Var "f")) "is"   ($#v2_hermitan :::"cmplxhomogeneousFAF"::: )  ) "iff" (Bool  "for" (Set (Var "v")) "being"   ($#m1_subset_1 :::"Vector":::) "of" (Set (Var "V")) "holds"  (Bool (Set   ($#k7_bilinear :::"FunctionalFAF"::: )   "(" (Set (Var "f")) "," (Set (Var "v")) ")" ) "is"   ($#v1_hermitan :::"cmplxhomogeneous"::: )  ))  ")" ))); 
 
theorem :: HERMITAN:27 (Bool  "for" (Set (Var "V")) "," (Set (Var "W")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_vectsp_1 :::"VectSpStr"::: )   "over" (Set   ($#k1_complfld :::"F_Complex"::: )  )  (Bool  "for" (Set (Var "v")) "being"   ($#m1_subset_1 :::"Vector":::) "of" (Set (Var "V"))  (Bool  "for" (Set (Var "w")) "being"   ($#m1_subset_1 :::"Vector":::) "of" (Set (Var "W"))  (Bool  "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set  ($#k1_complfld :::"F_Complex"::: ) )  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Form":::) "of" (Set (Var "V")) "," (Set (Var "W"))  "st" (Bool (Bool (Set (Var "f")) "is"   ($#v2_hermitan :::"cmplxhomogeneousFAF"::: )  )) "holds"  (Bool (Set (Set (Var "f"))  ($#k2_binop_1 :::"."::: )   "(" (Set (Var "v")) "," (Set  "(" (Set (Var "a"))  ($#k4_vectsp_1 :::"*"::: )  (Set (Var "w")) ")" ) ")" )  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "a"))  ($#k2_complfld :::"*'"::: )  ")" )  ($#k8_group_1 :::"*"::: )  (Set  "(" (Set (Var "f"))  ($#k2_binop_1 :::"."::: )   "(" (Set (Var "v")) "," (Set (Var "w")) ")"  ")" )))))))) ; 
 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 :::"Form":::) "of" (Set (Const "V")) "," (Set (Const "V")); attr "f" is  :::"hermitan":::  means :: HERMITAN:def 5 (Bool  "for" (Set (Var "v")) "," (Set (Var "u")) "being"   ($#m1_subset_1 :::"Vector":::) "of" "V" "holds"  (Bool (Set "f"  ($#k2_binop_1 :::"."::: )   "(" (Set (Var "v")) "," (Set (Var "u")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set  "(" "f"  ($#k2_binop_1 :::"."::: )   "(" (Set (Var "u")) "," (Set (Var "v")) ")"  ")" )  ($#k2_complfld :::"*'"::: )  ))); attr "f" is  :::"diagRvalued":::  means :: HERMITAN:def 6 (Bool  "for" (Set (Var "v")) "being"   ($#m1_subset_1 :::"Vector":::) "of" "V" "holds"  (Bool (Set   ($#k4_complex1 :::"Im"::: )  (Set  "(" "f"  ($#k2_binop_1 :::"."::: )   "(" (Set (Var "v")) "," (Set (Var "v")) ")"  ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))); attr "f" is  :::"diagReR+0valued":::  means :: HERMITAN:def 7 (Bool  "for" (Set (Var "v")) "being"   ($#m1_subset_1 :::"Vector":::) "of" "V" "holds"  (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k3_complex1 :::"Re"::: )  (Set  "(" "f"  ($#k2_binop_1 :::"."::: )   "(" (Set (Var "v")) "," (Set (Var "v")) ")"  ")" )))); end; 















:: deftheorem    defines :::"hermitan"::: HERMITAN:def 5 :  (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 :::"Form":::) "of" (Set (Var "V")) "," (Set (Var "V")) "holds"   (Bool  "("  (Bool (Set (Var "f")) "is"   ($#v3_hermitan :::"hermitan"::: )  ) "iff" (Bool  "for" (Set (Var "v")) "," (Set (Var "u")) "being"   ($#m1_subset_1 :::"Vector":::) "of" (Set (Var "V")) "holds"  (Bool (Set (Set (Var "f"))  ($#k2_binop_1 :::"."::: )   "(" (Set (Var "v")) "," (Set (Var "u")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "f"))  ($#k2_binop_1 :::"."::: )   "(" (Set (Var "u")) "," (Set (Var "v")) ")"  ")" )  ($#k2_complfld :::"*'"::: )  )))  ")" ))); 
 
:: deftheorem    defines :::"diagRvalued"::: HERMITAN:def 6 :  (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 :::"Form":::) "of" (Set (Var "V")) "," (Set (Var "V")) "holds"   (Bool  "("  (Bool (Set (Var "f")) "is"   ($#v4_hermitan :::"diagRvalued"::: )  ) "iff" (Bool  "for" (Set (Var "v")) "being"   ($#m1_subset_1 :::"Vector":::) "of" (Set (Var "V")) "holds"  (Bool (Set   ($#k4_complex1 :::"Im"::: )  (Set  "(" (Set (Var "f"))  ($#k2_binop_1 :::"."::: )   "(" (Set (Var "v")) "," (Set (Var "v")) ")"  ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  )))  ")" ))); 
 
:: deftheorem    defines :::"diagReR+0valued"::: HERMITAN:def 7 :  (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 :::"Form":::) "of" (Set (Var "V")) "," (Set (Var "V")) "holds"   (Bool  "("  (Bool (Set (Var "f")) "is"   ($#v5_hermitan :::"diagReR+0valued"::: )  ) "iff" (Bool  "for" (Set (Var "v")) "being"   ($#m1_subset_1 :::"Vector":::) "of" (Set (Var "V")) "holds"  (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k3_complex1 :::"Re"::: )  (Set  "(" (Set (Var "f"))  ($#k2_binop_1 :::"."::: )   "(" (Set (Var "v")) "," (Set (Var "v")) ")"  ")" ))))  ")" ))); 
 registrationlet "V", "W" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_vectsp_1 :::"VectSpStr"::: )   "over" (Set   ($#k1_complfld :::"F_Complex"::: )  ); 
cluster (Set   ($#k1_bilinear :::"NulForm"::: )   "(" "V" "," "W" ")" ) ->   ($#v2_hermitan :::"cmplxhomogeneousFAF"::: )   ; 
end; registrationlet "V" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_vectsp_1 :::"VectSpStr"::: )   "over" (Set   ($#k1_complfld :::"F_Complex"::: )  ); 
cluster (Set   ($#k1_bilinear :::"NulForm"::: )   "(" "V" "," "V" ")" ) ->   ($#v3_hermitan :::"hermitan"::: )   ; 

cluster (Set   ($#k1_bilinear :::"NulForm"::: )   "(" "V" "," "V" ")" ) ->   ($#v5_hermitan :::"diagReR+0valued"::: )   ; 
end; registrationlet "V" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_vectsp_1 :::"VectSpStr"::: )   "over" (Set   ($#k1_complfld :::"F_Complex"::: )  ); 
cluster   ($#v1_funct_1 :::"Function-like"::: )   bbbadV1_FUNCT_2((Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "V") "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "V") ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set  ($#k1_complfld :::"F_Complex"::: ) )))   ($#v3_hermitan :::"hermitan"::: )    ->   ($#v4_hermitan :::"diagRvalued"::: )    for    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k1_zfmisc_1 :::"bool"::: )  (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "V") "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "V") ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set  ($#k1_complfld :::"F_Complex"::: ) )) ($#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  ($#k2_zfmisc_1 :::"[:"::: ) (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "V") "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "V") ($#k2_zfmisc_1 :::":]"::: ) )) bbbadV5_RELAT_1((Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set  ($#k1_complfld :::"F_Complex"::: ) )))   ($#v1_funct_1 :::"Function-like"::: )   bbbadV1_FUNCT_2((Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "V") "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "V") ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set  ($#k1_complfld :::"F_Complex"::: ) )))   ($#v1_bilinear :::"additiveFAF"::: )     ($#v2_bilinear :::"additiveSAF"::: )     ($#v4_bilinear :::"homogeneousSAF"::: )     ($#v2_hermitan :::"cmplxhomogeneousFAF"::: )     ($#v3_hermitan :::"hermitan"::: )     ($#v4_hermitan :::"diagRvalued"::: )     ($#v5_hermitan :::"diagReR+0valued"::: )    for    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k1_zfmisc_1 :::"bool"::: )  (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "V") "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "V") ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set  ($#k1_complfld :::"F_Complex"::: ) )) ($#k2_zfmisc_1 :::":]"::: ) )); 
end; registrationlet "V", "W" 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  ($#k2_zfmisc_1 :::"[:"::: ) (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "V") "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "W") ($#k2_zfmisc_1 :::":]"::: ) )) bbbadV5_RELAT_1((Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set  ($#k1_complfld :::"F_Complex"::: ) )))   ($#v1_funct_1 :::"Function-like"::: )   bbbadV1_FUNCT_2((Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "V") "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "W") ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set  ($#k1_complfld :::"F_Complex"::: ) )))   ($#v1_bilinear :::"additiveFAF"::: )     ($#v2_bilinear :::"additiveSAF"::: )     ($#v4_bilinear :::"homogeneousSAF"::: )     ($#v2_hermitan :::"cmplxhomogeneousFAF"::: )    for    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k1_zfmisc_1 :::"bool"::: )  (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "V") "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "W") ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set  ($#k1_complfld :::"F_Complex"::: ) )) ($#k2_zfmisc_1 :::":]"::: ) )); 
end; definitionlet "V", "W" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_vectsp_1 :::"VectSpStr"::: )   "over" (Set   ($#k1_complfld :::"F_Complex"::: )  ); mode sesquilinear-Form of "V" "," "W" is   ($#v1_bilinear :::"additiveFAF"::: )     ($#v2_bilinear :::"additiveSAF"::: )     ($#v4_bilinear :::"homogeneousSAF"::: )     ($#v2_hermitan :::"cmplxhomogeneousFAF"::: )    ($#m1_subset_1 :::"Form":::) "of" "V" "," "W"; end; registrationlet "V" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_vectsp_1 :::"VectSpStr"::: )   "over" (Set   ($#k1_complfld :::"F_Complex"::: )  ); 
cluster   ($#v1_funct_1 :::"Function-like"::: )   bbbadV1_FUNCT_2((Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "V") "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "V") ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set  ($#k1_complfld :::"F_Complex"::: ) )))   ($#v1_bilinear :::"additiveFAF"::: )     ($#v3_hermitan :::"hermitan"::: )    ->   ($#v2_bilinear :::"additiveSAF"::: )    for    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k1_zfmisc_1 :::"bool"::: )  (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "V") "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "V") ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set  ($#k1_complfld :::"F_Complex"::: ) )) ($#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   ($#v1_funct_1 :::"Function-like"::: )   bbbadV1_FUNCT_2((Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "V") "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "V") ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set  ($#k1_complfld :::"F_Complex"::: ) )))   ($#v2_bilinear :::"additiveSAF"::: )     ($#v3_hermitan :::"hermitan"::: )    ->   ($#v1_bilinear :::"additiveFAF"::: )    for    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k1_zfmisc_1 :::"bool"::: )  (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "V") "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "V") ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set  ($#k1_complfld :::"F_Complex"::: ) )) ($#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   ($#v1_funct_1 :::"Function-like"::: )   bbbadV1_FUNCT_2((Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "V") "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "V") ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set  ($#k1_complfld :::"F_Complex"::: ) )))   ($#v4_bilinear :::"homogeneousSAF"::: )     ($#v3_hermitan :::"hermitan"::: )    ->   ($#v2_hermitan :::"cmplxhomogeneousFAF"::: )    for    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k1_zfmisc_1 :::"bool"::: )  (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "V") "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "V") ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set  ($#k1_complfld :::"F_Complex"::: ) )) ($#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   ($#v1_funct_1 :::"Function-like"::: )   bbbadV1_FUNCT_2((Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "V") "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "V") ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set  ($#k1_complfld :::"F_Complex"::: ) )))   ($#v2_hermitan :::"cmplxhomogeneousFAF"::: )     ($#v3_hermitan :::"hermitan"::: )    ->   ($#v4_bilinear :::"homogeneousSAF"::: )    for    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k1_zfmisc_1 :::"bool"::: )  (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "V") "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "V") ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set  ($#k1_complfld :::"F_Complex"::: ) )) ($#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 hermitan-Form of "V" is   ($#v2_bilinear :::"additiveSAF"::: )     ($#v4_bilinear :::"homogeneousSAF"::: )     ($#v3_hermitan :::"hermitan"::: )    ($#m1_subset_1 :::"Form":::) "of" "V" "," "V"; end; registrationlet "V", "W" 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 :::"Functional":::) "of" (Set (Const "V")); let "g" be   ($#v1_hermitan :::"cmplxhomogeneous"::: )    ($#m1_subset_1 :::"Functional":::) "of" (Set (Const "W")); 
cluster (Set   ($#k9_bilinear :::"FormFunctional"::: )   "(" "f" "," "g" ")" ) ->   ($#v2_hermitan :::"cmplxhomogeneousFAF"::: )   ; 
end; registrationlet "V", "W" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_vectsp_1 :::"VectSpStr"::: )   "over" (Set   ($#k1_complfld :::"F_Complex"::: )  ); let "f" be   ($#v2_hermitan :::"cmplxhomogeneousFAF"::: )    ($#m1_subset_1 :::"Form":::) "of" (Set (Const "V")) "," (Set (Const "W")); let "v" be   ($#m1_subset_1 :::"Vector":::) "of" (Set (Const "V")); 
cluster (Set   ($#k7_bilinear :::"FunctionalFAF"::: )   "(" "f" "," "v" ")" ) ->   ($#v1_hermitan :::"cmplxhomogeneous"::: )   ; 
end; registrationlet "V", "W" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_vectsp_1 :::"VectSpStr"::: )   "over" (Set   ($#k1_complfld :::"F_Complex"::: )  ); let "f", "g" be   ($#v2_hermitan :::"cmplxhomogeneousFAF"::: )    ($#m1_subset_1 :::"Form":::) "of" (Set (Const "V")) "," (Set (Const "W")); 
cluster (Set "f"  ($#k2_bilinear :::"+"::: )  "g") ->   ($#v2_hermitan :::"cmplxhomogeneousFAF"::: )   ; 
end; registrationlet "V", "W" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_vectsp_1 :::"VectSpStr"::: )   "over" (Set   ($#k1_complfld :::"F_Complex"::: )  ); let "f" be   ($#v2_hermitan :::"cmplxhomogeneousFAF"::: )    ($#m1_subset_1 :::"Form":::) "of" (Set (Const "V")) "," (Set (Const "W")); let "a" be   ($#m1_subset_1 :::"Scalar":::) "of" ; 
cluster (Set "a"  ($#k3_bilinear :::"*"::: )  "f") ->   ($#v2_hermitan :::"cmplxhomogeneousFAF"::: )   ; 
end; registrationlet "V", "W" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_vectsp_1 :::"VectSpStr"::: )   "over" (Set   ($#k1_complfld :::"F_Complex"::: )  ); let "f" be   ($#v2_hermitan :::"cmplxhomogeneousFAF"::: )    ($#m1_subset_1 :::"Form":::) "of" (Set (Const "V")) "," (Set (Const "W")); 
cluster (Set   ($#k4_bilinear :::"-"::: )  "f") ->   ($#v2_hermitan :::"cmplxhomogeneousFAF"::: )   ; 
end; registrationlet "V", "W" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_vectsp_1 :::"VectSpStr"::: )   "over" (Set   ($#k1_complfld :::"F_Complex"::: )  ); let "f", "g" be   ($#v2_hermitan :::"cmplxhomogeneousFAF"::: )    ($#m1_subset_1 :::"Form":::) "of" (Set (Const "V")) "," (Set (Const "W")); 
cluster (Set "f"  ($#k5_bilinear :::"-"::: )  "g") ->   ($#v2_hermitan :::"cmplxhomogeneousFAF"::: )   ; 
end; registrationlet "V", "W" be  ($#~v7_struct_0  "non"   ($#v7_struct_0 :::"trivial"::: )   )   ($#l1_vectsp_1 :::"VectSp":::) "of" (Set   ($#k1_complfld :::"F_Complex"::: )  ); 
cluster  ($#~v1_zfmisc_1  "non"   ($#v1_zfmisc_1 :::"trivial"::: )   )  bbbadV1_RELAT_1() bbbadV4_RELAT_1((Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "V") "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "W") ($#k2_zfmisc_1 :::":]"::: ) )) bbbadV5_RELAT_1((Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set  ($#k1_complfld :::"F_Complex"::: ) )))   ($#v1_funct_1 :::"Function-like"::: )    ($#~v3_funct_1  "non"   ($#v3_funct_1 :::"constant"::: )   )  bbbadV1_FUNCT_2((Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "V") "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "W") ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set  ($#k1_complfld :::"F_Complex"::: ) )))   ($#v1_bilinear :::"additiveFAF"::: )     ($#v2_bilinear :::"additiveSAF"::: )     ($#v4_bilinear :::"homogeneousSAF"::: )     ($#v2_hermitan :::"cmplxhomogeneousFAF"::: )    for    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k1_zfmisc_1 :::"bool"::: )  (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "V") "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "W") ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set  ($#k1_complfld :::"F_Complex"::: ) )) ($#k2_zfmisc_1 :::":]"::: ) )); 
end; definitionlet "V", "W" 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 :::"Form":::) "of" (Set (Const "V")) "," (Set (Const "W")); func "f" :::"*'":::  ->   ($#m1_subset_1 :::"Form":::) "of" "V" "," "W" means :: HERMITAN:def 8 (Bool  "for" (Set (Var "v")) "being"   ($#m1_subset_1 :::"Vector":::) "of" "V"  (Bool  "for" (Set (Var "w")) "being"   ($#m1_subset_1 :::"Vector":::) "of" "W" "holds"  (Bool (Set it  ($#k2_binop_1 :::"."::: )   "(" (Set (Var "v")) "," (Set (Var "w")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set  "(" "f"  ($#k2_binop_1 :::"."::: )   "(" (Set (Var "v")) "," (Set (Var "w")) ")"  ")" )  ($#k2_complfld :::"*'"::: )  )))); end; 







:: deftheorem    defines :::"*'"::: HERMITAN:def 8 :  (Bool  "for" (Set (Var "V")) "," (Set (Var "W")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_vectsp_1 :::"VectSpStr"::: )   "over" (Set   ($#k1_complfld :::"F_Complex"::: )  )  (Bool  "for" (Set (Var "f")) "," (Set (Var "b4")) "being"   ($#m1_subset_1 :::"Form":::) "of" (Set (Var "V")) "," (Set (Var "W")) "holds"   (Bool  "("  (Bool (Set (Var "b4"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "f"))  ($#k3_hermitan :::"*'"::: )  )) "iff" (Bool  "for" (Set (Var "v")) "being"   ($#m1_subset_1 :::"Vector":::) "of" (Set (Var "V"))  (Bool  "for" (Set (Var "w")) "being"   ($#m1_subset_1 :::"Vector":::) "of" (Set (Var "W")) "holds"  (Bool (Set (Set (Var "b4"))  ($#k2_binop_1 :::"."::: )   "(" (Set (Var "v")) "," (Set (Var "w")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "f"))  ($#k2_binop_1 :::"."::: )   "(" (Set (Var "v")) "," (Set (Var "w")) ")"  ")" )  ($#k2_complfld :::"*'"::: )  ))))  ")" ))); 
 registrationlet "V", "W" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_vectsp_1 :::"VectSpStr"::: )   "over" (Set   ($#k1_complfld :::"F_Complex"::: )  ); let "f" be   ($#v1_bilinear :::"additiveFAF"::: )    ($#m1_subset_1 :::"Form":::) "of" (Set (Const "V")) "," (Set (Const "W")); 
cluster (Set "f"  ($#k3_hermitan :::"*'"::: )  ) ->   ($#v1_bilinear :::"additiveFAF"::: )   ; 
end; registrationlet "V", "W" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_vectsp_1 :::"VectSpStr"::: )   "over" (Set   ($#k1_complfld :::"F_Complex"::: )  ); let "f" be   ($#v2_bilinear :::"additiveSAF"::: )    ($#m1_subset_1 :::"Form":::) "of" (Set (Const "V")) "," (Set (Const "W")); 
cluster (Set "f"  ($#k3_hermitan :::"*'"::: )  ) ->   ($#v2_bilinear :::"additiveSAF"::: )   ; 
end; registrationlet "V", "W" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_vectsp_1 :::"VectSpStr"::: )   "over" (Set   ($#k1_complfld :::"F_Complex"::: )  ); let "f" be   ($#v3_bilinear :::"homogeneousFAF"::: )    ($#m1_subset_1 :::"Form":::) "of" (Set (Const "V")) "," (Set (Const "W")); 
cluster (Set "f"  ($#k3_hermitan :::"*'"::: )  ) ->   ($#v2_hermitan :::"cmplxhomogeneousFAF"::: )   ; 
end; registrationlet "V", "W" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_vectsp_1 :::"VectSpStr"::: )   "over" (Set   ($#k1_complfld :::"F_Complex"::: )  ); let "f" be   ($#v2_hermitan :::"cmplxhomogeneousFAF"::: )    ($#m1_subset_1 :::"Form":::) "of" (Set (Const "V")) "," (Set (Const "W")); 
cluster (Set "f"  ($#k3_hermitan :::"*'"::: )  ) ->   ($#v3_bilinear :::"homogeneousFAF"::: )   ; 
end; registrationlet "V", "W" be  ($#~v7_struct_0  "non"   ($#v7_struct_0 :::"trivial"::: )   )   ($#l1_vectsp_1 :::"VectSp":::) "of" (Set   ($#k1_complfld :::"F_Complex"::: )  ); let "f" be  ($#~v3_funct_1  "non"   ($#v3_funct_1 :::"constant"::: )   )   ($#m1_subset_1 :::"Form":::) "of" (Set (Const "V")) "," (Set (Const "W")); 
cluster (Set "f"  ($#k3_hermitan :::"*'"::: )  ) ->  ($#~v3_funct_1  "non"   ($#v3_funct_1 :::"constant"::: )   )  ; 
end; 
theorem :: HERMITAN:28 (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 :::"Functional":::) "of" (Set (Var "V"))  (Bool  "for" (Set (Var "v")) "being"   ($#m1_subset_1 :::"Vector":::) "of" (Set (Var "V")) "holds"  (Bool (Set (Set  "("  ($#k9_bilinear :::"FormFunctional"::: )   "(" (Set (Var "f")) "," (Set  "(" (Set (Var "f"))  ($#k1_hermitan :::"*'"::: )  ")" ) ")"  ")" )  ($#k2_binop_1 :::"."::: )   "(" (Set (Var "v")) "," (Set (Var "v")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set  ($#k17_complex1 :::"|."::: ) (Set  "(" (Set (Var "f"))  ($#k3_funct_2 :::"."::: )  (Set (Var "v")) ")" ) ($#k17_complex1 :::".|"::: ) )  ($#k5_square_1 :::"^2"::: )  ))))) ; 
 registrationlet "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 :::"Functional":::) "of" (Set (Const "V")); 
cluster (Set   ($#k9_bilinear :::"FormFunctional"::: )   "(" "f" "," (Set  "(" "f"  ($#k1_hermitan :::"*'"::: )  ")" ) ")" ) ->   ($#v3_hermitan :::"hermitan"::: )     ($#v4_hermitan :::"diagRvalued"::: )     ($#v5_hermitan :::"diagReR+0valued"::: )   ; 
end; registrationlet "V" be  ($#~v7_struct_0  "non"   ($#v7_struct_0 :::"trivial"::: )   )   ($#l1_vectsp_1 :::"VectSp":::) "of" (Set   ($#k1_complfld :::"F_Complex"::: )  ); 
cluster  ($#~v1_zfmisc_1  "non"   ($#v1_zfmisc_1 :::"trivial"::: )   )  bbbadV1_RELAT_1() bbbadV4_RELAT_1((Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "V") "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "V") ($#k2_zfmisc_1 :::":]"::: ) )) bbbadV5_RELAT_1((Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set  ($#k1_complfld :::"F_Complex"::: ) )))   ($#v1_funct_1 :::"Function-like"::: )    ($#~v3_funct_1  "non"   ($#v3_funct_1 :::"constant"::: )   )  bbbadV1_FUNCT_2((Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "V") "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "V") ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set  ($#k1_complfld :::"F_Complex"::: ) )))   ($#v1_bilinear :::"additiveFAF"::: )     ($#v2_bilinear :::"additiveSAF"::: )     ($#v4_bilinear :::"homogeneousSAF"::: )     ($#v2_hermitan :::"cmplxhomogeneousFAF"::: )     ($#v3_hermitan :::"hermitan"::: )     ($#v4_hermitan :::"diagRvalued"::: )     ($#v5_hermitan :::"diagReR+0valued"::: )    for    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k1_zfmisc_1 :::"bool"::: )  (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "V") "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "V") ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set  ($#k1_complfld :::"F_Complex"::: ) )) ($#k2_zfmisc_1 :::":]"::: ) )); 
end; 
theorem :: HERMITAN:29 (Bool  "for" (Set (Var "V")) "," (Set (Var "W")) "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 :::"Form":::) "of" (Set (Var "V")) "," (Set (Var "W")) "holds"  (Bool (Set (Set  "(" (Set (Var "f"))  ($#k3_hermitan :::"*'"::: )  ")" )  ($#k3_hermitan :::"*'"::: )  )  ($#r2_funct_2 :::"="::: )  (Set (Var "f"))))) ; 
 
theorem :: HERMITAN:30 (Bool  "for" (Set (Var "V")) "," (Set (Var "W")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_vectsp_1 :::"VectSpStr"::: )   "over" (Set   ($#k1_complfld :::"F_Complex"::: )  ) "holds"  (Bool (Set (Set  "("  ($#k1_bilinear :::"NulForm"::: )   "(" (Set (Var "V")) "," (Set (Var "W")) ")"  ")" )  ($#k3_hermitan :::"*'"::: )  )  ($#r2_funct_2 :::"="::: )  (Set   ($#k1_bilinear :::"NulForm"::: )   "(" (Set (Var "V")) "," (Set (Var "W")) ")" ))) ; 
 
theorem :: HERMITAN:31 (Bool  "for" (Set (Var "V")) "," (Set (Var "W")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_vectsp_1 :::"VectSpStr"::: )   "over" (Set   ($#k1_complfld :::"F_Complex"::: )  )  (Bool  "for" (Set (Var "f")) "," (Set (Var "g")) "being"   ($#m1_subset_1 :::"Form":::) "of" (Set (Var "V")) "," (Set (Var "W")) "holds"  (Bool (Set (Set  "(" (Set (Var "f"))  ($#k6_bilinear :::"+"::: )  (Set (Var "g")) ")" )  ($#k3_hermitan :::"*'"::: )  )  ($#r2_funct_2 :::"="::: )  (Set (Set  "(" (Set (Var "f"))  ($#k3_hermitan :::"*'"::: )  ")" )  ($#k6_bilinear :::"+"::: )  (Set  "(" (Set (Var "g"))  ($#k3_hermitan :::"*'"::: )  ")" ))))) ; 
 
theorem :: HERMITAN:32 (Bool  "for" (Set (Var "V")) "," (Set (Var "W")) "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 :::"Form":::) "of" (Set (Var "V")) "," (Set (Var "W")) "holds"  (Bool (Set (Set  "("  ($#k4_bilinear :::"-"::: )  (Set (Var "f")) ")" )  ($#k3_hermitan :::"*'"::: )  )  ($#r2_funct_2 :::"="::: )  (Set   ($#k4_bilinear :::"-"::: )  (Set  "(" (Set (Var "f"))  ($#k3_hermitan :::"*'"::: )  ")" ))))) ; 
 
theorem :: HERMITAN:33 (Bool  "for" (Set (Var "V")) "," (Set (Var "W")) "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 :::"Form":::) "of" (Set (Var "V")) "," (Set (Var "W"))  (Bool  "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set  ($#k1_complfld :::"F_Complex"::: ) ) "holds"  (Bool (Set (Set  "(" (Set (Var "a"))  ($#k3_bilinear :::"*"::: )  (Set (Var "f")) ")" )  ($#k3_hermitan :::"*'"::: )  )  ($#r2_funct_2 :::"="::: )  (Set (Set  "(" (Set (Var "a"))  ($#k2_complfld :::"*'"::: )  ")" )  ($#k3_bilinear :::"*"::: )  (Set  "(" (Set (Var "f"))  ($#k3_hermitan :::"*'"::: )  ")" )))))) ; 
 
theorem :: HERMITAN:34 (Bool  "for" (Set (Var "V")) "," (Set (Var "W")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_vectsp_1 :::"VectSpStr"::: )   "over" (Set   ($#k1_complfld :::"F_Complex"::: )  )  (Bool  "for" (Set (Var "f")) "," (Set (Var "g")) "being"   ($#m1_subset_1 :::"Form":::) "of" (Set (Var "V")) "," (Set (Var "W")) "holds"  (Bool (Set (Set  "(" (Set (Var "f"))  ($#k5_bilinear :::"-"::: )  (Set (Var "g")) ")" )  ($#k3_hermitan :::"*'"::: )  )  ($#r2_funct_2 :::"="::: )  (Set (Set  "(" (Set (Var "f"))  ($#k3_hermitan :::"*'"::: )  ")" )  ($#k5_bilinear :::"-"::: )  (Set  "(" (Set (Var "g"))  ($#k3_hermitan :::"*'"::: )  ")" ))))) ; 
 
theorem :: HERMITAN:35 (Bool  "for" (Set (Var "V")) "," (Set (Var "W")) "being"   ($#l1_vectsp_1 :::"VectSp":::) "of" (Set   ($#k1_complfld :::"F_Complex"::: )  )  (Bool  "for" (Set (Var "v")) "being"   ($#m1_subset_1 :::"Vector":::) "of" (Set (Var "V"))  (Bool  "for" (Set (Var "w")) "," (Set (Var "t")) "being"   ($#m1_subset_1 :::"Vector":::) "of" (Set (Var "W"))  (Bool  "for" (Set (Var "f")) "being"   ($#v1_bilinear :::"additiveFAF"::: )     ($#v2_hermitan :::"cmplxhomogeneousFAF"::: )    ($#m1_subset_1 :::"Form":::) "of" (Set (Var "V")) "," (Set (Var "W")) "holds"  (Bool (Set (Set (Var "f"))  ($#k2_binop_1 :::"."::: )   "(" (Set (Var "v")) "," (Set  "(" (Set (Var "w"))  ($#k5_algstr_0 :::"-"::: )  (Set (Var "t")) ")" ) ")" )  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "f"))  ($#k2_binop_1 :::"."::: )   "(" (Set (Var "v")) "," (Set (Var "w")) ")"  ")" )  ($#k5_algstr_0 :::"-"::: )  (Set  "(" (Set (Var "f"))  ($#k2_binop_1 :::"."::: )   "(" (Set (Var "v")) "," (Set (Var "t")) ")"  ")" ))))))) ; 
 
theorem :: HERMITAN:36 (Bool  "for" (Set (Var "V")) "," (Set (Var "W")) "being"   ($#l1_vectsp_1 :::"VectSp":::) "of" (Set   ($#k1_complfld :::"F_Complex"::: )  )  (Bool  "for" (Set (Var "v")) "," (Set (Var "u")) "being"   ($#m1_subset_1 :::"Vector":::) "of" (Set (Var "V"))  (Bool  "for" (Set (Var "w")) "," (Set (Var "t")) "being"   ($#m1_subset_1 :::"Vector":::) "of" (Set (Var "W"))  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"sesquilinear-Form":::) "of" (Set (Var "V")) "," (Set (Var "W")) "holds"  (Bool (Set (Set (Var "f"))  ($#k2_binop_1 :::"."::: )   "(" (Set  "(" (Set (Var "v"))  ($#k5_algstr_0 :::"-"::: )  (Set (Var "u")) ")" ) "," (Set  "(" (Set (Var "w"))  ($#k5_algstr_0 :::"-"::: )  (Set (Var "t")) ")" ) ")" )  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set (Var "f"))  ($#k2_binop_1 :::"."::: )   "(" (Set (Var "v")) "," (Set (Var "w")) ")"  ")" )  ($#k5_algstr_0 :::"-"::: )  (Set  "(" (Set (Var "f"))  ($#k2_binop_1 :::"."::: )   "(" (Set (Var "v")) "," (Set (Var "t")) ")"  ")" ) ")" )  ($#k5_algstr_0 :::"-"::: )  (Set  "(" (Set  "(" (Set (Var "f"))  ($#k2_binop_1 :::"."::: )   "(" (Set (Var "u")) "," (Set (Var "w")) ")"  ")" )  ($#k5_algstr_0 :::"-"::: )  (Set  "(" (Set (Var "f"))  ($#k2_binop_1 :::"."::: )   "(" (Set (Var "u")) "," (Set (Var "t")) ")"  ")" ) ")" ))))))) ; 
 
theorem :: HERMITAN:37 (Bool  "for" (Set (Var "V")) "," (Set (Var "W")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v13_algstr_0 :::"right_complementable"::: )     ($#v3_rlvect_1 :::"add-associative"::: )     ($#v4_rlvect_1 :::"right_zeroed"::: )     ($#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 "v")) "," (Set (Var "u")) "being"   ($#m1_subset_1 :::"Vector":::) "of" (Set (Var "V"))  (Bool  "for" (Set (Var "w")) "," (Set (Var "t")) "being"   ($#m1_subset_1 :::"Vector":::) "of" (Set (Var "W"))  (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set  ($#k1_complfld :::"F_Complex"::: ) )  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"sesquilinear-Form":::) "of" (Set (Var "V")) "," (Set (Var "W")) "holds"  (Bool (Set (Set (Var "f"))  ($#k2_binop_1 :::"."::: )   "(" (Set  "(" (Set (Var "v"))  ($#k1_algstr_0 :::"+"::: )  (Set  "(" (Set (Var "a"))  ($#k4_vectsp_1 :::"*"::: )  (Set (Var "u")) ")" ) ")" ) "," (Set  "(" (Set (Var "w"))  ($#k1_algstr_0 :::"+"::: )  (Set  "(" (Set (Var "b"))  ($#k4_vectsp_1 :::"*"::: )  (Set (Var "t")) ")" ) ")" ) ")" )  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set (Var "f"))  ($#k2_binop_1 :::"."::: )   "(" (Set (Var "v")) "," (Set (Var "w")) ")"  ")" )  ($#k3_rlvect_1 :::"+"::: )  (Set  "(" (Set  "(" (Set (Var "b"))  ($#k2_complfld :::"*'"::: )  ")" )  ($#k8_group_1 :::"*"::: )  (Set  "(" (Set (Var "f"))  ($#k2_binop_1 :::"."::: )   "(" (Set (Var "v")) "," (Set (Var "t")) ")"  ")" ) ")" ) ")" )  ($#k3_rlvect_1 :::"+"::: )  (Set  "(" (Set  "(" (Set (Var "a"))  ($#k8_group_1 :::"*"::: )  (Set  "(" (Set (Var "f"))  ($#k2_binop_1 :::"."::: )   "(" (Set (Var "u")) "," (Set (Var "w")) ")"  ")" ) ")" )  ($#k3_rlvect_1 :::"+"::: )  (Set  "(" (Set (Var "a"))  ($#k8_group_1 :::"*"::: )  (Set  "(" (Set  "(" (Set (Var "b"))  ($#k2_complfld :::"*'"::: )  ")" )  ($#k8_group_1 :::"*"::: )  (Set  "(" (Set (Var "f"))  ($#k2_binop_1 :::"."::: )   "(" (Set (Var "u")) "," (Set (Var "t")) ")"  ")" ) ")" ) ")" ) ")" )))))))) ; 
 
theorem :: HERMITAN:38 (Bool  "for" (Set (Var "V")) "," (Set (Var "W")) "being"   ($#l1_vectsp_1 :::"VectSp":::) "of" (Set   ($#k1_complfld :::"F_Complex"::: )  )  (Bool  "for" (Set (Var "v")) "," (Set (Var "u")) "being"   ($#m1_subset_1 :::"Vector":::) "of" (Set (Var "V"))  (Bool  "for" (Set (Var "w")) "," (Set (Var "t")) "being"   ($#m1_subset_1 :::"Vector":::) "of" (Set (Var "W"))  (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set  ($#k1_complfld :::"F_Complex"::: ) )  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"sesquilinear-Form":::) "of" (Set (Var "V")) "," (Set (Var "W")) "holds"  (Bool (Set (Set (Var "f"))  ($#k2_binop_1 :::"."::: )   "(" (Set  "(" (Set (Var "v"))  ($#k5_algstr_0 :::"-"::: )  (Set  "(" (Set (Var "a"))  ($#k4_vectsp_1 :::"*"::: )  (Set (Var "u")) ")" ) ")" ) "," (Set  "(" (Set (Var "w"))  ($#k5_algstr_0 :::"-"::: )  (Set  "(" (Set (Var "b"))  ($#k4_vectsp_1 :::"*"::: )  (Set (Var "t")) ")" ) ")" ) ")" )  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set (Var "f"))  ($#k2_binop_1 :::"."::: )   "(" (Set (Var "v")) "," (Set (Var "w")) ")"  ")" )  ($#k5_algstr_0 :::"-"::: )  (Set  "(" (Set  "(" (Set (Var "b"))  ($#k2_complfld :::"*'"::: )  ")" )  ($#k8_group_1 :::"*"::: )  (Set  "(" (Set (Var "f"))  ($#k2_binop_1 :::"."::: )   "(" (Set (Var "v")) "," (Set (Var "t")) ")"  ")" ) ")" ) ")" )  ($#k5_algstr_0 :::"-"::: )  (Set  "(" (Set  "(" (Set (Var "a"))  ($#k8_group_1 :::"*"::: )  (Set  "(" (Set (Var "f"))  ($#k2_binop_1 :::"."::: )   "(" (Set (Var "u")) "," (Set (Var "w")) ")"  ")" ) ")" )  ($#k5_algstr_0 :::"-"::: )  (Set  "(" (Set (Var "a"))  ($#k8_group_1 :::"*"::: )  (Set  "(" (Set  "(" (Set (Var "b"))  ($#k2_complfld :::"*'"::: )  ")" )  ($#k8_group_1 :::"*"::: )  (Set  "(" (Set (Var "f"))  ($#k2_binop_1 :::"."::: )   "(" (Set (Var "u")) "," (Set (Var "t")) ")"  ")" ) ")" ) ")" ) ")" )))))))) ; 
 
theorem :: HERMITAN:39 (Bool  "for" (Set (Var "V")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v13_algstr_0 :::"right_complementable"::: )     ($#v3_rlvect_1 :::"add-associative"::: )     ($#v4_rlvect_1 :::"right_zeroed"::: )     ($#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"   ($#v2_hermitan :::"cmplxhomogeneousFAF"::: )    ($#m1_subset_1 :::"Form":::) "of" (Set (Var "V")) "," (Set (Var "V"))  (Bool  "for" (Set (Var "v")) "being"   ($#m1_subset_1 :::"Vector":::) "of" (Set (Var "V")) "holds"  (Bool (Set (Set (Var "f"))  ($#k2_binop_1 :::"."::: )   "(" (Set (Var "v")) "," (Set  "("  ($#k4_struct_0 :::"0."::: )  (Set (Var "V")) ")" ) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k4_struct_0 :::"0."::: )  (Set  ($#k1_complfld :::"F_Complex"::: ) )))))) ; 
 
theorem :: HERMITAN:40 (Bool  "for" (Set (Var "V")) "being"   ($#l1_vectsp_1 :::"VectSp":::) "of" (Set   ($#k1_complfld :::"F_Complex"::: )  )  (Bool  "for" (Set (Var "v")) "," (Set (Var "w")) "being"   ($#m1_subset_1 :::"Vector":::) "of" (Set (Var "V"))  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"hermitan-Form":::) "of" (Set (Var "V")) "holds"  (Bool (Set (Set  "(" (Set  "(" (Set  "(" (Set (Var "f"))  ($#k2_binop_1 :::"."::: )   "(" (Set (Var "v")) "," (Set (Var "w")) ")"  ")" )  ($#k3_rlvect_1 :::"+"::: )  (Set  "(" (Set (Var "f"))  ($#k2_binop_1 :::"."::: )   "(" (Set (Var "v")) "," (Set (Var "w")) ")"  ")" ) ")" )  ($#k3_rlvect_1 :::"+"::: )  (Set  "(" (Set (Var "f"))  ($#k2_binop_1 :::"."::: )   "(" (Set (Var "v")) "," (Set (Var "w")) ")"  ")" ) ")" )  ($#k3_rlvect_1 :::"+"::: )  (Set  "(" (Set (Var "f"))  ($#k2_binop_1 :::"."::: )   "(" (Set (Var "v")) "," (Set (Var "w")) ")"  ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set  "(" (Set (Var "f"))  ($#k2_binop_1 :::"."::: )   "(" (Set  "(" (Set (Var "v"))  ($#k3_rlvect_1 :::"+"::: )  (Set (Var "w")) ")" ) "," (Set  "(" (Set (Var "v"))  ($#k3_rlvect_1 :::"+"::: )  (Set (Var "w")) ")" ) ")"  ")" )  ($#k5_algstr_0 :::"-"::: )  (Set  "(" (Set (Var "f"))  ($#k2_binop_1 :::"."::: )   "(" (Set  "(" (Set (Var "v"))  ($#k5_algstr_0 :::"-"::: )  (Set (Var "w")) ")" ) "," (Set  "(" (Set (Var "v"))  ($#k5_algstr_0 :::"-"::: )  (Set (Var "w")) ")" ) ")"  ")" ) ")" )  ($#k3_rlvect_1 :::"+"::: )  (Set  "(" (Set  ($#k2_hahnban1 :::"i_FC"::: ) )  ($#k8_group_1 :::"*"::: )  (Set  "(" (Set (Var "f"))  ($#k2_binop_1 :::"."::: )   "(" (Set  "(" (Set (Var "v"))  ($#k3_rlvect_1 :::"+"::: )  (Set  "(" (Set  ($#k2_hahnban1 :::"i_FC"::: ) )  ($#k4_vectsp_1 :::"*"::: )  (Set (Var "w")) ")" ) ")" ) "," (Set  "(" (Set (Var "v"))  ($#k3_rlvect_1 :::"+"::: )  (Set  "(" (Set  ($#k2_hahnban1 :::"i_FC"::: ) )  ($#k4_vectsp_1 :::"*"::: )  (Set (Var "w")) ")" ) ")" ) ")"  ")" ) ")" ) ")" )  ($#k5_algstr_0 :::"-"::: )  (Set  "(" (Set  ($#k2_hahnban1 :::"i_FC"::: ) )  ($#k8_group_1 :::"*"::: )  (Set  "(" (Set (Var "f"))  ($#k2_binop_1 :::"."::: )   "(" (Set  "(" (Set (Var "v"))  ($#k5_algstr_0 :::"-"::: )  (Set  "(" (Set  ($#k2_hahnban1 :::"i_FC"::: ) )  ($#k4_vectsp_1 :::"*"::: )  (Set (Var "w")) ")" ) ")" ) "," (Set  "(" (Set (Var "v"))  ($#k5_algstr_0 :::"-"::: )  (Set  "(" (Set  ($#k2_hahnban1 :::"i_FC"::: ) )  ($#k4_vectsp_1 :::"*"::: )  (Set (Var "w")) ")" ) ")" ) ")"  ")" ) ")" )))))) ; 
 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 :::"Form":::) "of" (Set (Const "V")) "," (Set (Const "V")); let "v" be   ($#m1_subset_1 :::"Vector":::) "of" (Set (Const "V")); func  :::"signnorm":::  "(" "f" "," "v" ")"  ->   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )   equals :: HERMITAN:def 9 (Set   ($#k3_complex1 :::"Re"::: )  (Set  "(" "f"  ($#k2_binop_1 :::"."::: )   "(" "v" "," "v" ")"  ")" )); end; 







:: deftheorem    defines :::"signnorm"::: HERMITAN:def 9 :  (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 :::"Form":::) "of" (Set (Var "V")) "," (Set (Var "V"))  (Bool  "for" (Set (Var "v")) "being"   ($#m1_subset_1 :::"Vector":::) "of" (Set (Var "V")) "holds"  (Bool (Set   ($#k4_hermitan :::"signnorm"::: )   "(" (Set (Var "f")) "," (Set (Var "v")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k3_complex1 :::"Re"::: )  (Set  "(" (Set (Var "f"))  ($#k2_binop_1 :::"."::: )   "(" (Set (Var "v")) "," (Set (Var "v")) ")"  ")" )))))); 
 
theorem :: HERMITAN:41 (Bool  "for" (Set (Var "V")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v13_algstr_0 :::"right_complementable"::: )     ($#v3_rlvect_1 :::"add-associative"::: )     ($#v4_rlvect_1 :::"right_zeroed"::: )     ($#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"   ($#v4_hermitan :::"diagRvalued"::: )     ($#v5_hermitan :::"diagReR+0valued"::: )    ($#m1_subset_1 :::"Form":::) "of" (Set (Var "V")) "," (Set (Var "V"))  (Bool  "for" (Set (Var "v")) "being"   ($#m1_subset_1 :::"Vector":::) "of" (Set (Var "V")) "holds"   (Bool  "("  (Bool (Set  ($#k17_complex1 :::"|."::: ) (Set  "(" (Set (Var "f"))  ($#k2_binop_1 :::"."::: )   "(" (Set (Var "v")) "," (Set (Var "v")) ")"  ")" ) ($#k17_complex1 :::".|"::: ) )  ($#r1_hidden :::"="::: )  (Set   ($#k3_complex1 :::"Re"::: )  (Set  "(" (Set (Var "f"))  ($#k2_binop_1 :::"."::: )   "(" (Set (Var "v")) "," (Set (Var "v")) ")"  ")" ))) & (Bool (Set   ($#k4_hermitan :::"signnorm"::: )   "(" (Set (Var "f")) "," (Set (Var "v")) ")" )  ($#r1_hidden :::"="::: )  (Set  ($#k17_complex1 :::"|."::: ) (Set  "(" (Set (Var "f"))  ($#k2_binop_1 :::"."::: )   "(" (Set (Var "v")) "," (Set (Var "v")) ")"  ")" ) ($#k17_complex1 :::".|"::: ) ))  ")" )))) ; 
 
theorem :: HERMITAN:42 (Bool  "for" (Set (Var "V")) "being"   ($#l1_vectsp_1 :::"VectSp":::) "of" (Set   ($#k1_complfld :::"F_Complex"::: )  )  (Bool  "for" (Set (Var "v")) "," (Set (Var "w")) "being"   ($#m1_subset_1 :::"Vector":::) "of" (Set (Var "V"))  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"sesquilinear-Form":::) "of" (Set (Var "V")) "," (Set (Var "V"))  (Bool  "for" (Set (Var "r")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    (Bool  "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set  ($#k1_complfld :::"F_Complex"::: ) )  "st" (Bool (Bool (Set  ($#k17_complex1 :::"|."::: ) (Set (Var "a")) ($#k17_complex1 :::".|"::: ) )  ($#r1_hidden :::"="::: )  (Num 1))) "holds"  (Bool (Set (Set (Var "f"))  ($#k2_binop_1 :::"."::: )   "(" (Set  "(" (Set (Var "v"))  ($#k5_algstr_0 :::"-"::: )  (Set  "(" (Set  "(" (Set  ($#k1_hahnban1 :::"[**"::: ) (Set (Var "r")) "," (Set  ($#k6_numbers :::"0"::: ) ) ($#k1_hahnban1 :::"**]"::: ) )  ($#k8_group_1 :::"*"::: )  (Set (Var "a")) ")" )  ($#k4_vectsp_1 :::"*"::: )  (Set (Var "w")) ")" ) ")" ) "," (Set  "(" (Set (Var "v"))  ($#k5_algstr_0 :::"-"::: )  (Set  "(" (Set  "(" (Set  ($#k1_hahnban1 :::"[**"::: ) (Set (Var "r")) "," (Set  ($#k6_numbers :::"0"::: ) ) ($#k1_hahnban1 :::"**]"::: ) )  ($#k8_group_1 :::"*"::: )  (Set (Var "a")) ")" )  ($#k4_vectsp_1 :::"*"::: )  (Set (Var "w")) ")" ) ")" ) ")" )  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set  "(" (Set (Var "f"))  ($#k2_binop_1 :::"."::: )   "(" (Set (Var "v")) "," (Set (Var "v")) ")"  ")" )  ($#k5_algstr_0 :::"-"::: )  (Set  "(" (Set  ($#k1_hahnban1 :::"[**"::: ) (Set (Var "r")) "," (Set  ($#k6_numbers :::"0"::: ) ) ($#k1_hahnban1 :::"**]"::: ) )  ($#k8_group_1 :::"*"::: )  (Set  "(" (Set (Var "a"))  ($#k8_group_1 :::"*"::: )  (Set  "(" (Set (Var "f"))  ($#k2_binop_1 :::"."::: )   "(" (Set (Var "w")) "," (Set (Var "v")) ")"  ")" ) ")" ) ")" ) ")" )  ($#k5_algstr_0 :::"-"::: )  (Set  "(" (Set  ($#k1_hahnban1 :::"[**"::: ) (Set (Var "r")) "," (Set  ($#k6_numbers :::"0"::: ) ) ($#k1_hahnban1 :::"**]"::: ) )  ($#k8_group_1 :::"*"::: )  (Set  "(" (Set  "(" (Set (Var "a"))  ($#k2_complfld :::"*'"::: )  ")" )  ($#k8_group_1 :::"*"::: )  (Set  "(" (Set (Var "f"))  ($#k2_binop_1 :::"."::: )   "(" (Set (Var "v")) "," (Set (Var "w")) ")"  ")" ) ")" ) ")" ) ")" )  ($#k3_rlvect_1 :::"+"::: )  (Set  "(" (Set  ($#k1_hahnban1 :::"[**"::: ) (Set  "(" (Set (Var "r"))  ($#k3_square_1 :::"^2"::: )  ")" ) "," (Set  ($#k6_numbers :::"0"::: ) ) ($#k1_hahnban1 :::"**]"::: ) )  ($#k8_group_1 :::"*"::: )  (Set  "(" (Set (Var "f"))  ($#k2_binop_1 :::"."::: )   "(" (Set (Var "w")) "," (Set (Var "w")) ")"  ")" ) ")" )))))))) ; 
 
theorem :: HERMITAN:43 (Bool  "for" (Set (Var "V")) "being"   ($#l1_vectsp_1 :::"VectSp":::) "of" (Set   ($#k1_complfld :::"F_Complex"::: )  )  (Bool  "for" (Set (Var "v")) "," (Set (Var "w")) "being"   ($#m1_subset_1 :::"Vector":::) "of" (Set (Var "V"))  (Bool  "for" (Set (Var "f")) "being"   ($#v5_hermitan :::"diagReR+0valued"::: )    ($#m1_subset_1 :::"hermitan-Form":::) "of" (Set (Var "V"))  (Bool  "for" (Set (Var "r")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    (Bool  "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set  ($#k1_complfld :::"F_Complex"::: ) )  "st" (Bool (Bool (Set  ($#k17_complex1 :::"|."::: ) (Set (Var "a")) ($#k17_complex1 :::".|"::: ) )  ($#r1_hidden :::"="::: )  (Num 1)) & (Bool (Set   ($#k3_complex1 :::"Re"::: )  (Set  "(" (Set (Var "a"))  ($#k8_group_1 :::"*"::: )  (Set  "(" (Set (Var "f"))  ($#k2_binop_1 :::"."::: )   "(" (Set (Var "w")) "," (Set (Var "v")) ")"  ")" ) ")" ))  ($#r1_hidden :::"="::: )  (Set  ($#k17_complex1 :::"|."::: ) (Set  "(" (Set (Var "f"))  ($#k2_binop_1 :::"."::: )   "(" (Set (Var "w")) "," (Set (Var "v")) ")"  ")" ) ($#k17_complex1 :::".|"::: ) ))) "holds"  (Bool  "("  (Bool (Set   ($#k3_complex1 :::"Re"::: )  (Set  "(" (Set (Var "f"))  ($#k2_binop_1 :::"."::: )   "(" (Set  "(" (Set (Var "v"))  ($#k5_algstr_0 :::"-"::: )  (Set  "(" (Set  "(" (Set  ($#k1_hahnban1 :::"[**"::: ) (Set (Var "r")) "," (Set  ($#k6_numbers :::"0"::: ) ) ($#k1_hahnban1 :::"**]"::: ) )  ($#k8_group_1 :::"*"::: )  (Set (Var "a")) ")" )  ($#k4_vectsp_1 :::"*"::: )  (Set (Var "w")) ")" ) ")" ) "," (Set  "(" (Set (Var "v"))  ($#k5_algstr_0 :::"-"::: )  (Set  "(" (Set  "(" (Set  ($#k1_hahnban1 :::"[**"::: ) (Set (Var "r")) "," (Set  ($#k6_numbers :::"0"::: ) ) ($#k1_hahnban1 :::"**]"::: ) )  ($#k8_group_1 :::"*"::: )  (Set (Var "a")) ")" )  ($#k4_vectsp_1 :::"*"::: )  (Set (Var "w")) ")" ) ")" ) ")"  ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "("  ($#k4_hermitan :::"signnorm"::: )   "(" (Set (Var "f")) "," (Set (Var "v")) ")"  ")" )  ($#k5_real_1 :::"-"::: )  (Set  "(" (Set  "(" (Num 2)  ($#k8_real_1 :::"*"::: )  (Set  ($#k17_complex1 :::"|."::: ) (Set  "(" (Set (Var "f"))  ($#k2_binop_1 :::"."::: )   "(" (Set (Var "w")) "," (Set (Var "v")) ")"  ")" ) ($#k17_complex1 :::".|"::: ) ) ")" )  ($#k8_real_1 :::"*"::: )  (Set (Var "r")) ")" ) ")" )  ($#k7_real_1 :::"+"::: )  (Set  "(" (Set  "("  ($#k4_hermitan :::"signnorm"::: )   "(" (Set (Var "f")) "," (Set (Var "w")) ")"  ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set  "(" (Set (Var "r"))  ($#k3_square_1 :::"^2"::: )  ")" ) ")" ))) & (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<="::: )  (Set (Set  "(" (Set  "("  ($#k4_hermitan :::"signnorm"::: )   "(" (Set (Var "f")) "," (Set (Var "v")) ")"  ")" )  ($#k5_real_1 :::"-"::: )  (Set  "(" (Set  "(" (Num 2)  ($#k8_real_1 :::"*"::: )  (Set  ($#k17_complex1 :::"|."::: ) (Set  "(" (Set (Var "f"))  ($#k2_binop_1 :::"."::: )   "(" (Set (Var "w")) "," (Set (Var "v")) ")"  ")" ) ($#k17_complex1 :::".|"::: ) ) ")" )  ($#k8_real_1 :::"*"::: )  (Set (Var "r")) ")" ) ")" )  ($#k7_real_1 :::"+"::: )  (Set  "(" (Set  "("  ($#k4_hermitan :::"signnorm"::: )   "(" (Set (Var "f")) "," (Set (Var "w")) ")"  ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set  "(" (Set (Var "r"))  ($#k3_square_1 :::"^2"::: )  ")" ) ")" )))  ")" )))))) ; 
 
theorem :: HERMITAN:44 (Bool  "for" (Set (Var "V")) "being"   ($#l1_vectsp_1 :::"VectSp":::) "of" (Set   ($#k1_complfld :::"F_Complex"::: )  )  (Bool  "for" (Set (Var "v")) "," (Set (Var "w")) "being"   ($#m1_subset_1 :::"Vector":::) "of" (Set (Var "V"))  (Bool  "for" (Set (Var "f")) "being"   ($#v5_hermitan :::"diagReR+0valued"::: )    ($#m1_subset_1 :::"hermitan-Form":::) "of" (Set (Var "V"))  "st" (Bool (Bool (Set   ($#k4_hermitan :::"signnorm"::: )   "(" (Set (Var "f")) "," (Set (Var "w")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set  ($#k17_complex1 :::"|."::: ) (Set  "(" (Set (Var "f"))  ($#k2_binop_1 :::"."::: )   "(" (Set (Var "w")) "," (Set (Var "v")) ")"  ")" ) ($#k17_complex1 :::".|"::: ) )  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))))) ; 
 
theorem :: HERMITAN:45 (Bool  "for" (Set (Var "V")) "being"   ($#l1_vectsp_1 :::"VectSp":::) "of" (Set   ($#k1_complfld :::"F_Complex"::: )  )  (Bool  "for" (Set (Var "v")) "," (Set (Var "w")) "being"   ($#m1_subset_1 :::"Vector":::) "of" (Set (Var "V"))  (Bool  "for" (Set (Var "f")) "being"   ($#v5_hermitan :::"diagReR+0valued"::: )    ($#m1_subset_1 :::"hermitan-Form":::) "of" (Set (Var "V")) "holds"  (Bool (Set (Set  ($#k17_complex1 :::"|."::: ) (Set  "(" (Set (Var "f"))  ($#k2_binop_1 :::"."::: )   "(" (Set (Var "v")) "," (Set (Var "w")) ")"  ")" ) ($#k17_complex1 :::".|"::: ) )  ($#k5_square_1 :::"^2"::: )  )  ($#r1_xxreal_0 :::"<="::: )  (Set (Set  "("  ($#k4_hermitan :::"signnorm"::: )   "(" (Set (Var "f")) "," (Set (Var "v")) ")"  ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set  "("  ($#k4_hermitan :::"signnorm"::: )   "(" (Set (Var "f")) "," (Set (Var "w")) ")"  ")" )))))) ; 
 
theorem :: HERMITAN:46 (Bool  "for" (Set (Var "V")) "being"   ($#l1_vectsp_1 :::"VectSp":::) "of" (Set   ($#k1_complfld :::"F_Complex"::: )  )  (Bool  "for" (Set (Var "f")) "being"   ($#v5_hermitan :::"diagReR+0valued"::: )    ($#m1_subset_1 :::"hermitan-Form":::) "of" (Set (Var "V"))  (Bool  "for" (Set (Var "v")) "," (Set (Var "w")) "being"   ($#m1_subset_1 :::"Vector":::) "of" (Set (Var "V")) "holds"  (Bool (Set (Set  ($#k17_complex1 :::"|."::: ) (Set  "(" (Set (Var "f"))  ($#k2_binop_1 :::"."::: )   "(" (Set (Var "v")) "," (Set (Var "w")) ")"  ")" ) ($#k17_complex1 :::".|"::: ) )  ($#k5_square_1 :::"^2"::: )  )  ($#r1_xxreal_0 :::"<="::: )  (Set (Set  ($#k17_complex1 :::"|."::: ) (Set  "(" (Set (Var "f"))  ($#k2_binop_1 :::"."::: )   "(" (Set (Var "v")) "," (Set (Var "v")) ")"  ")" ) ($#k17_complex1 :::".|"::: ) )  ($#k8_real_1 :::"*"::: )  (Set  ($#k17_complex1 :::"|."::: ) (Set  "(" (Set (Var "f"))  ($#k2_binop_1 :::"."::: )   "(" (Set (Var "w")) "," (Set (Var "w")) ")"  ")" ) ($#k17_complex1 :::".|"::: ) )))))) ; 
 
theorem :: HERMITAN:47 (Bool  "for" (Set (Var "V")) "being"   ($#l1_vectsp_1 :::"VectSp":::) "of" (Set   ($#k1_complfld :::"F_Complex"::: )  )  (Bool  "for" (Set (Var "f")) "being"   ($#v5_hermitan :::"diagReR+0valued"::: )    ($#m1_subset_1 :::"hermitan-Form":::) "of" (Set (Var "V"))  (Bool  "for" (Set (Var "v")) "," (Set (Var "w")) "being"   ($#m1_subset_1 :::"Vector":::) "of" (Set (Var "V")) "holds"  (Bool (Set   ($#k4_hermitan :::"signnorm"::: )   "(" (Set (Var "f")) "," (Set  "(" (Set (Var "v"))  ($#k3_rlvect_1 :::"+"::: )  (Set (Var "w")) ")" ) ")" )  ($#r1_xxreal_0 :::"<="::: )  (Set (Set  "(" (Set  "("  ($#k6_square_1 :::"sqrt"::: )  (Set  "("  ($#k4_hermitan :::"signnorm"::: )   "(" (Set (Var "f")) "," (Set (Var "v")) ")"  ")" ) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "("  ($#k6_square_1 :::"sqrt"::: )  (Set  "("  ($#k4_hermitan :::"signnorm"::: )   "(" (Set (Var "f")) "," (Set (Var "w")) ")"  ")" ) ")" ) ")" )  ($#k3_square_1 :::"^2"::: )  ))))) ; 
 
theorem :: HERMITAN:48 (Bool  "for" (Set (Var "V")) "being"   ($#l1_vectsp_1 :::"VectSp":::) "of" (Set   ($#k1_complfld :::"F_Complex"::: )  )  (Bool  "for" (Set (Var "f")) "being"   ($#v5_hermitan :::"diagReR+0valued"::: )    ($#m1_subset_1 :::"hermitan-Form":::) "of" (Set (Var "V"))  (Bool  "for" (Set (Var "v")) "," (Set (Var "w")) "being"   ($#m1_subset_1 :::"Vector":::) "of" (Set (Var "V")) "holds"  (Bool (Set  ($#k17_complex1 :::"|."::: ) (Set  "(" (Set (Var "f"))  ($#k2_binop_1 :::"."::: )   "(" (Set  "(" (Set (Var "v"))  ($#k3_rlvect_1 :::"+"::: )  (Set (Var "w")) ")" ) "," (Set  "(" (Set (Var "v"))  ($#k3_rlvect_1 :::"+"::: )  (Set (Var "w")) ")" ) ")"  ")" ) ($#k17_complex1 :::".|"::: ) )  ($#r1_xxreal_0 :::"<="::: )  (Set (Set  "(" (Set  "("  ($#k7_square_1 :::"sqrt"::: )  (Set  ($#k17_complex1 :::"|."::: ) (Set  "(" (Set (Var "f"))  ($#k2_binop_1 :::"."::: )   "(" (Set (Var "v")) "," (Set (Var "v")) ")"  ")" ) ($#k17_complex1 :::".|"::: ) ) ")" )  ($#k7_real_1 :::"+"::: )  (Set  "("  ($#k7_square_1 :::"sqrt"::: )  (Set  ($#k17_complex1 :::"|."::: ) (Set  "(" (Set (Var "f"))  ($#k2_binop_1 :::"."::: )   "(" (Set (Var "w")) "," (Set (Var "w")) ")"  ")" ) ($#k17_complex1 :::".|"::: ) ) ")" ) ")" )  ($#k5_square_1 :::"^2"::: )  ))))) ; 
 
theorem :: HERMITAN:49 (Bool  "for" (Set (Var "V")) "being"   ($#l1_vectsp_1 :::"VectSp":::) "of" (Set   ($#k1_complfld :::"F_Complex"::: )  )  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"hermitan-Form":::) "of" (Set (Var "V"))  (Bool  "for" (Set (Var "v")) "," (Set (Var "w")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "V")) "holds"  (Bool (Set (Set  "("  ($#k4_hermitan :::"signnorm"::: )   "(" (Set (Var "f")) "," (Set  "(" (Set (Var "v"))  ($#k3_rlvect_1 :::"+"::: )  (Set (Var "w")) ")" ) ")"  ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "("  ($#k4_hermitan :::"signnorm"::: )   "(" (Set (Var "f")) "," (Set  "(" (Set (Var "v"))  ($#k5_algstr_0 :::"-"::: )  (Set (Var "w")) ")" ) ")"  ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Num 2)  ($#k8_real_1 :::"*"::: )  (Set  "("  ($#k4_hermitan :::"signnorm"::: )   "(" (Set (Var "f")) "," (Set (Var "v")) ")"  ")" ) ")" )  ($#k7_real_1 :::"+"::: )  (Set  "(" (Num 2)  ($#k8_real_1 :::"*"::: )  (Set  "("  ($#k4_hermitan :::"signnorm"::: )   "(" (Set (Var "f")) "," (Set (Var "w")) ")"  ")" ) ")" )))))) ; 
 
theorem :: HERMITAN:50 (Bool  "for" (Set (Var "V")) "being"   ($#l1_vectsp_1 :::"VectSp":::) "of" (Set   ($#k1_complfld :::"F_Complex"::: )  )  (Bool  "for" (Set (Var "f")) "being"   ($#v5_hermitan :::"diagReR+0valued"::: )    ($#m1_subset_1 :::"hermitan-Form":::) "of" (Set (Var "V"))  (Bool  "for" (Set (Var "v")) "," (Set (Var "w")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "V")) "holds"  (Bool (Set (Set  ($#k17_complex1 :::"|."::: ) (Set  "(" (Set (Var "f"))  ($#k2_binop_1 :::"."::: )   "(" (Set  "(" (Set (Var "v"))  ($#k3_rlvect_1 :::"+"::: )  (Set (Var "w")) ")" ) "," (Set  "(" (Set (Var "v"))  ($#k3_rlvect_1 :::"+"::: )  (Set (Var "w")) ")" ) ")"  ")" ) ($#k17_complex1 :::".|"::: ) )  ($#k7_real_1 :::"+"::: )  (Set  ($#k17_complex1 :::"|."::: ) (Set  "(" (Set (Var "f"))  ($#k2_binop_1 :::"."::: )   "(" (Set  "(" (Set (Var "v"))  ($#k5_algstr_0 :::"-"::: )  (Set (Var "w")) ")" ) "," (Set  "(" (Set (Var "v"))  ($#k5_algstr_0 :::"-"::: )  (Set (Var "w")) ")" ) ")"  ")" ) ($#k17_complex1 :::".|"::: ) ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Num 2)  ($#k8_real_1 :::"*"::: )  (Set  ($#k17_complex1 :::"|."::: ) (Set  "(" (Set (Var "f"))  ($#k2_binop_1 :::"."::: )   "(" (Set (Var "v")) "," (Set (Var "v")) ")"  ")" ) ($#k17_complex1 :::".|"::: ) ) ")" )  ($#k7_real_1 :::"+"::: )  (Set  "(" (Num 2)  ($#k8_real_1 :::"*"::: )  (Set  ($#k17_complex1 :::"|."::: ) (Set  "(" (Set (Var "f"))  ($#k2_binop_1 :::"."::: )   "(" (Set (Var "w")) "," (Set (Var "w")) ")"  ")" ) ($#k17_complex1 :::".|"::: ) ) ")" )))))) ; 
 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 :::"Form":::) "of" (Set (Const "V")) "," (Set (Const "V")); func  :::"quasinorm"::: "f" ->   ($#m1_subset_1 :::"RFunctional":::) "of" "V" means :: HERMITAN:def 10 (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   ($#k6_square_1 :::"sqrt"::: )  (Set  "("  ($#k4_hermitan :::"signnorm"::: )   "(" "f" "," (Set (Var "v")) ")"  ")" )))); end; 






:: deftheorem    defines :::"quasinorm"::: HERMITAN:def 10 :  (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 :::"Form":::) "of" (Set (Var "V")) "," (Set (Var "V"))  (Bool  "for" (Set (Var "b3")) "being"   ($#m1_subset_1 :::"RFunctional":::) "of" (Set (Var "V")) "holds"   (Bool  "("  (Bool (Set (Var "b3"))  ($#r1_hidden :::"="::: )  (Set   ($#k5_hermitan :::"quasinorm"::: )  (Set (Var "f")))) "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   ($#k6_square_1 :::"sqrt"::: )  (Set  "("  ($#k4_hermitan :::"signnorm"::: )   "(" (Set (Var "f")) "," (Set (Var "v")) ")"  ")" ))))  ")" )))); 
 registrationlet "V" be   ($#l1_vectsp_1 :::"VectSp":::) "of" (Set   ($#k1_complfld :::"F_Complex"::: )  ); let "f" be   ($#v5_hermitan :::"diagReR+0valued"::: )    ($#m1_subset_1 :::"hermitan-Form":::) "of" (Set (Const "V")); 
cluster (Set   ($#k5_hermitan :::"quasinorm"::: )  "f") ->   ($#v3_hahnban1 :::"subadditive"::: )     ($#v6_hahnban1 :::"homogeneous"::: )   ; 
end; begin  registrationlet "V" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v13_algstr_0 :::"right_complementable"::: )     ($#v3_rlvect_1 :::"add-associative"::: )     ($#v4_rlvect_1 :::"right_zeroed"::: )     ($#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"::: )  ); let "f" be   ($#v2_hermitan :::"cmplxhomogeneousFAF"::: )    ($#m1_subset_1 :::"Form":::) "of" (Set (Const "V")) "," (Set (Const "V")); 
cluster (Set   ($#k12_bilinear :::"diagker"::: )  "f") ->  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )  ; 
end; 
theorem :: HERMITAN:51 (Bool  "for" (Set (Var "V")) "being"   ($#l1_vectsp_1 :::"VectSp":::) "of" (Set   ($#k1_complfld :::"F_Complex"::: )  )  (Bool  "for" (Set (Var "f")) "being"   ($#v5_hermitan :::"diagReR+0valued"::: )    ($#m1_subset_1 :::"hermitan-Form":::) "of" (Set (Var "V")) "holds"  (Bool (Set   ($#k12_bilinear :::"diagker"::: )  (Set (Var "f"))) "is"   ($#v1_vectsp_4 :::"linearly-closed"::: )  ))) ; 
 
theorem :: HERMITAN:52 (Bool  "for" (Set (Var "V")) "being"   ($#l1_vectsp_1 :::"VectSp":::) "of" (Set   ($#k1_complfld :::"F_Complex"::: )  )  (Bool  "for" (Set (Var "f")) "being"   ($#v5_hermitan :::"diagReR+0valued"::: )    ($#m1_subset_1 :::"hermitan-Form":::) "of" (Set (Var "V")) "holds"  (Bool (Set   ($#k12_bilinear :::"diagker"::: )  (Set (Var "f")))  ($#r1_hidden :::"="::: )  (Set   ($#k10_bilinear :::"leftker"::: )  (Set (Var "f")))))) ; 
 
theorem :: HERMITAN:53 (Bool  "for" (Set (Var "V")) "being"   ($#l1_vectsp_1 :::"VectSp":::) "of" (Set   ($#k1_complfld :::"F_Complex"::: )  )  (Bool  "for" (Set (Var "f")) "being"   ($#v5_hermitan :::"diagReR+0valued"::: )    ($#m1_subset_1 :::"hermitan-Form":::) "of" (Set (Var "V")) "holds"  (Bool (Set   ($#k12_bilinear :::"diagker"::: )  (Set (Var "f")))  ($#r1_hidden :::"="::: )  (Set   ($#k11_bilinear :::"rightker"::: )  (Set (Var "f")))))) ; 
 
theorem :: HERMITAN:54 (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 :::"Form":::) "of" (Set (Var "V")) "," (Set (Var "V")) "holds"  (Bool (Set   ($#k12_bilinear :::"diagker"::: )  (Set (Var "f")))  ($#r1_hidden :::"="::: )  (Set   ($#k12_bilinear :::"diagker"::: )  (Set  "(" (Set (Var "f"))  ($#k3_hermitan :::"*'"::: )  ")" ))))) ; 
 
theorem :: HERMITAN:55 (Bool  "for" (Set (Var "V")) "," (Set (Var "W")) "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 :::"Form":::) "of" (Set (Var "V")) "," (Set (Var "W")) "holds"   (Bool  "("  (Bool (Set   ($#k10_bilinear :::"leftker"::: )  (Set (Var "f")))  ($#r1_hidden :::"="::: )  (Set   ($#k10_bilinear :::"leftker"::: )  (Set  "(" (Set (Var "f"))  ($#k3_hermitan :::"*'"::: )  ")" ))) & (Bool (Set   ($#k11_bilinear :::"rightker"::: )  (Set (Var "f")))  ($#r1_hidden :::"="::: )  (Set   ($#k11_bilinear :::"rightker"::: )  (Set  "(" (Set (Var "f"))  ($#k3_hermitan :::"*'"::: )  ")" )))  ")" ))) ; 
 
theorem :: HERMITAN:56 (Bool  "for" (Set (Var "V")) "being"   ($#l1_vectsp_1 :::"VectSp":::) "of" (Set   ($#k1_complfld :::"F_Complex"::: )  )  (Bool  "for" (Set (Var "f")) "being"   ($#v5_hermitan :::"diagReR+0valued"::: )    ($#m1_subset_1 :::"hermitan-Form":::) "of" (Set (Var "V")) "holds"  (Bool (Set   ($#k13_bilinear :::"LKer"::: )  (Set (Var "f")))  ($#r1_hidden :::"="::: )  (Set   ($#k14_bilinear :::"RKer"::: )  (Set  "(" (Set (Var "f"))  ($#k3_hermitan :::"*'"::: )  ")" ))))) ; 
 
theorem :: HERMITAN:57 (Bool  "for" (Set (Var "V")) "being"   ($#l1_vectsp_1 :::"VectSp":::) "of" (Set   ($#k1_complfld :::"F_Complex"::: )  )  (Bool  "for" (Set (Var "f")) "being"   ($#v4_hermitan :::"diagRvalued"::: )     ($#v5_hermitan :::"diagReR+0valued"::: )    ($#m1_subset_1 :::"Form":::) "of" (Set (Var "V")) "," (Set (Var "V"))  (Bool  "for" (Set (Var "v")) "being"   ($#m1_subset_1 :::"Vector":::) "of" (Set (Var "V"))  "st" (Bool (Bool (Set   ($#k3_complex1 :::"Re"::: )  (Set  "(" (Set (Var "f"))  ($#k2_binop_1 :::"."::: )   "(" (Set (Var "v")) "," (Set (Var "v")) ")"  ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set (Set (Var "f"))  ($#k2_binop_1 :::"."::: )   "(" (Set (Var "v")) "," (Set (Var "v")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k4_struct_0 :::"0."::: )  (Set  ($#k1_complfld :::"F_Complex"::: ) )))))) ; 
 
theorem :: HERMITAN:58 (Bool  "for" (Set (Var "V")) "being"   ($#l1_vectsp_1 :::"VectSp":::) "of" (Set   ($#k1_complfld :::"F_Complex"::: )  )  (Bool  "for" (Set (Var "f")) "being"   ($#v5_hermitan :::"diagReR+0valued"::: )    ($#m1_subset_1 :::"hermitan-Form":::) "of" (Set (Var "V"))  (Bool  "for" (Set (Var "v")) "being"   ($#m1_subset_1 :::"Vector":::) "of" (Set (Var "V"))  "st" (Bool (Bool (Set   ($#k3_complex1 :::"Re"::: )  (Set  "(" (Set (Var "f"))  ($#k2_binop_1 :::"."::: )   "(" (Set (Var "v")) "," (Set (Var "v")) ")"  ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool  "("   "not" (Bool (Set (Var "f")) "is"   ($#v5_bilinear :::"degenerated-on-left"::: )  ) "or"  "not" (Bool (Set (Var "f")) "is"   ($#v6_bilinear :::"degenerated-on-right"::: )  )  ")" )) "holds"  (Bool (Set (Var "v"))  ($#r1_hidden :::"="::: )  (Set   ($#k4_struct_0 :::"0."::: )  (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 "W" be   ($#l1_vectsp_1 :::"VectSp":::) "of" (Set   ($#k1_complfld :::"F_Complex"::: )  ); let "f" be   ($#v1_bilinear :::"additiveFAF"::: )     ($#v2_hermitan :::"cmplxhomogeneousFAF"::: )    ($#m1_subset_1 :::"Form":::) "of" (Set (Const "V")) "," (Set (Const "W")); func  :::"RQ*Form"::: "f" ->   ($#v1_bilinear :::"additiveFAF"::: )     ($#v2_hermitan :::"cmplxhomogeneousFAF"::: )    ($#m1_subset_1 :::"Form":::) "of" "V" "," (Set  "("  ($#k6_vectsp10 :::"VectQuot"::: )   "(" "W" "," (Set  "("  ($#k14_bilinear :::"RKer"::: )  (Set  "(" "f"  ($#k3_hermitan :::"*'"::: )  ")" ) ")" ) ")"  ")" ) equals :: HERMITAN:def 11 (Set (Set  "("  ($#k16_bilinear :::"RQForm"::: )  (Set  "(" "f"  ($#k3_hermitan :::"*'"::: )  ")" ) ")" )  ($#k3_hermitan :::"*'"::: )  ); end; 







:: deftheorem    defines :::"RQ*Form"::: HERMITAN:def 11 :  (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 "W")) "being"   ($#l1_vectsp_1 :::"VectSp":::) "of" (Set   ($#k1_complfld :::"F_Complex"::: )  )  (Bool  "for" (Set (Var "f")) "being"   ($#v1_bilinear :::"additiveFAF"::: )     ($#v2_hermitan :::"cmplxhomogeneousFAF"::: )    ($#m1_subset_1 :::"Form":::) "of" (Set (Var "V")) "," (Set (Var "W")) "holds"  (Bool (Set   ($#k6_hermitan :::"RQ*Form"::: )  (Set (Var "f")))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k16_bilinear :::"RQForm"::: )  (Set  "(" (Set (Var "f"))  ($#k3_hermitan :::"*'"::: )  ")" ) ")" )  ($#k3_hermitan :::"*'"::: )  ))))); 
 
theorem :: HERMITAN:59 (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 "W")) "being"   ($#l1_vectsp_1 :::"VectSp":::) "of" (Set   ($#k1_complfld :::"F_Complex"::: )  )  (Bool  "for" (Set (Var "f")) "being"   ($#v1_bilinear :::"additiveFAF"::: )     ($#v2_hermitan :::"cmplxhomogeneousFAF"::: )    ($#m1_subset_1 :::"Form":::) "of" (Set (Var "V")) "," (Set (Var "W"))  (Bool  "for" (Set (Var "v")) "being"   ($#m1_subset_1 :::"Vector":::) "of" (Set (Var "V"))  (Bool  "for" (Set (Var "w")) "being"   ($#m1_subset_1 :::"Vector":::) "of" (Set (Var "W")) "holds"  (Bool (Set (Set  "("  ($#k6_hermitan :::"RQ*Form"::: )  (Set (Var "f")) ")" )  ($#k1_binop_1 :::"."::: )   "(" (Set (Var "v")) "," (Set  "(" (Set (Var "w"))  ($#k3_vectsp_4 :::"+"::: )  (Set  "("  ($#k14_bilinear :::"RKer"::: )  (Set  "(" (Set (Var "f"))  ($#k3_hermitan :::"*'"::: )  ")" ) ")" ) ")" ) ")" )  ($#r1_hidden :::"="::: )  (Set (Set (Var "f"))  ($#k2_binop_1 :::"."::: )   "(" (Set (Var "v")) "," (Set (Var "w")) ")" ))))))) ; 
 registrationlet "V", "W" be   ($#l1_vectsp_1 :::"VectSp":::) "of" (Set   ($#k1_complfld :::"F_Complex"::: )  ); let "f" be   ($#m1_subset_1 :::"sesquilinear-Form":::) "of" (Set (Const "V")) "," (Set (Const "W")); 
cluster (Set   ($#k15_bilinear :::"LQForm"::: )  "f") ->   ($#v1_bilinear :::"additiveFAF"::: )     ($#v2_hermitan :::"cmplxhomogeneousFAF"::: )   ; 

cluster (Set   ($#k6_hermitan :::"RQ*Form"::: )  "f") ->   ($#v1_bilinear :::"additiveFAF"::: )     ($#v2_bilinear :::"additiveSAF"::: )     ($#v4_bilinear :::"homogeneousSAF"::: )     ($#v2_hermitan :::"cmplxhomogeneousFAF"::: )   ; 
end; definitionlet "V", "W" be   ($#l1_vectsp_1 :::"VectSp":::) "of" (Set   ($#k1_complfld :::"F_Complex"::: )  ); let "f" be   ($#m1_subset_1 :::"sesquilinear-Form":::) "of" (Set (Const "V")) "," (Set (Const "W")); func  :::"Q*Form"::: "f" ->   ($#m1_subset_1 :::"sesquilinear-Form":::) "of" (Set  "("  ($#k6_vectsp10 :::"VectQuot"::: )   "(" "V" "," (Set  "("  ($#k13_bilinear :::"LKer"::: )  "f" ")" ) ")"  ")" ) "," (Set  "("  ($#k6_vectsp10 :::"VectQuot"::: )   "(" "W" "," (Set  "("  ($#k14_bilinear :::"RKer"::: )  (Set  "(" "f"  ($#k3_hermitan :::"*'"::: )  ")" ) ")" ) ")"  ")" ) means :: HERMITAN:def 12 (Bool  "for" (Set (Var "A")) "being"   ($#m1_subset_1 :::"Vector":::) "of" (Set  "("  ($#k6_vectsp10 :::"VectQuot"::: )   "(" "V" "," (Set  "("  ($#k13_bilinear :::"LKer"::: )  "f" ")" ) ")"  ")" )  (Bool  "for" (Set (Var "B")) "being"   ($#m1_subset_1 :::"Vector":::) "of" (Set  "("  ($#k6_vectsp10 :::"VectQuot"::: )   "(" "W" "," (Set  "("  ($#k14_bilinear :::"RKer"::: )  (Set  "(" "f"  ($#k3_hermitan :::"*'"::: )  ")" ) ")" ) ")"  ")" )  (Bool  "for" (Set (Var "v")) "being"   ($#m1_subset_1 :::"Vector":::) "of" "V"  (Bool  "for" (Set (Var "w")) "being"   ($#m1_subset_1 :::"Vector":::) "of" "W"  "st" (Bool (Bool (Set (Var "A"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "v"))  ($#k3_vectsp_4 :::"+"::: )  (Set  "("  ($#k13_bilinear :::"LKer"::: )  "f" ")" ))) & (Bool (Set (Var "B"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "w"))  ($#k3_vectsp_4 :::"+"::: )  (Set  "("  ($#k14_bilinear :::"RKer"::: )  (Set  "(" "f"  ($#k3_hermitan :::"*'"::: )  ")" ) ")" )))) "holds"  (Bool (Set it  ($#k2_binop_1 :::"."::: )   "(" (Set (Var "A")) "," (Set (Var "B")) ")" )  ($#r1_hidden :::"="::: )  (Set "f"  ($#k2_binop_1 :::"."::: )   "(" (Set (Var "v")) "," (Set (Var "w")) ")" )))))); end; 







:: deftheorem    defines :::"Q*Form"::: HERMITAN:def 12 :  (Bool  "for" (Set (Var "V")) "," (Set (Var "W")) "being"   ($#l1_vectsp_1 :::"VectSp":::) "of" (Set   ($#k1_complfld :::"F_Complex"::: )  )  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"sesquilinear-Form":::) "of" (Set (Var "V")) "," (Set (Var "W"))  (Bool  "for" (Set (Var "b4")) "being"   ($#m1_subset_1 :::"sesquilinear-Form":::) "of" (Set  "("  ($#k6_vectsp10 :::"VectQuot"::: )   "(" (Set (Var "V")) "," (Set  "("  ($#k13_bilinear :::"LKer"::: )  (Set (Var "f")) ")" ) ")"  ")" ) "," (Set  "("  ($#k6_vectsp10 :::"VectQuot"::: )   "(" (Set (Var "W")) "," (Set  "("  ($#k14_bilinear :::"RKer"::: )  (Set  "(" (Set (Var "f"))  ($#k3_hermitan :::"*'"::: )  ")" ) ")" ) ")"  ")" ) "holds"   (Bool  "("  (Bool (Set (Var "b4"))  ($#r1_hidden :::"="::: )  (Set   ($#k7_hermitan :::"Q*Form"::: )  (Set (Var "f")))) "iff" (Bool  "for" (Set (Var "A")) "being"   ($#m1_subset_1 :::"Vector":::) "of" (Set  "("  ($#k6_vectsp10 :::"VectQuot"::: )   "(" (Set (Var "V")) "," (Set  "("  ($#k13_bilinear :::"LKer"::: )  (Set (Var "f")) ")" ) ")"  ")" )  (Bool  "for" (Set (Var "B")) "being"   ($#m1_subset_1 :::"Vector":::) "of" (Set  "("  ($#k6_vectsp10 :::"VectQuot"::: )   "(" (Set (Var "W")) "," (Set  "("  ($#k14_bilinear :::"RKer"::: )  (Set  "(" (Set (Var "f"))  ($#k3_hermitan :::"*'"::: )  ")" ) ")" ) ")"  ")" )  (Bool  "for" (Set (Var "v")) "being"   ($#m1_subset_1 :::"Vector":::) "of" (Set (Var "V"))  (Bool  "for" (Set (Var "w")) "being"   ($#m1_subset_1 :::"Vector":::) "of" (Set (Var "W"))  "st" (Bool (Bool (Set (Var "A"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "v"))  ($#k3_vectsp_4 :::"+"::: )  (Set  "("  ($#k13_bilinear :::"LKer"::: )  (Set (Var "f")) ")" ))) & (Bool (Set (Var "B"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "w"))  ($#k3_vectsp_4 :::"+"::: )  (Set  "("  ($#k14_bilinear :::"RKer"::: )  (Set  "(" (Set (Var "f"))  ($#k3_hermitan :::"*'"::: )  ")" ) ")" )))) "holds"  (Bool (Set (Set (Var "b4"))  ($#k2_binop_1 :::"."::: )   "(" (Set (Var "A")) "," (Set (Var "B")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set (Var "f"))  ($#k2_binop_1 :::"."::: )   "(" (Set (Var "v")) "," (Set (Var "w")) ")" ))))))  ")" )))); 
 registrationlet "V", "W" be  ($#~v7_struct_0  "non"   ($#v7_struct_0 :::"trivial"::: )   )   ($#l1_vectsp_1 :::"VectSp":::) "of" (Set   ($#k1_complfld :::"F_Complex"::: )  ); let "f" be  ($#~v3_funct_1  "non"   ($#v3_funct_1 :::"constant"::: )   )   ($#m1_subset_1 :::"sesquilinear-Form":::) "of" (Set (Const "V")) "," (Set (Const "W")); 
cluster (Set   ($#k7_hermitan :::"Q*Form"::: )  "f") ->  ($#~v3_funct_1  "non"   ($#v3_funct_1 :::"constant"::: )   )  ; 
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"::: )  ); let "W" be   ($#l1_vectsp_1 :::"VectSp":::) "of" (Set   ($#k1_complfld :::"F_Complex"::: )  ); let "f" be   ($#v1_bilinear :::"additiveFAF"::: )     ($#v2_hermitan :::"cmplxhomogeneousFAF"::: )    ($#m1_subset_1 :::"Form":::) "of" (Set (Const "V")) "," (Set (Const "W")); 
cluster (Set   ($#k6_hermitan :::"RQ*Form"::: )  "f") ->   ($#v1_bilinear :::"additiveFAF"::: )    ($#~v6_bilinear  "non"   ($#v6_bilinear :::"degenerated-on-right"::: )   )    ($#v2_hermitan :::"cmplxhomogeneousFAF"::: )   ; 
end; 
theorem :: HERMITAN:60 (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 "W")) "being"   ($#l1_vectsp_1 :::"VectSp":::) "of" (Set   ($#k1_complfld :::"F_Complex"::: )  )  (Bool  "for" (Set (Var "f")) "being"   ($#v1_bilinear :::"additiveFAF"::: )     ($#v2_hermitan :::"cmplxhomogeneousFAF"::: )    ($#m1_subset_1 :::"Form":::) "of" (Set (Var "V")) "," (Set (Var "W")) "holds"  (Bool (Set   ($#k10_bilinear :::"leftker"::: )  (Set (Var "f")))  ($#r1_hidden :::"="::: )  (Set   ($#k10_bilinear :::"leftker"::: )  (Set  "("  ($#k6_hermitan :::"RQ*Form"::: )  (Set (Var "f")) ")" )))))) ; 
 
theorem :: HERMITAN:61 (Bool  "for" (Set (Var "V")) "," (Set (Var "W")) "being"   ($#l1_vectsp_1 :::"VectSp":::) "of" (Set   ($#k1_complfld :::"F_Complex"::: )  )  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"sesquilinear-Form":::) "of" (Set (Var "V")) "," (Set (Var "W")) "holds"  (Bool (Set   ($#k14_bilinear :::"RKer"::: )  (Set  "(" (Set (Var "f"))  ($#k3_hermitan :::"*'"::: )  ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k14_bilinear :::"RKer"::: )  (Set  "(" (Set  "("  ($#k15_bilinear :::"LQForm"::: )  (Set (Var "f")) ")" )  ($#k3_hermitan :::"*'"::: )  ")" ))))) ; 
 
theorem :: HERMITAN:62 (Bool  "for" (Set (Var "V")) "," (Set (Var "W")) "being"   ($#l1_vectsp_1 :::"VectSp":::) "of" (Set   ($#k1_complfld :::"F_Complex"::: )  )  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"sesquilinear-Form":::) "of" (Set (Var "V")) "," (Set (Var "W")) "holds"  (Bool (Set   ($#k13_bilinear :::"LKer"::: )  (Set (Var "f")))  ($#r1_hidden :::"="::: )  (Set   ($#k13_bilinear :::"LKer"::: )  (Set  "("  ($#k6_hermitan :::"RQ*Form"::: )  (Set (Var "f")) ")" ))))) ; 
 
theorem :: HERMITAN:63 (Bool  "for" (Set (Var "V")) "," (Set (Var "W")) "being"   ($#l1_vectsp_1 :::"VectSp":::) "of" (Set   ($#k1_complfld :::"F_Complex"::: )  )  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"sesquilinear-Form":::) "of" (Set (Var "V")) "," (Set (Var "W")) "holds"   (Bool  "("  (Bool (Set   ($#k7_hermitan :::"Q*Form"::: )  (Set (Var "f")))  ($#r1_funct_2 :::"="::: )  (Set   ($#k6_hermitan :::"RQ*Form"::: )  (Set  "("  ($#k15_bilinear :::"LQForm"::: )  (Set (Var "f")) ")" ))) & (Bool (Set   ($#k7_hermitan :::"Q*Form"::: )  (Set (Var "f")))  ($#r1_funct_2 :::"="::: )  (Set   ($#k15_bilinear :::"LQForm"::: )  (Set  "("  ($#k6_hermitan :::"RQ*Form"::: )  (Set (Var "f")) ")" )))  ")" ))) ; 
 
theorem :: HERMITAN:64 (Bool  "for" (Set (Var "V")) "," (Set (Var "W")) "being"   ($#l1_vectsp_1 :::"VectSp":::) "of" (Set   ($#k1_complfld :::"F_Complex"::: )  )  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"sesquilinear-Form":::) "of" (Set (Var "V")) "," (Set (Var "W")) "holds"   (Bool  "("  (Bool (Set   ($#k10_bilinear :::"leftker"::: )  (Set  "("  ($#k7_hermitan :::"Q*Form"::: )  (Set (Var "f")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k10_bilinear :::"leftker"::: )  (Set  "("  ($#k6_hermitan :::"RQ*Form"::: )  (Set  "("  ($#k15_bilinear :::"LQForm"::: )  (Set (Var "f")) ")" ) ")" ))) & (Bool (Set   ($#k11_bilinear :::"rightker"::: )  (Set  "("  ($#k7_hermitan :::"Q*Form"::: )  (Set (Var "f")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k11_bilinear :::"rightker"::: )  (Set  "("  ($#k6_hermitan :::"RQ*Form"::: )  (Set  "("  ($#k15_bilinear :::"LQForm"::: )  (Set (Var "f")) ")" ) ")" ))) & (Bool (Set   ($#k10_bilinear :::"leftker"::: )  (Set  "("  ($#k7_hermitan :::"Q*Form"::: )  (Set (Var "f")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k10_bilinear :::"leftker"::: )  (Set  "("  ($#k15_bilinear :::"LQForm"::: )  (Set  "("  ($#k6_hermitan :::"RQ*Form"::: )  (Set (Var "f")) ")" ) ")" ))) & (Bool (Set   ($#k11_bilinear :::"rightker"::: )  (Set  "("  ($#k7_hermitan :::"Q*Form"::: )  (Set (Var "f")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k11_bilinear :::"rightker"::: )  (Set  "("  ($#k15_bilinear :::"LQForm"::: )  (Set  "("  ($#k6_hermitan :::"RQ*Form"::: )  (Set (Var "f")) ")" ) ")" )))  ")" ))) ; 
 registrationlet "V", "W" be   ($#l1_vectsp_1 :::"VectSp":::) "of" (Set   ($#k1_complfld :::"F_Complex"::: )  ); let "f" be   ($#m1_subset_1 :::"sesquilinear-Form":::) "of" (Set (Const "V")) "," (Set (Const "W")); 
cluster (Set   ($#k6_hermitan :::"RQ*Form"::: )  (Set  "("  ($#k15_bilinear :::"LQForm"::: )  "f" ")" )) ->   ($#v1_bilinear :::"additiveFAF"::: )    ($#~v5_bilinear  "non"   ($#v5_bilinear :::"degenerated-on-left"::: )   )   ($#~v6_bilinear  "non"   ($#v6_bilinear :::"degenerated-on-right"::: )   )    ($#v2_hermitan :::"cmplxhomogeneousFAF"::: )   ; 

cluster (Set   ($#k15_bilinear :::"LQForm"::: )  (Set  "("  ($#k6_hermitan :::"RQ*Form"::: )  "f" ")" )) ->  ($#~v5_bilinear  "non"   ($#v5_bilinear :::"degenerated-on-left"::: )   )   ($#~v6_bilinear  "non"   ($#v6_bilinear :::"degenerated-on-right"::: )   )  ; 
end; registrationlet "V", "W" be   ($#l1_vectsp_1 :::"VectSp":::) "of" (Set   ($#k1_complfld :::"F_Complex"::: )  ); let "f" be   ($#m1_subset_1 :::"sesquilinear-Form":::) "of" (Set (Const "V")) "," (Set (Const "W")); 
cluster (Set   ($#k7_hermitan :::"Q*Form"::: )  "f") ->  ($#~v5_bilinear  "non"   ($#v5_bilinear :::"degenerated-on-left"::: )   )   ($#~v6_bilinear  "non"   ($#v6_bilinear :::"degenerated-on-right"::: )   )  ; 
end; begin  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 :::"Form":::) "of" (Set (Const "V")) "," (Set (Const "V")); attr "f" is  :::"positivediagvalued":::  means :: HERMITAN:def 13 (Bool  "for" (Set (Var "v")) "being"   ($#m1_subset_1 :::"Vector":::) "of" "V"  "st" (Bool (Bool (Set (Var "v"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k4_struct_0 :::"0."::: )  "V"))) "holds"  (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k3_complex1 :::"Re"::: )  (Set  "(" "f"  ($#k2_binop_1 :::"."::: )   "(" (Set (Var "v")) "," (Set (Var "v")) ")"  ")" )))); end; 





:: deftheorem    defines :::"positivediagvalued"::: HERMITAN: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 :::"Form":::) "of" (Set (Var "V")) "," (Set (Var "V")) "holds"   (Bool  "("  (Bool (Set (Var "f")) "is"   ($#v6_hermitan :::"positivediagvalued"::: )  ) "iff" (Bool  "for" (Set (Var "v")) "being"   ($#m1_subset_1 :::"Vector":::) "of" (Set (Var "V"))  "st" (Bool (Bool (Set (Var "v"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k4_struct_0 :::"0."::: )  (Set (Var "V"))))) "holds"  (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k3_complex1 :::"Re"::: )  (Set  "(" (Set (Var "f"))  ($#k2_binop_1 :::"."::: )   "(" (Set (Var "v")) "," (Set (Var "v")) ")"  ")" ))))  ")" ))); 
 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   ($#v1_funct_1 :::"Function-like"::: )   bbbadV1_FUNCT_2((Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "V") "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "V") ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set  ($#k1_complfld :::"F_Complex"::: ) )))   ($#v2_bilinear :::"additiveSAF"::: )     ($#v6_hermitan :::"positivediagvalued"::: )    ->   ($#v5_hermitan :::"diagReR+0valued"::: )    for    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k1_zfmisc_1 :::"bool"::: )  (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "V") "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "V") ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set  ($#k1_complfld :::"F_Complex"::: ) )) ($#k2_zfmisc_1 :::":]"::: ) )); 
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   ($#v1_funct_1 :::"Function-like"::: )   bbbadV1_FUNCT_2((Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "V") "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "V") ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set  ($#k1_complfld :::"F_Complex"::: ) )))   ($#v1_bilinear :::"additiveFAF"::: )     ($#v6_hermitan :::"positivediagvalued"::: )    ->   ($#v5_hermitan :::"diagReR+0valued"::: )    for    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k1_zfmisc_1 :::"bool"::: )  (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "V") "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "V") ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set  ($#k1_complfld :::"F_Complex"::: ) )) ($#k2_zfmisc_1 :::":]"::: ) )); 
end; definitionlet "V" be   ($#l1_vectsp_1 :::"VectSp":::) "of" (Set   ($#k1_complfld :::"F_Complex"::: )  ); let "f" be   ($#v5_hermitan :::"diagReR+0valued"::: )    ($#m1_subset_1 :::"hermitan-Form":::) "of" (Set (Const "V")); func  :::"ScalarForm"::: "f" ->   ($#v5_hermitan :::"diagReR+0valued"::: )    ($#m1_subset_1 :::"hermitan-Form":::) "of" (Set  "("  ($#k6_vectsp10 :::"VectQuot"::: )   "(" "V" "," (Set  "("  ($#k13_bilinear :::"LKer"::: )  "f" ")" ) ")"  ")" ) equals :: HERMITAN:def 14 (Set   ($#k7_hermitan :::"Q*Form"::: )  "f"); end; 






:: deftheorem    defines :::"ScalarForm"::: HERMITAN:def 14 :  (Bool  "for" (Set (Var "V")) "being"   ($#l1_vectsp_1 :::"VectSp":::) "of" (Set   ($#k1_complfld :::"F_Complex"::: )  )  (Bool  "for" (Set (Var "f")) "being"   ($#v5_hermitan :::"diagReR+0valued"::: )    ($#m1_subset_1 :::"hermitan-Form":::) "of" (Set (Var "V")) "holds"  (Bool (Set   ($#k8_hermitan :::"ScalarForm"::: )  (Set (Var "f")))  ($#r1_hidden :::"="::: )  (Set   ($#k7_hermitan :::"Q*Form"::: )  (Set (Var "f")))))); 
 
theorem :: HERMITAN:65 (Bool  "for" (Set (Var "V")) "being"   ($#l1_vectsp_1 :::"VectSp":::) "of" (Set   ($#k1_complfld :::"F_Complex"::: )  )  (Bool  "for" (Set (Var "f")) "being"   ($#v5_hermitan :::"diagReR+0valued"::: )    ($#m1_subset_1 :::"hermitan-Form":::) "of" (Set (Var "V"))  (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"   ($#m1_subset_1 :::"Vector":::) "of" (Set  "("  ($#k6_vectsp10 :::"VectQuot"::: )   "(" (Set (Var "V")) "," (Set  "("  ($#k13_bilinear :::"LKer"::: )  (Set (Var "f")) ")" ) ")"  ")" )  (Bool  "for" (Set (Var "v")) "," (Set (Var "w")) "being"   ($#m1_subset_1 :::"Vector":::) "of" (Set (Var "V"))  "st" (Bool (Bool (Set (Var "A"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "v"))  ($#k3_vectsp_4 :::"+"::: )  (Set  "("  ($#k13_bilinear :::"LKer"::: )  (Set (Var "f")) ")" ))) & (Bool (Set (Var "B"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "w"))  ($#k3_vectsp_4 :::"+"::: )  (Set  "("  ($#k13_bilinear :::"LKer"::: )  (Set (Var "f")) ")" )))) "holds"  (Bool (Set (Set  "("  ($#k8_hermitan :::"ScalarForm"::: )  (Set (Var "f")) ")" )  ($#k2_binop_1 :::"."::: )   "(" (Set (Var "A")) "," (Set (Var "B")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set (Var "f"))  ($#k2_binop_1 :::"."::: )   "(" (Set (Var "v")) "," (Set (Var "w")) ")" )))))) ; 
 
theorem :: HERMITAN:66 (Bool  "for" (Set (Var "V")) "being"   ($#l1_vectsp_1 :::"VectSp":::) "of" (Set   ($#k1_complfld :::"F_Complex"::: )  )  (Bool  "for" (Set (Var "f")) "being"   ($#v5_hermitan :::"diagReR+0valued"::: )    ($#m1_subset_1 :::"hermitan-Form":::) "of" (Set (Var "V")) "holds"  (Bool (Set   ($#k10_bilinear :::"leftker"::: )  (Set  "("  ($#k8_hermitan :::"ScalarForm"::: )  (Set (Var "f")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k10_bilinear :::"leftker"::: )  (Set  "("  ($#k7_hermitan :::"Q*Form"::: )  (Set (Var "f")) ")" ))))) ; 
 
theorem :: HERMITAN:67 (Bool  "for" (Set (Var "V")) "being"   ($#l1_vectsp_1 :::"VectSp":::) "of" (Set   ($#k1_complfld :::"F_Complex"::: )  )  (Bool  "for" (Set (Var "f")) "being"   ($#v5_hermitan :::"diagReR+0valued"::: )    ($#m1_subset_1 :::"hermitan-Form":::) "of" (Set (Var "V")) "holds"  (Bool (Set   ($#k11_bilinear :::"rightker"::: )  (Set  "("  ($#k8_hermitan :::"ScalarForm"::: )  (Set (Var "f")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k11_bilinear :::"rightker"::: )  (Set  "("  ($#k7_hermitan :::"Q*Form"::: )  (Set (Var "f")) ")" ))))) ; 
 registrationlet "V" be   ($#l1_vectsp_1 :::"VectSp":::) "of" (Set   ($#k1_complfld :::"F_Complex"::: )  ); let "f" be   ($#v5_hermitan :::"diagReR+0valued"::: )    ($#m1_subset_1 :::"hermitan-Form":::) "of" (Set (Const "V")); 
cluster (Set   ($#k8_hermitan :::"ScalarForm"::: )  "f") ->  ($#~v5_bilinear  "non"   ($#v5_bilinear :::"degenerated-on-left"::: )   )   ($#~v6_bilinear  "non"   ($#v6_bilinear :::"degenerated-on-right"::: )   )    ($#v5_hermitan :::"diagReR+0valued"::: )     ($#v6_hermitan :::"positivediagvalued"::: )   ; 
end; registrationlet "V" be  ($#~v7_struct_0  "non"   ($#v7_struct_0 :::"trivial"::: )   )   ($#l1_vectsp_1 :::"VectSp":::) "of" (Set   ($#k1_complfld :::"F_Complex"::: )  ); let "f" be  ($#~v3_funct_1  "non"   ($#v3_funct_1 :::"constant"::: )   )    ($#v5_hermitan :::"diagReR+0valued"::: )    ($#m1_subset_1 :::"hermitan-Form":::) "of" (Set (Const "V")); 
cluster (Set   ($#k8_hermitan :::"ScalarForm"::: )  "f") ->  ($#~v3_funct_1  "non"   ($#v3_funct_1 :::"constant"::: )   )    ($#v5_hermitan :::"diagReR+0valued"::: )   ; 
end;