:: CSSPACE  semantic presentation begin  definitionfunc  :::"the_set_of_ComplexSequences":::  ->  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )   means :: CSSPACE:def 1 (Bool  "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  it) "iff" (Bool (Set (Var "x")) "is"   ($#m1_subset_1 :::"Complex_Sequence":::))  ")" )); end; 




:: deftheorem    defines :::"the_set_of_ComplexSequences"::: CSSPACE:def 1 :  (Bool  "for" (Set (Var "b1")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Var "b1"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_csspace :::"the_set_of_ComplexSequences"::: )  )) "iff" (Bool  "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "b1"))) "iff" (Bool (Set (Var "x")) "is"   ($#m1_subset_1 :::"Complex_Sequence":::))  ")" ))  ")" )); 
 definitionlet "z" be    ($#m1_hidden :::"set"::: )  ; assume 
(Bool (Set (Const "z"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_csspace :::"the_set_of_ComplexSequences"::: )  ))
 ; func  :::"seq_id"::: "z" ->   ($#m1_subset_1 :::"Complex_Sequence":::) equals :: CSSPACE:def 2 "z"; end; 






:: deftheorem    defines :::"seq_id"::: CSSPACE:def 2 :  (Bool  "for" (Set (Var "z")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "z"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_csspace :::"the_set_of_ComplexSequences"::: )  ))) "holds"  (Bool (Set   ($#k2_csspace :::"seq_id"::: )  (Set (Var "z")))  ($#r1_hidden :::"="::: )  (Set (Var "z")))); 
 definitionlet "z" be    ($#m1_hidden :::"set"::: )  ; assume 
(Bool (Set (Const "z")) "is"   ($#m1_hidden :::"Complex":::))
 ; func  :::"C_id"::: "z" ->   ($#m1_hidden :::"Complex":::) equals :: CSSPACE:def 3 "z"; end; 






:: deftheorem    defines :::"C_id"::: CSSPACE:def 3 :  (Bool  "for" (Set (Var "z")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "z")) "is"   ($#m1_hidden :::"Complex":::))) "holds"  (Bool (Set   ($#k3_csspace :::"C_id"::: )  (Set (Var "z")))  ($#r1_hidden :::"="::: )  (Set (Var "z")))); 
 definitionfunc  :::"l_add":::  ->   ($#m1_subset_1 :::"BinOp":::) "of" (Set  ($#k1_csspace :::"the_set_of_ComplexSequences"::: ) ) means :: CSSPACE:def 4 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k1_csspace :::"the_set_of_ComplexSequences"::: )  ) "holds"  (Bool (Set it  ($#k5_binop_1 :::"."::: )   "(" (Set (Var "a")) "," (Set (Var "b")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k2_csspace :::"seq_id"::: )  (Set (Var "a")) ")" )  ($#k1_series_1 :::"+"::: )  (Set  "("  ($#k2_csspace :::"seq_id"::: )  (Set (Var "b")) ")" )))); end; 




:: deftheorem    defines :::"l_add"::: CSSPACE:def 4 :  (Bool  "for" (Set (Var "b1")) "being"   ($#m1_subset_1 :::"BinOp":::) "of" (Set  ($#k1_csspace :::"the_set_of_ComplexSequences"::: ) ) "holds"   (Bool  "("  (Bool (Set (Var "b1"))  ($#r1_hidden :::"="::: )  (Set   ($#k4_csspace :::"l_add"::: )  )) "iff" (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k1_csspace :::"the_set_of_ComplexSequences"::: )  ) "holds"  (Bool (Set (Set (Var "b1"))  ($#k5_binop_1 :::"."::: )   "(" (Set (Var "a")) "," (Set (Var "b")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k2_csspace :::"seq_id"::: )  (Set (Var "a")) ")" )  ($#k1_series_1 :::"+"::: )  (Set  "("  ($#k2_csspace :::"seq_id"::: )  (Set (Var "b")) ")" ))))  ")" )); 
 definitionfunc  :::"l_mult":::  ->   ($#m1_subset_1 :::"Function":::) "of" (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set  ($#k2_numbers :::"COMPLEX"::: ) ) "," (Set  ($#k1_csspace :::"the_set_of_ComplexSequences"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set  ($#k1_csspace :::"the_set_of_ComplexSequences"::: ) ) means :: CSSPACE:def 5 (Bool  "for" (Set (Var "z")) "," (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "z")) "is"   ($#m1_hidden :::"Complex":::)) & (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_csspace :::"the_set_of_ComplexSequences"::: )  ))) "holds"  (Bool (Set it  ($#k1_binop_1 :::"."::: )   "(" (Set (Var "z")) "," (Set (Var "x")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k3_csspace :::"C_id"::: )  (Set (Var "z")) ")" )  ($#k25_valued_1 :::"(#)"::: )  (Set  "("  ($#k2_csspace :::"seq_id"::: )  (Set (Var "x")) ")" )))); end; 




:: deftheorem    defines :::"l_mult"::: CSSPACE:def 5 :  (Bool  "for" (Set (Var "b1")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set  ($#k2_numbers :::"COMPLEX"::: ) ) "," (Set  ($#k1_csspace :::"the_set_of_ComplexSequences"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set  ($#k1_csspace :::"the_set_of_ComplexSequences"::: ) ) "holds"   (Bool  "("  (Bool (Set (Var "b1"))  ($#r1_hidden :::"="::: )  (Set   ($#k5_csspace :::"l_mult"::: )  )) "iff" (Bool  "for" (Set (Var "z")) "," (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "z")) "is"   ($#m1_hidden :::"Complex":::)) & (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_csspace :::"the_set_of_ComplexSequences"::: )  ))) "holds"  (Bool (Set (Set (Var "b1"))  ($#k1_binop_1 :::"."::: )   "(" (Set (Var "z")) "," (Set (Var "x")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k3_csspace :::"C_id"::: )  (Set (Var "z")) ")" )  ($#k25_valued_1 :::"(#)"::: )  (Set  "("  ($#k2_csspace :::"seq_id"::: )  (Set (Var "x")) ")" ))))  ")" )); 
 definitionfunc  :::"CZeroseq":::  ->    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k1_csspace :::"the_set_of_ComplexSequences"::: )  ) means :: CSSPACE:def 6 (Bool  "for" (Set (Var "n")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"  (Bool (Set (Set  "("  ($#k2_csspace :::"seq_id"::: )  it ")" )  ($#k8_nat_1 :::"."::: )  (Set (Var "n")))  ($#r1_hidden :::"="::: )  (Set   ($#k5_complex1 :::"0c"::: )  ))); end; 




:: deftheorem    defines :::"CZeroseq"::: CSSPACE:def 6 :  (Bool  "for" (Set (Var "b1")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k1_csspace :::"the_set_of_ComplexSequences"::: )  ) "holds"   (Bool  "("  (Bool (Set (Var "b1"))  ($#r1_hidden :::"="::: )  (Set   ($#k6_csspace :::"CZeroseq"::: )  )) "iff" (Bool  "for" (Set (Var "n")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"  (Bool (Set (Set  "("  ($#k2_csspace :::"seq_id"::: )  (Set (Var "b1")) ")" )  ($#k8_nat_1 :::"."::: )  (Set (Var "n")))  ($#r1_hidden :::"="::: )  (Set   ($#k5_complex1 :::"0c"::: )  )))  ")" )); 
 
theorem :: CSSPACE:1 (Bool  "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Complex_Sequence":::) "holds"  (Bool (Set   ($#k2_csspace :::"seq_id"::: )  (Set (Var "x")))  ($#r2_funct_2 :::"="::: )  (Set (Var "x")))) ; 
 
theorem :: CSSPACE:2 (Bool  "for" (Set (Var "v")) "," (Set (Var "w")) "being"   ($#m1_subset_1 :::"VECTOR":::) "of" (Set  ($#g1_clvect_1 :::"CLSStruct"::: )  "(#"  (Set  ($#k1_csspace :::"the_set_of_ComplexSequences"::: ) ) "," (Set  ($#k6_csspace :::"CZeroseq"::: ) ) "," (Set  ($#k4_csspace :::"l_add"::: ) ) "," (Set  ($#k5_csspace :::"l_mult"::: ) ) "#)" ) "holds"  (Bool (Set (Set (Var "v"))  ($#k1_algstr_0 :::"+"::: )  (Set (Var "w")))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k2_csspace :::"seq_id"::: )  (Set (Var "v")) ")" )  ($#k1_series_1 :::"+"::: )  (Set  "("  ($#k2_csspace :::"seq_id"::: )  (Set (Var "w")) ")" )))) ; 
 
theorem :: CSSPACE:3 (Bool  "for" (Set (Var "z")) "being"   ($#m1_hidden :::"Complex":::)  (Bool  "for" (Set (Var "v")) "being"   ($#m1_subset_1 :::"VECTOR":::) "of" (Set  ($#g1_clvect_1 :::"CLSStruct"::: )  "(#"  (Set  ($#k1_csspace :::"the_set_of_ComplexSequences"::: ) ) "," (Set  ($#k6_csspace :::"CZeroseq"::: ) ) "," (Set  ($#k4_csspace :::"l_add"::: ) ) "," (Set  ($#k5_csspace :::"l_mult"::: ) ) "#)" ) "holds"  (Bool (Set (Set (Var "z"))  ($#k1_clvect_1 :::"*"::: )  (Set (Var "v")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "z"))  ($#k25_valued_1 :::"(#)"::: )  (Set  "("  ($#k2_csspace :::"seq_id"::: )  (Set (Var "v")) ")" ))))) ; 
 registration
cluster (Set   ($#g1_clvect_1 :::"CLSStruct"::: )  "(#"  (Set  ($#k1_csspace :::"the_set_of_ComplexSequences"::: ) ) "," (Set  ($#k6_csspace :::"CZeroseq"::: ) ) "," (Set  ($#k4_csspace :::"l_add"::: ) ) "," (Set  ($#k5_csspace :::"l_mult"::: ) ) "#)" ) ->   ($#v2_rlvect_1 :::"Abelian"::: )   ; 
end; 
theorem :: CSSPACE:4 (Bool  "for" (Set (Var "u")) "," (Set (Var "v")) "," (Set (Var "w")) "being"   ($#m1_subset_1 :::"VECTOR":::) "of" (Set  ($#g1_clvect_1 :::"CLSStruct"::: )  "(#"  (Set  ($#k1_csspace :::"the_set_of_ComplexSequences"::: ) ) "," (Set  ($#k6_csspace :::"CZeroseq"::: ) ) "," (Set  ($#k4_csspace :::"l_add"::: ) ) "," (Set  ($#k5_csspace :::"l_mult"::: ) ) "#)" ) "holds"  (Bool (Set (Set  "(" (Set (Var "u"))  ($#k3_rlvect_1 :::"+"::: )  (Set (Var "v")) ")" )  ($#k3_rlvect_1 :::"+"::: )  (Set (Var "w")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "u"))  ($#k3_rlvect_1 :::"+"::: )  (Set  "(" (Set (Var "v"))  ($#k3_rlvect_1 :::"+"::: )  (Set (Var "w")) ")" )))) ; 
 
theorem :: CSSPACE:5 (Bool  "for" (Set (Var "v")) "being"   ($#m1_subset_1 :::"VECTOR":::) "of" (Set  ($#g1_clvect_1 :::"CLSStruct"::: )  "(#"  (Set  ($#k1_csspace :::"the_set_of_ComplexSequences"::: ) ) "," (Set  ($#k6_csspace :::"CZeroseq"::: ) ) "," (Set  ($#k4_csspace :::"l_add"::: ) ) "," (Set  ($#k5_csspace :::"l_mult"::: ) ) "#)" ) "holds"  (Bool (Set (Set (Var "v"))  ($#k3_rlvect_1 :::"+"::: )  (Set  "("  ($#k4_struct_0 :::"0."::: )  (Set  ($#g1_clvect_1 :::"CLSStruct"::: )  "(#"  (Set  ($#k1_csspace :::"the_set_of_ComplexSequences"::: ) ) "," (Set  ($#k6_csspace :::"CZeroseq"::: ) ) "," (Set  ($#k4_csspace :::"l_add"::: ) ) "," (Set  ($#k5_csspace :::"l_mult"::: ) ) "#)" ) ")" ))  ($#r1_hidden :::"="::: )  (Set (Var "v")))) ; 
 
theorem :: CSSPACE:6 (Bool  "for" (Set (Var "v")) "being"   ($#m1_subset_1 :::"VECTOR":::) "of" (Set  ($#g1_clvect_1 :::"CLSStruct"::: )  "(#"  (Set  ($#k1_csspace :::"the_set_of_ComplexSequences"::: ) ) "," (Set  ($#k6_csspace :::"CZeroseq"::: ) ) "," (Set  ($#k4_csspace :::"l_add"::: ) ) "," (Set  ($#k5_csspace :::"l_mult"::: ) ) "#)" ) (Bool  "ex" (Set (Var "w")) "being"   ($#m1_subset_1 :::"VECTOR":::) "of" (Set  ($#g1_clvect_1 :::"CLSStruct"::: )  "(#"  (Set  ($#k1_csspace :::"the_set_of_ComplexSequences"::: ) ) "," (Set  ($#k6_csspace :::"CZeroseq"::: ) ) "," (Set  ($#k4_csspace :::"l_add"::: ) ) "," (Set  ($#k5_csspace :::"l_mult"::: ) ) "#)" ) "st" (Bool (Set (Set (Var "v"))  ($#k3_rlvect_1 :::"+"::: )  (Set (Var "w")))  ($#r1_hidden :::"="::: )  (Set   ($#k4_struct_0 :::"0."::: )  (Set  ($#g1_clvect_1 :::"CLSStruct"::: )  "(#"  (Set  ($#k1_csspace :::"the_set_of_ComplexSequences"::: ) ) "," (Set  ($#k6_csspace :::"CZeroseq"::: ) ) "," (Set  ($#k4_csspace :::"l_add"::: ) ) "," (Set  ($#k5_csspace :::"l_mult"::: ) ) "#)" ))))) ; 
 
theorem :: CSSPACE:7 (Bool  "for" (Set (Var "z")) "being"   ($#m1_hidden :::"Complex":::)  (Bool  "for" (Set (Var "v")) "," (Set (Var "w")) "being"   ($#m1_subset_1 :::"VECTOR":::) "of" (Set  ($#g1_clvect_1 :::"CLSStruct"::: )  "(#"  (Set  ($#k1_csspace :::"the_set_of_ComplexSequences"::: ) ) "," (Set  ($#k6_csspace :::"CZeroseq"::: ) ) "," (Set  ($#k4_csspace :::"l_add"::: ) ) "," (Set  ($#k5_csspace :::"l_mult"::: ) ) "#)" ) "holds"  (Bool (Set (Set (Var "z"))  ($#k1_clvect_1 :::"*"::: )  (Set  "(" (Set (Var "v"))  ($#k3_rlvect_1 :::"+"::: )  (Set (Var "w")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "z"))  ($#k1_clvect_1 :::"*"::: )  (Set (Var "v")) ")" )  ($#k3_rlvect_1 :::"+"::: )  (Set  "(" (Set (Var "z"))  ($#k1_clvect_1 :::"*"::: )  (Set (Var "w")) ")" ))))) ; 
 
theorem :: CSSPACE:8 (Bool  "for" (Set (Var "z1")) "," (Set (Var "z2")) "being"   ($#m1_hidden :::"Complex":::)  (Bool  "for" (Set (Var "v")) "being"   ($#m1_subset_1 :::"VECTOR":::) "of" (Set  ($#g1_clvect_1 :::"CLSStruct"::: )  "(#"  (Set  ($#k1_csspace :::"the_set_of_ComplexSequences"::: ) ) "," (Set  ($#k6_csspace :::"CZeroseq"::: ) ) "," (Set  ($#k4_csspace :::"l_add"::: ) ) "," (Set  ($#k5_csspace :::"l_mult"::: ) ) "#)" ) "holds"  (Bool (Set (Set  "(" (Set (Var "z1"))  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "z2")) ")" )  ($#k1_clvect_1 :::"*"::: )  (Set (Var "v")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "z1"))  ($#k1_clvect_1 :::"*"::: )  (Set (Var "v")) ")" )  ($#k3_rlvect_1 :::"+"::: )  (Set  "(" (Set (Var "z2"))  ($#k1_clvect_1 :::"*"::: )  (Set (Var "v")) ")" ))))) ; 
 
theorem :: CSSPACE:9 (Bool  "for" (Set (Var "z1")) "," (Set (Var "z2")) "being"   ($#m1_hidden :::"Complex":::)  (Bool  "for" (Set (Var "v")) "being"   ($#m1_subset_1 :::"VECTOR":::) "of" (Set  ($#g1_clvect_1 :::"CLSStruct"::: )  "(#"  (Set  ($#k1_csspace :::"the_set_of_ComplexSequences"::: ) ) "," (Set  ($#k6_csspace :::"CZeroseq"::: ) ) "," (Set  ($#k4_csspace :::"l_add"::: ) ) "," (Set  ($#k5_csspace :::"l_mult"::: ) ) "#)" ) "holds"  (Bool (Set (Set  "(" (Set (Var "z1"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "z2")) ")" )  ($#k1_clvect_1 :::"*"::: )  (Set (Var "v")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "z1"))  ($#k1_clvect_1 :::"*"::: )  (Set  "(" (Set (Var "z2"))  ($#k1_clvect_1 :::"*"::: )  (Set (Var "v")) ")" ))))) ; 
 
theorem :: CSSPACE:10 (Bool  "for" (Set (Var "v")) "being"   ($#m1_subset_1 :::"VECTOR":::) "of" (Set  ($#g1_clvect_1 :::"CLSStruct"::: )  "(#"  (Set  ($#k1_csspace :::"the_set_of_ComplexSequences"::: ) ) "," (Set  ($#k6_csspace :::"CZeroseq"::: ) ) "," (Set  ($#k4_csspace :::"l_add"::: ) ) "," (Set  ($#k5_csspace :::"l_mult"::: ) ) "#)" ) "holds"  (Bool (Set (Set  ($#k6_complex1 :::"1r"::: ) )  ($#k1_clvect_1 :::"*"::: )  (Set (Var "v")))  ($#r1_hidden :::"="::: )  (Set (Var "v")))) ; 
 definitionfunc  :::"Linear_Space_of_ComplexSequences":::  ->  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v1_clvect_1 :::"strict"::: )     ($#l1_clvect_1 :::"CLSStruct"::: )   equals :: CSSPACE:def 7 (Set   ($#g1_clvect_1 :::"CLSStruct"::: )  "(#"  (Set  ($#k1_csspace :::"the_set_of_ComplexSequences"::: ) ) "," (Set  ($#k6_csspace :::"CZeroseq"::: ) ) "," (Set  ($#k4_csspace :::"l_add"::: ) ) "," (Set  ($#k5_csspace :::"l_mult"::: ) ) "#)" ); end; 




:: deftheorem    defines :::"Linear_Space_of_ComplexSequences"::: CSSPACE:def 7 :  (Bool (Set   ($#k7_csspace :::"Linear_Space_of_ComplexSequences"::: )  )  ($#r1_hidden :::"="::: )  (Set   ($#g1_clvect_1 :::"CLSStruct"::: )  "(#"  (Set  ($#k1_csspace :::"the_set_of_ComplexSequences"::: ) ) "," (Set  ($#k6_csspace :::"CZeroseq"::: ) ) "," (Set  ($#k4_csspace :::"l_add"::: ) ) "," (Set  ($#k5_csspace :::"l_mult"::: ) ) "#)" )); 
 registration
cluster (Set   ($#k7_csspace :::"Linear_Space_of_ComplexSequences"::: )  ) ->  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v13_algstr_0 :::"right_complementable"::: )     ($#v2_rlvect_1 :::"Abelian"::: )     ($#v3_rlvect_1 :::"add-associative"::: )     ($#v4_rlvect_1 :::"right_zeroed"::: )     ($#v1_clvect_1 :::"strict"::: )     ($#v2_clvect_1 :::"vector-distributive"::: )     ($#v3_clvect_1 :::"scalar-distributive"::: )     ($#v4_clvect_1 :::"scalar-associative"::: )     ($#v5_clvect_1 :::"scalar-unital"::: )   ; 
end; definitionlet "X" be   ($#l1_clvect_1 :::"ComplexLinearSpace":::); let "X1" be   ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "X")); assume 
(Bool (Set (Const "X1")) "is"   ($#v6_clvect_1 :::"linearly-closed"::: )  )
 ; func  :::"Add_":::  "(" "X1" "," "X" ")"  ->   ($#m1_subset_1 :::"BinOp":::) "of" "X1" equals :: CSSPACE:def 8 (Set (Set  "the"  ($#u1_algstr_0 :::"addF"::: )  "of" "X")  ($#k1_realset1 :::"||"::: )  "X1"); end; 







:: deftheorem    defines :::"Add_"::: CSSPACE:def 8 :  (Bool  "for" (Set (Var "X")) "being"   ($#l1_clvect_1 :::"ComplexLinearSpace":::)  (Bool  "for" (Set (Var "X1")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X"))  "st" (Bool (Bool (Set (Var "X1")) "is"   ($#v6_clvect_1 :::"linearly-closed"::: )  )) "holds"  (Bool (Set   ($#k8_csspace :::"Add_"::: )   "(" (Set (Var "X1")) "," (Set (Var "X")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set  "the"  ($#u1_algstr_0 :::"addF"::: )  "of" (Set (Var "X")))  ($#k1_realset1 :::"||"::: )  (Set (Var "X1")))))); 
 definitionlet "X" be   ($#l1_clvect_1 :::"ComplexLinearSpace":::); let "X1" be   ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "X")); assume 
(Bool (Set (Const "X1")) "is"   ($#v6_clvect_1 :::"linearly-closed"::: )  )
 ; func  :::"Mult_":::  "(" "X1" "," "X" ")"  ->   ($#m1_subset_1 :::"Function":::) "of" (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set  ($#k2_numbers :::"COMPLEX"::: ) ) "," "X1" ($#k2_zfmisc_1 :::":]"::: ) ) "," "X1" equals :: CSSPACE:def 9 (Set (Set  "the"  ($#u1_clvect_1 :::"Mult"::: )  "of" "X")  ($#k5_relat_1 :::"|"::: )  (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set  ($#k2_numbers :::"COMPLEX"::: ) ) "," "X1" ($#k2_zfmisc_1 :::":]"::: ) )); end; 







:: deftheorem    defines :::"Mult_"::: CSSPACE:def 9 :  (Bool  "for" (Set (Var "X")) "being"   ($#l1_clvect_1 :::"ComplexLinearSpace":::)  (Bool  "for" (Set (Var "X1")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X"))  "st" (Bool (Bool (Set (Var "X1")) "is"   ($#v6_clvect_1 :::"linearly-closed"::: )  )) "holds"  (Bool (Set   ($#k9_csspace :::"Mult_"::: )   "(" (Set (Var "X1")) "," (Set (Var "X")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set  "the"  ($#u1_clvect_1 :::"Mult"::: )  "of" (Set (Var "X")))  ($#k5_relat_1 :::"|"::: )  (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set  ($#k2_numbers :::"COMPLEX"::: ) ) "," (Set (Var "X1")) ($#k2_zfmisc_1 :::":]"::: ) ))))); 
 definitionlet "X" be   ($#l1_clvect_1 :::"ComplexLinearSpace":::); let "X1" be   ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "X")); assume that  
(Bool (Set (Const "X1")) "is"   ($#v6_clvect_1 :::"linearly-closed"::: )  )
 and  
(Bool (Bool  "not" (Set (Const "X1")) "is"   ($#v1_xboole_0 :::"empty"::: )  ))
 ; func  :::"Zero_":::  "(" "X1" "," "X" ")"  ->    ($#m1_subset_1 :::"Element"::: )   "of" "X1" equals :: CSSPACE:def 10 (Set   ($#k4_struct_0 :::"0."::: )  "X"); end; 







:: deftheorem    defines :::"Zero_"::: CSSPACE:def 10 :  (Bool  "for" (Set (Var "X")) "being"   ($#l1_clvect_1 :::"ComplexLinearSpace":::)  (Bool  "for" (Set (Var "X1")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X"))  "st" (Bool (Bool (Set (Var "X1")) "is"   ($#v6_clvect_1 :::"linearly-closed"::: )  ) & (Bool (Bool  "not" (Set (Var "X1")) "is"   ($#v1_xboole_0 :::"empty"::: )  ))) "holds"  (Bool (Set   ($#k10_csspace :::"Zero_"::: )   "(" (Set (Var "X1")) "," (Set (Var "X")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k4_struct_0 :::"0."::: )  (Set (Var "X")))))); 
 
theorem :: CSSPACE:11 (Bool  "for" (Set (Var "V")) "being"   ($#l1_clvect_1 :::"ComplexLinearSpace":::)  (Bool  "for" (Set (Var "V1")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V"))  "st" (Bool (Bool (Set (Var "V1")) "is"   ($#v6_clvect_1 :::"linearly-closed"::: )  ) & (Bool (Bool  "not" (Set (Var "V1")) "is"   ($#v1_xboole_0 :::"empty"::: )  ))) "holds"  (Bool (Set   ($#g1_clvect_1 :::"CLSStruct"::: )  "(#"  (Set (Var "V1")) "," (Set  "("  ($#k10_csspace :::"Zero_"::: )   "(" (Set (Var "V1")) "," (Set (Var "V")) ")"  ")" ) "," (Set  "("  ($#k8_csspace :::"Add_"::: )   "(" (Set (Var "V1")) "," (Set (Var "V")) ")"  ")" ) "," (Set  "("  ($#k9_csspace :::"Mult_"::: )   "(" (Set (Var "V1")) "," (Set (Var "V")) ")"  ")" ) "#)" ) "is"    ($#m1_clvect_1 :::"Subspace"::: )   "of" (Set (Var "V"))))) ; 
 definitionfunc  :::"the_set_of_l2ComplexSequences":::  ->   ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k7_csspace :::"Linear_Space_of_ComplexSequences"::: ) ) means :: CSSPACE:def 11 (Bool  "("  (Bool (Bool  "not" it "is"   ($#v1_xboole_0 :::"empty"::: )  )) & (Bool  "("   "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  it) "iff" (Bool  "("  (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_csspace :::"the_set_of_ComplexSequences"::: )  )) & (Bool (Set (Set  ($#k55_valued_1 :::"|."::: ) (Set  "("  ($#k2_csspace :::"seq_id"::: )  (Set (Var "x")) ")" ) ($#k55_valued_1 :::".|"::: ) )  ($#k20_valued_1 :::"(#)"::: )  (Set  ($#k55_valued_1 :::"|."::: ) (Set  "("  ($#k2_csspace :::"seq_id"::: )  (Set (Var "x")) ")" ) ($#k55_valued_1 :::".|"::: ) )) "is"   ($#v1_series_1 :::"summable"::: )  )  ")" )  ")" )  ")" )  ")" ); end; 




:: deftheorem    defines :::"the_set_of_l2ComplexSequences"::: CSSPACE:def 11 :  (Bool  "for" (Set (Var "b1")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k7_csspace :::"Linear_Space_of_ComplexSequences"::: ) ) "holds"   (Bool  "("  (Bool (Set (Var "b1"))  ($#r1_hidden :::"="::: )  (Set   ($#k11_csspace :::"the_set_of_l2ComplexSequences"::: )  )) "iff" (Bool  "("  (Bool (Bool  "not" (Set (Var "b1")) "is"   ($#v1_xboole_0 :::"empty"::: )  )) & (Bool  "("   "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "b1"))) "iff" (Bool  "("  (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_csspace :::"the_set_of_ComplexSequences"::: )  )) & (Bool (Set (Set  ($#k55_valued_1 :::"|."::: ) (Set  "("  ($#k2_csspace :::"seq_id"::: )  (Set (Var "x")) ")" ) ($#k55_valued_1 :::".|"::: ) )  ($#k20_valued_1 :::"(#)"::: )  (Set  ($#k55_valued_1 :::"|."::: ) (Set  "("  ($#k2_csspace :::"seq_id"::: )  (Set (Var "x")) ")" ) ($#k55_valued_1 :::".|"::: ) )) "is"   ($#v1_series_1 :::"summable"::: )  )  ")" )  ")" )  ")" )  ")" )  ")" )); 
 
theorem :: CSSPACE:12 (Bool  "("  (Bool (Set   ($#k11_csspace :::"the_set_of_l2ComplexSequences"::: )  ) "is"   ($#v6_clvect_1 :::"linearly-closed"::: )  ) & (Bool (Bool  "not" (Set   ($#k11_csspace :::"the_set_of_l2ComplexSequences"::: )  ) "is"   ($#v1_xboole_0 :::"empty"::: )  ))  ")" ) ; 
 
theorem :: CSSPACE:13 (Bool (Set   ($#g1_clvect_1 :::"CLSStruct"::: )  "(#"  (Set  ($#k11_csspace :::"the_set_of_l2ComplexSequences"::: ) ) "," (Set  "("  ($#k10_csspace :::"Zero_"::: )   "(" (Set  ($#k11_csspace :::"the_set_of_l2ComplexSequences"::: ) ) "," (Set  ($#k7_csspace :::"Linear_Space_of_ComplexSequences"::: ) ) ")"  ")" ) "," (Set  "("  ($#k8_csspace :::"Add_"::: )   "(" (Set  ($#k11_csspace :::"the_set_of_l2ComplexSequences"::: ) ) "," (Set  ($#k7_csspace :::"Linear_Space_of_ComplexSequences"::: ) ) ")"  ")" ) "," (Set  "("  ($#k9_csspace :::"Mult_"::: )   "(" (Set  ($#k11_csspace :::"the_set_of_l2ComplexSequences"::: ) ) "," (Set  ($#k7_csspace :::"Linear_Space_of_ComplexSequences"::: ) ) ")"  ")" ) "#)" ) "is"    ($#m1_clvect_1 :::"Subspace"::: )   "of" (Set   ($#k7_csspace :::"Linear_Space_of_ComplexSequences"::: )  )) ; 
 
theorem :: CSSPACE:14 (Bool (Set   ($#g1_clvect_1 :::"CLSStruct"::: )  "(#"  (Set  ($#k11_csspace :::"the_set_of_l2ComplexSequences"::: ) ) "," (Set  "("  ($#k10_csspace :::"Zero_"::: )   "(" (Set  ($#k11_csspace :::"the_set_of_l2ComplexSequences"::: ) ) "," (Set  ($#k7_csspace :::"Linear_Space_of_ComplexSequences"::: ) ) ")"  ")" ) "," (Set  "("  ($#k8_csspace :::"Add_"::: )   "(" (Set  ($#k11_csspace :::"the_set_of_l2ComplexSequences"::: ) ) "," (Set  ($#k7_csspace :::"Linear_Space_of_ComplexSequences"::: ) ) ")"  ")" ) "," (Set  "("  ($#k9_csspace :::"Mult_"::: )   "(" (Set  ($#k11_csspace :::"the_set_of_l2ComplexSequences"::: ) ) "," (Set  ($#k7_csspace :::"Linear_Space_of_ComplexSequences"::: ) ) ")"  ")" ) "#)" ) "is"   ($#l1_clvect_1 :::"ComplexLinearSpace":::)) ; 
 
theorem :: CSSPACE:15 (Bool  "("  (Bool (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set  ($#k7_csspace :::"Linear_Space_of_ComplexSequences"::: ) ))  ($#r1_hidden :::"="::: )  (Set   ($#k1_csspace :::"the_set_of_ComplexSequences"::: )  )) & (Bool  "("   "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Var "x")) "is"   ($#m1_subset_1 :::"Element":::) "of" (Set  ($#k7_csspace :::"Linear_Space_of_ComplexSequences"::: ) )) "iff" (Bool (Set (Var "x")) "is"   ($#m1_subset_1 :::"Complex_Sequence":::))  ")" )  ")" ) & (Bool  "("   "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Var "x")) "is"   ($#m1_subset_1 :::"VECTOR":::) "of" (Set  ($#k7_csspace :::"Linear_Space_of_ComplexSequences"::: ) )) "iff" (Bool (Set (Var "x")) "is"   ($#m1_subset_1 :::"Complex_Sequence":::))  ")" )  ")" ) & (Bool  "("   "for" (Set (Var "u")) "being"   ($#m1_subset_1 :::"VECTOR":::) "of" (Set  ($#k7_csspace :::"Linear_Space_of_ComplexSequences"::: ) ) "holds"  (Bool (Set (Var "u"))  ($#r1_hidden :::"="::: )  (Set   ($#k2_csspace :::"seq_id"::: )  (Set (Var "u"))))  ")" ) & (Bool  "("   "for" (Set (Var "u")) "," (Set (Var "v")) "being"   ($#m1_subset_1 :::"VECTOR":::) "of" (Set  ($#k7_csspace :::"Linear_Space_of_ComplexSequences"::: ) ) "holds"  (Bool (Set (Set (Var "u"))  ($#k3_rlvect_1 :::"+"::: )  (Set (Var "v")))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k2_csspace :::"seq_id"::: )  (Set (Var "u")) ")" )  ($#k1_series_1 :::"+"::: )  (Set  "("  ($#k2_csspace :::"seq_id"::: )  (Set (Var "v")) ")" )))  ")" ) & (Bool  "("   "for" (Set (Var "z")) "being"   ($#m1_hidden :::"Complex":::)  (Bool  "for" (Set (Var "u")) "being"   ($#m1_subset_1 :::"VECTOR":::) "of" (Set  ($#k7_csspace :::"Linear_Space_of_ComplexSequences"::: ) ) "holds"  (Bool (Set (Set (Var "z"))  ($#k1_clvect_1 :::"*"::: )  (Set (Var "u")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "z"))  ($#k25_valued_1 :::"(#)"::: )  (Set  "("  ($#k2_csspace :::"seq_id"::: )  (Set (Var "u")) ")" ))))  ")" )  ")" ) ; 
 begin  definitionattr "c1" is  :::"strict"::: ; struct  :::"CUNITSTR":::  ->    ($#l1_clvect_1 :::"CLSStruct"::: )  ; aggr :::"CUNITSTR":::(# :::"carrier":::, :::"ZeroF":::, :::"addF":::, :::"Mult":::, :::"scalar"::: #) ->    ($#l1_csspace :::"CUNITSTR"::: )  ; sel  :::"scalar"::: "c1" ->   ($#m1_subset_1 :::"Function":::) "of" (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "c1") "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "c1") ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set  ($#k2_numbers :::"COMPLEX"::: ) ); end; registration
cluster  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v1_csspace :::"strict"::: )    for    ($#l1_csspace :::"CUNITSTR"::: )  ; 
end; registrationlet "D" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )  ; let "Z" be    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Const "D")); let "a" be   ($#m1_subset_1 :::"BinOp":::) "of" (Set (Const "D")); let "m" be   ($#m1_subset_1 :::"Function":::) "of" (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set  ($#k2_numbers :::"COMPLEX"::: ) ) "," (Set (Const "D")) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set (Const "D")); let "s" be   ($#m1_subset_1 :::"Function":::) "of" (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set (Const "D")) "," (Set (Const "D")) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set  ($#k2_numbers :::"COMPLEX"::: ) ); 
cluster (Set   ($#g1_csspace :::"CUNITSTR"::: )  "(#"  "D" "," "Z" "," "a" "," "m" "," "s" "#)" ) ->  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )  ; 
end; 










definitionlet "X" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_csspace :::"CUNITSTR"::: )  ; let "x", "y" be   ($#m1_subset_1 :::"Point":::) "of" (Set (Const "X")); func "x" :::".|."::: "y" ->   ($#m1_hidden :::"Complex":::) equals :: CSSPACE:def 12 (Set (Set  "the"  ($#u1_csspace :::"scalar"::: )  "of" "X")  ($#k2_binop_1 :::"."::: )   "(" "x" "," "y" ")" ); end; 







:: deftheorem    defines :::".|."::: CSSPACE:def 12 :  (Bool  "for" (Set (Var "X")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_csspace :::"CUNITSTR"::: )    (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) "holds"  (Bool (Set (Set (Var "x"))  ($#k12_csspace :::".|."::: )  (Set (Var "y")))  ($#r1_hidden :::"="::: )  (Set (Set  "the"  ($#u1_csspace :::"scalar"::: )  "of" (Set (Var "X")))  ($#k2_binop_1 :::"."::: )   "(" (Set (Var "x")) "," (Set (Var "y")) ")" )))); 
 definitionlet "IT" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_csspace :::"CUNITSTR"::: )  ; attr "IT" is  :::"ComplexUnitarySpace-like":::  means :: CSSPACE:def 13 (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "w")) "being"   ($#m1_subset_1 :::"Point":::) "of" "IT"  (Bool  "for" (Set (Var "a")) "being"   ($#m1_hidden :::"Complex":::) "holds"   (Bool  "("   "("  (Bool (Bool (Set (Set (Var "x"))  ($#k12_csspace :::".|."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "implies" (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set   ($#k4_struct_0 :::"0."::: )  "IT"))  ")"  &  "("  (Bool (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set   ($#k4_struct_0 :::"0."::: )  "IT"))) "implies" (Bool (Set (Set (Var "x"))  ($#k12_csspace :::".|."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")"  & (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k3_complex1 :::"Re"::: )  (Set  "(" (Set (Var "x"))  ($#k12_csspace :::".|."::: )  (Set (Var "x")) ")" ))) & (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_hidden :::"="::: )  (Set   ($#k4_complex1 :::"Im"::: )  (Set  "(" (Set (Var "x"))  ($#k12_csspace :::".|."::: )  (Set (Var "x")) ")" ))) & (Bool (Set (Set (Var "x"))  ($#k12_csspace :::".|."::: )  (Set (Var "y")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "y"))  ($#k12_csspace :::".|."::: )  (Set (Var "x")) ")" )  ($#k15_complex1 :::"*'"::: )  )) & (Bool (Set (Set  "(" (Set (Var "x"))  ($#k1_algstr_0 :::"+"::: )  (Set (Var "y")) ")" )  ($#k12_csspace :::".|."::: )  (Set (Var "w")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "x"))  ($#k12_csspace :::".|."::: )  (Set (Var "w")) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" (Set (Var "y"))  ($#k12_csspace :::".|."::: )  (Set (Var "w")) ")" ))) & (Bool (Set (Set  "(" (Set (Var "a"))  ($#k1_clvect_1 :::"*"::: )  (Set (Var "x")) ")" )  ($#k12_csspace :::".|."::: )  (Set (Var "y")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "a"))  ($#k3_xcmplx_0 :::"*"::: )  (Set  "(" (Set (Var "x"))  ($#k12_csspace :::".|."::: )  (Set (Var "y")) ")" )))  ")" ))); end; 




:: deftheorem    defines :::"ComplexUnitarySpace-like"::: CSSPACE:def 13 :  (Bool  "for" (Set (Var "IT")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_csspace :::"CUNITSTR"::: )   "holds"   (Bool  "("  (Bool (Set (Var "IT")) "is"   ($#v2_csspace :::"ComplexUnitarySpace-like"::: )  ) "iff" (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "w")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set (Var "IT"))  (Bool  "for" (Set (Var "a")) "being"   ($#m1_hidden :::"Complex":::) "holds"   (Bool  "("   "("  (Bool (Bool (Set (Set (Var "x"))  ($#k12_csspace :::".|."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "implies" (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set   ($#k4_struct_0 :::"0."::: )  (Set (Var "IT"))))  ")"  &  "("  (Bool (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set   ($#k4_struct_0 :::"0."::: )  (Set (Var "IT"))))) "implies" (Bool (Set (Set (Var "x"))  ($#k12_csspace :::".|."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")"  & (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k3_complex1 :::"Re"::: )  (Set  "(" (Set (Var "x"))  ($#k12_csspace :::".|."::: )  (Set (Var "x")) ")" ))) & (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_hidden :::"="::: )  (Set   ($#k4_complex1 :::"Im"::: )  (Set  "(" (Set (Var "x"))  ($#k12_csspace :::".|."::: )  (Set (Var "x")) ")" ))) & (Bool (Set (Set (Var "x"))  ($#k12_csspace :::".|."::: )  (Set (Var "y")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "y"))  ($#k12_csspace :::".|."::: )  (Set (Var "x")) ")" )  ($#k15_complex1 :::"*'"::: )  )) & (Bool (Set (Set  "(" (Set (Var "x"))  ($#k1_algstr_0 :::"+"::: )  (Set (Var "y")) ")" )  ($#k12_csspace :::".|."::: )  (Set (Var "w")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "x"))  ($#k12_csspace :::".|."::: )  (Set (Var "w")) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" (Set (Var "y"))  ($#k12_csspace :::".|."::: )  (Set (Var "w")) ")" ))) & (Bool (Set (Set  "(" (Set (Var "a"))  ($#k1_clvect_1 :::"*"::: )  (Set (Var "x")) ")" )  ($#k12_csspace :::".|."::: )  (Set (Var "y")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "a"))  ($#k3_xcmplx_0 :::"*"::: )  (Set  "(" (Set (Var "x"))  ($#k12_csspace :::".|."::: )  (Set (Var "y")) ")" )))  ")" )))  ")" )); 
 registration
cluster  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v13_algstr_0 :::"right_complementable"::: )     ($#v2_rlvect_1 :::"Abelian"::: )     ($#v3_rlvect_1 :::"add-associative"::: )     ($#v4_rlvect_1 :::"right_zeroed"::: )     ($#v2_clvect_1 :::"vector-distributive"::: )     ($#v3_clvect_1 :::"scalar-distributive"::: )     ($#v4_clvect_1 :::"scalar-associative"::: )     ($#v5_clvect_1 :::"scalar-unital"::: )     ($#v1_csspace :::"strict"::: )     ($#v2_csspace :::"ComplexUnitarySpace-like"::: )    for    ($#l1_csspace :::"CUNITSTR"::: )  ; 
end; definitionmode ComplexUnitarySpace is  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v13_algstr_0 :::"right_complementable"::: )     ($#v2_rlvect_1 :::"Abelian"::: )     ($#v3_rlvect_1 :::"add-associative"::: )     ($#v4_rlvect_1 :::"right_zeroed"::: )     ($#v2_clvect_1 :::"vector-distributive"::: )     ($#v3_clvect_1 :::"scalar-distributive"::: )     ($#v4_clvect_1 :::"scalar-associative"::: )     ($#v5_clvect_1 :::"scalar-unital"::: )     ($#v2_csspace :::"ComplexUnitarySpace-like"::: )     ($#l1_csspace :::"CUNITSTR"::: )  ; end; 










theorem :: CSSPACE:16 (Bool  "for" (Set (Var "X")) "being"   ($#l1_csspace :::"ComplexUnitarySpace":::) "holds"  (Bool (Set (Set  "("  ($#k4_struct_0 :::"0."::: )  (Set (Var "X")) ")" )  ($#k12_csspace :::".|."::: )  (Set  "("  ($#k4_struct_0 :::"0."::: )  (Set (Var "X")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))) ; 
 
theorem :: CSSPACE:17 (Bool  "for" (Set (Var "X")) "being"   ($#l1_csspace :::"ComplexUnitarySpace":::)  (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) "holds"  (Bool (Set (Set (Var "x"))  ($#k12_csspace :::".|."::: )  (Set  "(" (Set (Var "y"))  ($#k3_rlvect_1 :::"+"::: )  (Set (Var "z")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "x"))  ($#k12_csspace :::".|."::: )  (Set (Var "y")) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" (Set (Var "x"))  ($#k12_csspace :::".|."::: )  (Set (Var "z")) ")" ))))) ; 
 
theorem :: CSSPACE:18 (Bool  "for" (Set (Var "a")) "being"   ($#m1_hidden :::"Complex":::)  (Bool  "for" (Set (Var "X")) "being"   ($#l1_csspace :::"ComplexUnitarySpace":::)  (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) "holds"  (Bool (Set (Set (Var "x"))  ($#k12_csspace :::".|."::: )  (Set  "(" (Set (Var "a"))  ($#k1_clvect_1 :::"*"::: )  (Set (Var "y")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "a"))  ($#k15_complex1 :::"*'"::: )  ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set  "(" (Set (Var "x"))  ($#k12_csspace :::".|."::: )  (Set (Var "y")) ")" )))))) ; 
 
theorem :: CSSPACE:19 (Bool  "for" (Set (Var "a")) "being"   ($#m1_hidden :::"Complex":::)  (Bool  "for" (Set (Var "X")) "being"   ($#l1_csspace :::"ComplexUnitarySpace":::)  (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) "holds"  (Bool (Set (Set  "(" (Set (Var "a"))  ($#k1_clvect_1 :::"*"::: )  (Set (Var "x")) ")" )  ($#k12_csspace :::".|."::: )  (Set (Var "y")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "x"))  ($#k12_csspace :::".|."::: )  (Set  "(" (Set  "(" (Set (Var "a"))  ($#k15_complex1 :::"*'"::: )  ")" )  ($#k1_clvect_1 :::"*"::: )  (Set (Var "y")) ")" )))))) ; 
 
theorem :: CSSPACE:20 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_hidden :::"Complex":::)  (Bool  "for" (Set (Var "X")) "being"   ($#l1_csspace :::"ComplexUnitarySpace":::)  (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) "holds"  (Bool (Set (Set  "(" (Set  "(" (Set (Var "a"))  ($#k1_clvect_1 :::"*"::: )  (Set (Var "x")) ")" )  ($#k3_rlvect_1 :::"+"::: )  (Set  "(" (Set (Var "b"))  ($#k1_clvect_1 :::"*"::: )  (Set (Var "y")) ")" ) ")" )  ($#k12_csspace :::".|."::: )  (Set (Var "z")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "a"))  ($#k3_xcmplx_0 :::"*"::: )  (Set  "(" (Set (Var "x"))  ($#k12_csspace :::".|."::: )  (Set (Var "z")) ")" ) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" (Set (Var "b"))  ($#k3_xcmplx_0 :::"*"::: )  (Set  "(" (Set (Var "y"))  ($#k12_csspace :::".|."::: )  (Set (Var "z")) ")" ) ")" )))))) ; 
 
theorem :: CSSPACE:21 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_hidden :::"Complex":::)  (Bool  "for" (Set (Var "X")) "being"   ($#l1_csspace :::"ComplexUnitarySpace":::)  (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) "holds"  (Bool (Set (Set (Var "x"))  ($#k12_csspace :::".|."::: )  (Set  "(" (Set  "(" (Set (Var "a"))  ($#k1_clvect_1 :::"*"::: )  (Set (Var "y")) ")" )  ($#k3_rlvect_1 :::"+"::: )  (Set  "(" (Set (Var "b"))  ($#k1_clvect_1 :::"*"::: )  (Set (Var "z")) ")" ) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set (Var "a"))  ($#k15_complex1 :::"*'"::: )  ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set  "(" (Set (Var "x"))  ($#k12_csspace :::".|."::: )  (Set (Var "y")) ")" ) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" (Set  "(" (Set (Var "b"))  ($#k15_complex1 :::"*'"::: )  ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set  "(" (Set (Var "x"))  ($#k12_csspace :::".|."::: )  (Set (Var "z")) ")" ) ")" )))))) ; 
 
theorem :: CSSPACE:22 (Bool  "for" (Set (Var "X")) "being"   ($#l1_csspace :::"ComplexUnitarySpace":::)  (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) "holds"  (Bool (Set (Set  "("  ($#k4_algstr_0 :::"-"::: )  (Set (Var "x")) ")" )  ($#k12_csspace :::".|."::: )  (Set (Var "y")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "x"))  ($#k12_csspace :::".|."::: )  (Set  "("  ($#k4_algstr_0 :::"-"::: )  (Set (Var "y")) ")" ))))) ; 
 
theorem :: CSSPACE:23 (Bool  "for" (Set (Var "X")) "being"   ($#l1_csspace :::"ComplexUnitarySpace":::)  (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) "holds"  (Bool (Set (Set  "("  ($#k4_algstr_0 :::"-"::: )  (Set (Var "x")) ")" )  ($#k12_csspace :::".|."::: )  (Set (Var "y")))  ($#r1_hidden :::"="::: )  (Set   ($#k4_xcmplx_0 :::"-"::: )  (Set  "(" (Set (Var "x"))  ($#k12_csspace :::".|."::: )  (Set (Var "y")) ")" ))))) ; 
 
theorem :: CSSPACE:24 (Bool  "for" (Set (Var "X")) "being"   ($#l1_csspace :::"ComplexUnitarySpace":::)  (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) "holds"  (Bool (Set (Set (Var "x"))  ($#k12_csspace :::".|."::: )  (Set  "("  ($#k4_algstr_0 :::"-"::: )  (Set (Var "y")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k4_xcmplx_0 :::"-"::: )  (Set  "(" (Set (Var "x"))  ($#k12_csspace :::".|."::: )  (Set (Var "y")) ")" ))))) ; 
 
theorem :: CSSPACE:25 (Bool  "for" (Set (Var "X")) "being"   ($#l1_csspace :::"ComplexUnitarySpace":::)  (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) "holds"  (Bool (Set (Set  "("  ($#k4_algstr_0 :::"-"::: )  (Set (Var "x")) ")" )  ($#k12_csspace :::".|."::: )  (Set  "("  ($#k4_algstr_0 :::"-"::: )  (Set (Var "y")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "x"))  ($#k12_csspace :::".|."::: )  (Set (Var "y")))))) ; 
 
theorem :: CSSPACE:26 (Bool  "for" (Set (Var "X")) "being"   ($#l1_csspace :::"ComplexUnitarySpace":::)  (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) "holds"  (Bool (Set (Set  "(" (Set (Var "x"))  ($#k5_algstr_0 :::"-"::: )  (Set (Var "y")) ")" )  ($#k12_csspace :::".|."::: )  (Set (Var "z")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "x"))  ($#k12_csspace :::".|."::: )  (Set (Var "z")) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" (Set (Var "y"))  ($#k12_csspace :::".|."::: )  (Set (Var "z")) ")" ))))) ; 
 
theorem :: CSSPACE:27 (Bool  "for" (Set (Var "X")) "being"   ($#l1_csspace :::"ComplexUnitarySpace":::)  (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) "holds"  (Bool (Set (Set (Var "x"))  ($#k12_csspace :::".|."::: )  (Set  "(" (Set (Var "y"))  ($#k5_algstr_0 :::"-"::: )  (Set (Var "z")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "x"))  ($#k12_csspace :::".|."::: )  (Set (Var "y")) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" (Set (Var "x"))  ($#k12_csspace :::".|."::: )  (Set (Var "z")) ")" ))))) ; 
 
theorem :: CSSPACE:28 (Bool  "for" (Set (Var "X")) "being"   ($#l1_csspace :::"ComplexUnitarySpace":::)  (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "u")) "," (Set (Var "v")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) "holds"  (Bool (Set (Set  "(" (Set (Var "x"))  ($#k5_algstr_0 :::"-"::: )  (Set (Var "y")) ")" )  ($#k12_csspace :::".|."::: )  (Set  "(" (Set (Var "u"))  ($#k5_algstr_0 :::"-"::: )  (Set (Var "v")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set  "(" (Set (Var "x"))  ($#k12_csspace :::".|."::: )  (Set (Var "u")) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" (Set (Var "x"))  ($#k12_csspace :::".|."::: )  (Set (Var "v")) ")" ) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" (Set (Var "y"))  ($#k12_csspace :::".|."::: )  (Set (Var "u")) ")" ) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" (Set (Var "y"))  ($#k12_csspace :::".|."::: )  (Set (Var "v")) ")" ))))) ; 
 
theorem :: CSSPACE:29 (Bool  "for" (Set (Var "X")) "being"   ($#l1_csspace :::"ComplexUnitarySpace":::)  (Bool  "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) "holds"  (Bool (Set (Set  "("  ($#k4_struct_0 :::"0."::: )  (Set (Var "X")) ")" )  ($#k12_csspace :::".|."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  )))) ; 
 
theorem :: CSSPACE:30 (Bool  "for" (Set (Var "X")) "being"   ($#l1_csspace :::"ComplexUnitarySpace":::)  (Bool  "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) "holds"  (Bool (Set (Set (Var "x"))  ($#k12_csspace :::".|."::: )  (Set  "("  ($#k4_struct_0 :::"0."::: )  (Set (Var "X")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  )))) ; 
 
theorem :: CSSPACE:31 (Bool  "for" (Set (Var "X")) "being"   ($#l1_csspace :::"ComplexUnitarySpace":::)  (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) "holds"  (Bool (Set (Set  "(" (Set (Var "x"))  ($#k3_rlvect_1 :::"+"::: )  (Set (Var "y")) ")" )  ($#k12_csspace :::".|."::: )  (Set  "(" (Set (Var "x"))  ($#k3_rlvect_1 :::"+"::: )  (Set (Var "y")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set  "(" (Set (Var "x"))  ($#k12_csspace :::".|."::: )  (Set (Var "x")) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" (Set (Var "x"))  ($#k12_csspace :::".|."::: )  (Set (Var "y")) ")" ) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" (Set (Var "y"))  ($#k12_csspace :::".|."::: )  (Set (Var "x")) ")" ) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" (Set (Var "y"))  ($#k12_csspace :::".|."::: )  (Set (Var "y")) ")" ))))) ; 
 
theorem :: CSSPACE:32 (Bool  "for" (Set (Var "X")) "being"   ($#l1_csspace :::"ComplexUnitarySpace":::)  (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) "holds"  (Bool (Set (Set  "(" (Set (Var "x"))  ($#k3_rlvect_1 :::"+"::: )  (Set (Var "y")) ")" )  ($#k12_csspace :::".|."::: )  (Set  "(" (Set (Var "x"))  ($#k5_algstr_0 :::"-"::: )  (Set (Var "y")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set  "(" (Set (Var "x"))  ($#k12_csspace :::".|."::: )  (Set (Var "x")) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" (Set (Var "x"))  ($#k12_csspace :::".|."::: )  (Set (Var "y")) ")" ) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" (Set (Var "y"))  ($#k12_csspace :::".|."::: )  (Set (Var "x")) ")" ) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" (Set (Var "y"))  ($#k12_csspace :::".|."::: )  (Set (Var "y")) ")" ))))) ; 
 
theorem :: CSSPACE:33 (Bool  "for" (Set (Var "X")) "being"   ($#l1_csspace :::"ComplexUnitarySpace":::)  (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) "holds"  (Bool (Set (Set  "(" (Set (Var "x"))  ($#k5_algstr_0 :::"-"::: )  (Set (Var "y")) ")" )  ($#k12_csspace :::".|."::: )  (Set  "(" (Set (Var "x"))  ($#k5_algstr_0 :::"-"::: )  (Set (Var "y")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set  "(" (Set (Var "x"))  ($#k12_csspace :::".|."::: )  (Set (Var "x")) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" (Set (Var "x"))  ($#k12_csspace :::".|."::: )  (Set (Var "y")) ")" ) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" (Set (Var "y"))  ($#k12_csspace :::".|."::: )  (Set (Var "x")) ")" ) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" (Set (Var "y"))  ($#k12_csspace :::".|."::: )  (Set (Var "y")) ")" ))))) ; 
 
theorem :: CSSPACE:34 (Bool  "for" (Set (Var "X")) "being"   ($#l1_csspace :::"ComplexUnitarySpace":::)  (Bool  "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) "holds"  (Bool (Set  ($#k17_complex1 :::"|."::: ) (Set  "(" (Set (Var "x"))  ($#k12_csspace :::".|."::: )  (Set (Var "x")) ")" ) ($#k17_complex1 :::".|"::: ) )  ($#r1_hidden :::"="::: )  (Set   ($#k3_complex1 :::"Re"::: )  (Set  "(" (Set (Var "x"))  ($#k12_csspace :::".|."::: )  (Set (Var "x")) ")" ))))) ; 
 
theorem :: CSSPACE:35 (Bool  "for" (Set (Var "X")) "being"   ($#l1_csspace :::"ComplexUnitarySpace":::)  (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) "holds"  (Bool (Set  ($#k17_complex1 :::"|."::: ) (Set  "(" (Set (Var "x"))  ($#k12_csspace :::".|."::: )  (Set (Var "y")) ")" ) ($#k17_complex1 :::".|"::: ) )  ($#r1_xxreal_0 :::"<="::: )  (Set (Set  "("  ($#k7_square_1 :::"sqrt"::: )  (Set  ($#k17_complex1 :::"|."::: ) (Set  "(" (Set (Var "x"))  ($#k12_csspace :::".|."::: )  (Set (Var "x")) ")" ) ($#k17_complex1 :::".|"::: ) ) ")" )  ($#k8_real_1 :::"*"::: )  (Set  "("  ($#k7_square_1 :::"sqrt"::: )  (Set  ($#k17_complex1 :::"|."::: ) (Set  "(" (Set (Var "y"))  ($#k12_csspace :::".|."::: )  (Set (Var "y")) ")" ) ($#k17_complex1 :::".|"::: ) ) ")" ))))) ; 
 definitionlet "X" be   ($#l1_csspace :::"ComplexUnitarySpace":::); let "x", "y" be   ($#m1_subset_1 :::"Point":::) "of" (Set (Const "X")); pred "x" "," "y" :::"are_orthogonal":::  means :: CSSPACE:def 14 (Bool (Set "x"  ($#k12_csspace :::".|."::: )  "y")  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  )); symmetry  
(Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set (Const "X"))  "st" (Bool (Bool (Set (Set (Var "x"))  ($#k12_csspace :::".|."::: )  (Set (Var "y")))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set (Set (Var "y"))  ($#k12_csspace :::".|."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  )))
 ; end; 






:: deftheorem    defines :::"are_orthogonal"::: CSSPACE:def 14 :  (Bool  "for" (Set (Var "X")) "being"   ($#l1_csspace :::"ComplexUnitarySpace":::)  (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) "holds"   (Bool  "("  (Bool (Set (Var "x")) "," (Set (Var "y"))  ($#r1_csspace :::"are_orthogonal"::: )  ) "iff" (Bool (Set (Set (Var "x"))  ($#k12_csspace :::".|."::: )  (Set (Var "y")))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")" ))); 
 
theorem :: CSSPACE:36 (Bool  "for" (Set (Var "X")) "being"   ($#l1_csspace :::"ComplexUnitarySpace":::)  (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X"))  "st" (Bool (Bool (Set (Var "x")) "," (Set (Var "y"))  ($#r1_csspace :::"are_orthogonal"::: )  )) "holds"  (Bool (Set (Var "x")) "," (Set   ($#k4_algstr_0 :::"-"::: )  (Set (Var "y")))  ($#r1_csspace :::"are_orthogonal"::: )  ))) ; 
 
theorem :: CSSPACE:37 (Bool  "for" (Set (Var "X")) "being"   ($#l1_csspace :::"ComplexUnitarySpace":::)  (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X"))  "st" (Bool (Bool (Set (Var "x")) "," (Set (Var "y"))  ($#r1_csspace :::"are_orthogonal"::: )  )) "holds"  (Bool (Set   ($#k4_algstr_0 :::"-"::: )  (Set (Var "x"))) "," (Set (Var "y"))  ($#r1_csspace :::"are_orthogonal"::: )  ))) ; 
 
theorem :: CSSPACE:38 (Bool  "for" (Set (Var "X")) "being"   ($#l1_csspace :::"ComplexUnitarySpace":::)  (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X"))  "st" (Bool (Bool (Set (Var "x")) "," (Set (Var "y"))  ($#r1_csspace :::"are_orthogonal"::: )  )) "holds"  (Bool (Set   ($#k4_algstr_0 :::"-"::: )  (Set (Var "x"))) "," (Set   ($#k4_algstr_0 :::"-"::: )  (Set (Var "y")))  ($#r1_csspace :::"are_orthogonal"::: )  ))) ; 
 
theorem :: CSSPACE:39 (Bool  "for" (Set (Var "X")) "being"   ($#l1_csspace :::"ComplexUnitarySpace":::)  (Bool  "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) "holds"  (Bool (Set (Var "x")) "," (Set   ($#k4_struct_0 :::"0."::: )  (Set (Var "X")))  ($#r1_csspace :::"are_orthogonal"::: )  ))) ; 
 
theorem :: CSSPACE:40 (Bool  "for" (Set (Var "X")) "being"   ($#l1_csspace :::"ComplexUnitarySpace":::)  (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X"))  "st" (Bool (Bool (Set (Var "x")) "," (Set (Var "y"))  ($#r1_csspace :::"are_orthogonal"::: )  )) "holds"  (Bool (Set (Set  "(" (Set (Var "x"))  ($#k3_rlvect_1 :::"+"::: )  (Set (Var "y")) ")" )  ($#k12_csspace :::".|."::: )  (Set  "(" (Set (Var "x"))  ($#k3_rlvect_1 :::"+"::: )  (Set (Var "y")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "x"))  ($#k12_csspace :::".|."::: )  (Set (Var "x")) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" (Set (Var "y"))  ($#k12_csspace :::".|."::: )  (Set (Var "y")) ")" ))))) ; 
 
theorem :: CSSPACE:41 (Bool  "for" (Set (Var "X")) "being"   ($#l1_csspace :::"ComplexUnitarySpace":::)  (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X"))  "st" (Bool (Bool (Set (Var "x")) "," (Set (Var "y"))  ($#r1_csspace :::"are_orthogonal"::: )  )) "holds"  (Bool (Set (Set  "(" (Set (Var "x"))  ($#k5_algstr_0 :::"-"::: )  (Set (Var "y")) ")" )  ($#k12_csspace :::".|."::: )  (Set  "(" (Set (Var "x"))  ($#k5_algstr_0 :::"-"::: )  (Set (Var "y")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "x"))  ($#k12_csspace :::".|."::: )  (Set (Var "x")) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" (Set (Var "y"))  ($#k12_csspace :::".|."::: )  (Set (Var "y")) ")" ))))) ; 
 definitionlet "X" be   ($#l1_csspace :::"ComplexUnitarySpace":::); let "x" be   ($#m1_subset_1 :::"Point":::) "of" (Set (Const "X")); func :::"||.":::"x":::".||"::: ->   ($#m1_subset_1 :::"Real":::) equals :: CSSPACE:def 15 (Set   ($#k7_square_1 :::"sqrt"::: )  (Set  ($#k17_complex1 :::"|."::: ) (Set  "(" "x"  ($#k12_csspace :::".|."::: )  "x" ")" ) ($#k17_complex1 :::".|"::: ) )); end; 






:: deftheorem    defines :::"||."::: CSSPACE:def 15 :  (Bool  "for" (Set (Var "X")) "being"   ($#l1_csspace :::"ComplexUnitarySpace":::)  (Bool  "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) "holds"  (Bool (Set  ($#k13_csspace :::"||."::: ) (Set (Var "x")) ($#k13_csspace :::".||"::: ) )  ($#r1_hidden :::"="::: )  (Set   ($#k7_square_1 :::"sqrt"::: )  (Set  ($#k17_complex1 :::"|."::: ) (Set  "(" (Set (Var "x"))  ($#k12_csspace :::".|."::: )  (Set (Var "x")) ")" ) ($#k17_complex1 :::".|"::: ) ))))); 
 
theorem :: CSSPACE:42 (Bool  "for" (Set (Var "X")) "being"   ($#l1_csspace :::"ComplexUnitarySpace":::)  (Bool  "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) "holds"   (Bool  "("  (Bool (Set  ($#k13_csspace :::"||."::: ) (Set (Var "x")) ($#k13_csspace :::".||"::: ) )  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  )) "iff" (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set   ($#k4_struct_0 :::"0."::: )  (Set (Var "X"))))  ")" ))) ; 
 
theorem :: CSSPACE:43 (Bool  "for" (Set (Var "a")) "being"   ($#m1_hidden :::"Complex":::)  (Bool  "for" (Set (Var "X")) "being"   ($#l1_csspace :::"ComplexUnitarySpace":::)  (Bool  "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) "holds"  (Bool (Set  ($#k13_csspace :::"||."::: ) (Set  "(" (Set (Var "a"))  ($#k1_clvect_1 :::"*"::: )  (Set (Var "x")) ")" ) ($#k13_csspace :::".||"::: ) )  ($#r1_hidden :::"="::: )  (Set (Set  ($#k17_complex1 :::"|."::: ) (Set (Var "a")) ($#k17_complex1 :::".|"::: ) )  ($#k8_real_1 :::"*"::: )  (Set  ($#k13_csspace :::"||."::: ) (Set (Var "x")) ($#k13_csspace :::".||"::: ) )))))) ; 
 
theorem :: CSSPACE:44 (Bool  "for" (Set (Var "X")) "being"   ($#l1_csspace :::"ComplexUnitarySpace":::)  (Bool  "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) "holds"  (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<="::: )  (Set  ($#k13_csspace :::"||."::: ) (Set (Var "x")) ($#k13_csspace :::".||"::: ) )))) ; 
 
theorem :: CSSPACE:45 (Bool  "for" (Set (Var "X")) "being"   ($#l1_csspace :::"ComplexUnitarySpace":::)  (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) "holds"  (Bool (Set  ($#k17_complex1 :::"|."::: ) (Set  "(" (Set (Var "x"))  ($#k12_csspace :::".|."::: )  (Set (Var "y")) ")" ) ($#k17_complex1 :::".|"::: ) )  ($#r1_xxreal_0 :::"<="::: )  (Set (Set  ($#k13_csspace :::"||."::: ) (Set (Var "x")) ($#k13_csspace :::".||"::: ) )  ($#k8_real_1 :::"*"::: )  (Set  ($#k13_csspace :::"||."::: ) (Set (Var "y")) ($#k13_csspace :::".||"::: ) ))))) ; 
 
theorem :: CSSPACE:46 (Bool  "for" (Set (Var "X")) "being"   ($#l1_csspace :::"ComplexUnitarySpace":::)  (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) "holds"  (Bool (Set  ($#k13_csspace :::"||."::: ) (Set  "(" (Set (Var "x"))  ($#k3_rlvect_1 :::"+"::: )  (Set (Var "y")) ")" ) ($#k13_csspace :::".||"::: ) )  ($#r1_xxreal_0 :::"<="::: )  (Set (Set  ($#k13_csspace :::"||."::: ) (Set (Var "x")) ($#k13_csspace :::".||"::: ) )  ($#k7_real_1 :::"+"::: )  (Set  ($#k13_csspace :::"||."::: ) (Set (Var "y")) ($#k13_csspace :::".||"::: ) ))))) ; 
 
theorem :: CSSPACE:47 (Bool  "for" (Set (Var "X")) "being"   ($#l1_csspace :::"ComplexUnitarySpace":::)  (Bool  "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) "holds"  (Bool (Set  ($#k13_csspace :::"||."::: ) (Set  "("  ($#k4_algstr_0 :::"-"::: )  (Set (Var "x")) ")" ) ($#k13_csspace :::".||"::: ) )  ($#r1_hidden :::"="::: )  (Set  ($#k13_csspace :::"||."::: ) (Set (Var "x")) ($#k13_csspace :::".||"::: ) )))) ; 
 
theorem :: CSSPACE:48 (Bool  "for" (Set (Var "X")) "being"   ($#l1_csspace :::"ComplexUnitarySpace":::)  (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) "holds"  (Bool (Set (Set  ($#k13_csspace :::"||."::: ) (Set (Var "x")) ($#k13_csspace :::".||"::: ) )  ($#k9_real_1 :::"-"::: )  (Set  ($#k13_csspace :::"||."::: ) (Set (Var "y")) ($#k13_csspace :::".||"::: ) ))  ($#r1_xxreal_0 :::"<="::: )  (Set  ($#k13_csspace :::"||."::: ) (Set  "(" (Set (Var "x"))  ($#k5_algstr_0 :::"-"::: )  (Set (Var "y")) ")" ) ($#k13_csspace :::".||"::: ) )))) ; 
 
theorem :: CSSPACE:49 (Bool  "for" (Set (Var "X")) "being"   ($#l1_csspace :::"ComplexUnitarySpace":::)  (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) "holds"  (Bool (Set   ($#k18_complex1 :::"abs"::: )  (Set  "(" (Set  ($#k13_csspace :::"||."::: ) (Set (Var "x")) ($#k13_csspace :::".||"::: ) )  ($#k9_real_1 :::"-"::: )  (Set  ($#k13_csspace :::"||."::: ) (Set (Var "y")) ($#k13_csspace :::".||"::: ) ) ")" ))  ($#r1_xxreal_0 :::"<="::: )  (Set  ($#k13_csspace :::"||."::: ) (Set  "(" (Set (Var "x"))  ($#k5_algstr_0 :::"-"::: )  (Set (Var "y")) ")" ) ($#k13_csspace :::".||"::: ) )))) ; 
 definitionlet "X" be   ($#l1_csspace :::"ComplexUnitarySpace":::); let "x", "y" be   ($#m1_subset_1 :::"Point":::) "of" (Set (Const "X")); func  :::"dist":::  "(" "x" "," "y" ")"  ->   ($#m1_subset_1 :::"Real":::) equals :: CSSPACE:def 16 (Set  ($#k13_csspace :::"||."::: ) (Set  "(" "x"  ($#k5_algstr_0 :::"-"::: )  "y" ")" ) ($#k13_csspace :::".||"::: ) ); end; 







:: deftheorem    defines :::"dist"::: CSSPACE:def 16 :  (Bool  "for" (Set (Var "X")) "being"   ($#l1_csspace :::"ComplexUnitarySpace":::)  (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) "holds"  (Bool (Set   ($#k14_csspace :::"dist"::: )   "(" (Set (Var "x")) "," (Set (Var "y")) ")" )  ($#r1_hidden :::"="::: )  (Set  ($#k13_csspace :::"||."::: ) (Set  "(" (Set (Var "x"))  ($#k5_algstr_0 :::"-"::: )  (Set (Var "y")) ")" ) ($#k13_csspace :::".||"::: ) )))); 
 definitionlet "X" be   ($#l1_csspace :::"ComplexUnitarySpace":::); let "x", "y" be   ($#m1_subset_1 :::"Point":::) "of" (Set (Const "X")); :: original: :::"dist"::: redefine func  :::"dist":::  "(" "x" "," "y" ")"  ->   ($#m1_subset_1 :::"Real":::); commutativity  
(Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set (Const "X")) "holds"  (Bool (Set   ($#k14_csspace :::"dist"::: )   "(" (Set (Var "x")) "," (Set (Var "y")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k14_csspace :::"dist"::: )   "(" (Set (Var "y")) "," (Set (Var "x")) ")" )))
 ; end; 
theorem :: CSSPACE:50 (Bool  "for" (Set (Var "X")) "being"   ($#l1_csspace :::"ComplexUnitarySpace":::)  (Bool  "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) "holds"  (Bool (Set   ($#k15_csspace :::"dist"::: )   "(" (Set (Var "x")) "," (Set (Var "x")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  )))) ; 
 
theorem :: CSSPACE:51 (Bool  "for" (Set (Var "X")) "being"   ($#l1_csspace :::"ComplexUnitarySpace":::)  (Bool  "for" (Set (Var "x")) "," (Set (Var "z")) "," (Set (Var "y")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) "holds"  (Bool (Set   ($#k15_csspace :::"dist"::: )   "(" (Set (Var "x")) "," (Set (Var "z")) ")" )  ($#r1_xxreal_0 :::"<="::: )  (Set (Set  "("  ($#k15_csspace :::"dist"::: )   "(" (Set (Var "x")) "," (Set (Var "y")) ")"  ")" )  ($#k7_real_1 :::"+"::: )  (Set  "("  ($#k15_csspace :::"dist"::: )   "(" (Set (Var "y")) "," (Set (Var "z")) ")"  ")" ))))) ; 
 
theorem :: CSSPACE:52 (Bool  "for" (Set (Var "X")) "being"   ($#l1_csspace :::"ComplexUnitarySpace":::)  (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) "holds"   (Bool  "("  (Bool (Set (Var "x"))  ($#r1_hidden :::"<>"::: )  (Set (Var "y"))) "iff" (Bool (Set   ($#k15_csspace :::"dist"::: )   "(" (Set (Var "x")) "," (Set (Var "y")) ")" )  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")" ))) ; 
 
theorem :: CSSPACE:53 (Bool  "for" (Set (Var "X")) "being"   ($#l1_csspace :::"ComplexUnitarySpace":::)  (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) "holds"  (Bool (Set   ($#k15_csspace :::"dist"::: )   "(" (Set (Var "x")) "," (Set (Var "y")) ")" )  ($#r1_xxreal_0 :::">="::: )  (Set   ($#k6_numbers :::"0"::: )  )))) ; 
 
theorem :: CSSPACE:54 (Bool  "for" (Set (Var "X")) "being"   ($#l1_csspace :::"ComplexUnitarySpace":::)  (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) "holds"   (Bool  "("  (Bool (Set (Var "x"))  ($#r1_hidden :::"<>"::: )  (Set (Var "y"))) "iff" (Bool (Set   ($#k15_csspace :::"dist"::: )   "(" (Set (Var "x")) "," (Set (Var "y")) ")" )  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")" ))) ; 
 
theorem :: CSSPACE:55 (Bool  "for" (Set (Var "X")) "being"   ($#l1_csspace :::"ComplexUnitarySpace":::)  (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) "holds"  (Bool (Set   ($#k15_csspace :::"dist"::: )   "(" (Set (Var "x")) "," (Set (Var "y")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k7_square_1 :::"sqrt"::: )  (Set  ($#k17_complex1 :::"|."::: ) (Set  "(" (Set  "(" (Set (Var "x"))  ($#k5_algstr_0 :::"-"::: )  (Set (Var "y")) ")" )  ($#k12_csspace :::".|."::: )  (Set  "(" (Set (Var "x"))  ($#k5_algstr_0 :::"-"::: )  (Set (Var "y")) ")" ) ")" ) ($#k17_complex1 :::".|"::: ) ))))) ; 
 
theorem :: CSSPACE:56 (Bool  "for" (Set (Var "X")) "being"   ($#l1_csspace :::"ComplexUnitarySpace":::)  (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "u")) "," (Set (Var "v")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) "holds"  (Bool (Set   ($#k15_csspace :::"dist"::: )   "(" (Set  "(" (Set (Var "x"))  ($#k3_rlvect_1 :::"+"::: )  (Set (Var "y")) ")" ) "," (Set  "(" (Set (Var "u"))  ($#k3_rlvect_1 :::"+"::: )  (Set (Var "v")) ")" ) ")" )  ($#r1_xxreal_0 :::"<="::: )  (Set (Set  "("  ($#k15_csspace :::"dist"::: )   "(" (Set (Var "x")) "," (Set (Var "u")) ")"  ")" )  ($#k7_real_1 :::"+"::: )  (Set  "("  ($#k15_csspace :::"dist"::: )   "(" (Set (Var "y")) "," (Set (Var "v")) ")"  ")" ))))) ; 
 
theorem :: CSSPACE:57 (Bool  "for" (Set (Var "X")) "being"   ($#l1_csspace :::"ComplexUnitarySpace":::)  (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "u")) "," (Set (Var "v")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) "holds"  (Bool (Set   ($#k15_csspace :::"dist"::: )   "(" (Set  "(" (Set (Var "x"))  ($#k5_algstr_0 :::"-"::: )  (Set (Var "y")) ")" ) "," (Set  "(" (Set (Var "u"))  ($#k5_algstr_0 :::"-"::: )  (Set (Var "v")) ")" ) ")" )  ($#r1_xxreal_0 :::"<="::: )  (Set (Set  "("  ($#k15_csspace :::"dist"::: )   "(" (Set (Var "x")) "," (Set (Var "u")) ")"  ")" )  ($#k7_real_1 :::"+"::: )  (Set  "("  ($#k15_csspace :::"dist"::: )   "(" (Set (Var "y")) "," (Set (Var "v")) ")"  ")" ))))) ; 
 
theorem :: CSSPACE:58 (Bool  "for" (Set (Var "X")) "being"   ($#l1_csspace :::"ComplexUnitarySpace":::)  (Bool  "for" (Set (Var "x")) "," (Set (Var "z")) "," (Set (Var "y")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) "holds"  (Bool (Set   ($#k15_csspace :::"dist"::: )   "(" (Set  "(" (Set (Var "x"))  ($#k5_algstr_0 :::"-"::: )  (Set (Var "z")) ")" ) "," (Set  "(" (Set (Var "y"))  ($#k5_algstr_0 :::"-"::: )  (Set (Var "z")) ")" ) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k15_csspace :::"dist"::: )   "(" (Set (Var "x")) "," (Set (Var "y")) ")" )))) ; 
 
theorem :: CSSPACE:59 (Bool  "for" (Set (Var "X")) "being"   ($#l1_csspace :::"ComplexUnitarySpace":::)  (Bool  "for" (Set (Var "x")) "," (Set (Var "z")) "," (Set (Var "y")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) "holds"  (Bool (Set   ($#k15_csspace :::"dist"::: )   "(" (Set  "(" (Set (Var "x"))  ($#k5_algstr_0 :::"-"::: )  (Set (Var "z")) ")" ) "," (Set  "(" (Set (Var "y"))  ($#k5_algstr_0 :::"-"::: )  (Set (Var "z")) ")" ) ")" )  ($#r1_xxreal_0 :::"<="::: )  (Set (Set  "("  ($#k15_csspace :::"dist"::: )   "(" (Set (Var "z")) "," (Set (Var "x")) ")"  ")" )  ($#k7_real_1 :::"+"::: )  (Set  "("  ($#k15_csspace :::"dist"::: )   "(" (Set (Var "z")) "," (Set (Var "y")) ")"  ")" ))))) ; 
 








definitionlet "X" be   ($#l1_csspace :::"ComplexUnitarySpace":::); let "seq1", "seq2" be   ($#m1_subset_1 :::"sequence":::) "of" (Set (Const "X")); :: original: :::"+"::: redefine func "seq1" :::"+"::: "seq2" ->    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k1_zfmisc_1 :::"bool"::: )  (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set  ($#k5_numbers :::"NAT"::: ) ) "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "X") ($#k2_zfmisc_1 :::":]"::: ) )); commutativity  
(Bool  "for" (Set (Var "seq1")) "," (Set (Var "seq2")) "being"   ($#m1_subset_1 :::"sequence":::) "of" (Set (Const "X")) "holds"  (Bool (Set (Set (Var "seq1"))  ($#k2_normsp_1 :::"+"::: )  (Set (Var "seq2")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "seq2"))  ($#k2_normsp_1 :::"+"::: )  (Set (Var "seq1")))))
 ; end; 
theorem :: CSSPACE:60 (Bool  "for" (Set (Var "X")) "being"   ($#l1_csspace :::"ComplexUnitarySpace":::)  (Bool  "for" (Set (Var "seq1")) "," (Set (Var "seq2")) "," (Set (Var "seq3")) "being"   ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X")) "holds"  (Bool (Set (Set (Var "seq1"))  ($#k16_csspace :::"+"::: )  (Set  "(" (Set (Var "seq2"))  ($#k16_csspace :::"+"::: )  (Set (Var "seq3")) ")" ))  ($#r2_funct_2 :::"="::: )  (Set (Set  "(" (Set (Var "seq1"))  ($#k16_csspace :::"+"::: )  (Set (Var "seq2")) ")" )  ($#k16_csspace :::"+"::: )  (Set (Var "seq3")))))) ; 
 
theorem :: CSSPACE:61 (Bool  "for" (Set (Var "X")) "being"   ($#l1_csspace :::"ComplexUnitarySpace":::)  (Bool  "for" (Set (Var "seq1")) "," (Set (Var "seq2")) "," (Set (Var "seq")) "being"   ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X"))  "st" (Bool (Bool (Set (Var "seq1")) "is"   ($#v3_funct_1 :::"constant"::: )  ) & (Bool (Set (Var "seq2")) "is"   ($#v3_funct_1 :::"constant"::: )  ) & (Bool (Set (Var "seq"))  ($#r2_funct_2 :::"="::: )  (Set (Set (Var "seq1"))  ($#k16_csspace :::"+"::: )  (Set (Var "seq2"))))) "holds"  (Bool (Set (Var "seq")) "is"   ($#v3_funct_1 :::"constant"::: )  ))) ; 
 
theorem :: CSSPACE:62 (Bool  "for" (Set (Var "X")) "being"   ($#l1_csspace :::"ComplexUnitarySpace":::)  (Bool  "for" (Set (Var "seq1")) "," (Set (Var "seq2")) "," (Set (Var "seq")) "being"   ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X"))  "st" (Bool (Bool (Set (Var "seq1")) "is"   ($#v3_funct_1 :::"constant"::: )  ) & (Bool (Set (Var "seq2")) "is"   ($#v3_funct_1 :::"constant"::: )  ) & (Bool (Set (Var "seq"))  ($#r2_funct_2 :::"="::: )  (Set (Set (Var "seq1"))  ($#k3_normsp_1 :::"-"::: )  (Set (Var "seq2"))))) "holds"  (Bool (Set (Var "seq")) "is"   ($#v3_funct_1 :::"constant"::: )  ))) ; 
 
theorem :: CSSPACE:63 (Bool  "for" (Set (Var "a")) "being"   ($#m1_hidden :::"Complex":::)  (Bool  "for" (Set (Var "X")) "being"   ($#l1_csspace :::"ComplexUnitarySpace":::)  (Bool  "for" (Set (Var "seq1")) "," (Set (Var "seq")) "being"   ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X"))  "st" (Bool (Bool (Set (Var "seq1")) "is"   ($#v3_funct_1 :::"constant"::: )  ) & (Bool (Set (Var "seq"))  ($#r2_funct_2 :::"="::: )  (Set (Set (Var "a"))  ($#k6_clvect_1 :::"*"::: )  (Set (Var "seq1"))))) "holds"  (Bool (Set (Var "seq")) "is"   ($#v3_funct_1 :::"constant"::: )  )))) ; 
 
theorem :: CSSPACE:64 (Bool  "for" (Set (Var "X")) "being"   ($#l1_csspace :::"ComplexUnitarySpace":::)  (Bool  "for" (Set (Var "seq1")) "," (Set (Var "seq2")) "being"   ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X")) "holds"  (Bool (Set (Set (Var "seq1"))  ($#k3_normsp_1 :::"-"::: )  (Set (Var "seq2")))  ($#r2_funct_2 :::"="::: )  (Set (Set (Var "seq1"))  ($#k16_csspace :::"+"::: )  (Set  "("  ($#k5_vfunct_1 :::"-"::: )  (Set (Var "seq2")) ")" ))))) ; 
 
theorem :: CSSPACE:65 (Bool  "for" (Set (Var "X")) "being"   ($#l1_csspace :::"ComplexUnitarySpace":::)  (Bool  "for" (Set (Var "seq")) "being"   ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X")) "holds"  (Bool (Set (Var "seq"))  ($#r2_funct_2 :::"="::: )  (Set (Set (Var "seq"))  ($#k5_bhsp_1 :::"+"::: )  (Set  "("  ($#k4_struct_0 :::"0."::: )  (Set (Var "X")) ")" ))))) ; 
 
theorem :: CSSPACE:66 (Bool  "for" (Set (Var "a")) "being"   ($#m1_hidden :::"Complex":::)  (Bool  "for" (Set (Var "X")) "being"   ($#l1_csspace :::"ComplexUnitarySpace":::)  (Bool  "for" (Set (Var "seq1")) "," (Set (Var "seq2")) "being"   ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X")) "holds"  (Bool (Set (Set (Var "a"))  ($#k6_clvect_1 :::"*"::: )  (Set  "(" (Set (Var "seq1"))  ($#k16_csspace :::"+"::: )  (Set (Var "seq2")) ")" ))  ($#r2_funct_2 :::"="::: )  (Set (Set  "(" (Set (Var "a"))  ($#k6_clvect_1 :::"*"::: )  (Set (Var "seq1")) ")" )  ($#k16_csspace :::"+"::: )  (Set  "(" (Set (Var "a"))  ($#k6_clvect_1 :::"*"::: )  (Set (Var "seq2")) ")" )))))) ; 
 
theorem :: CSSPACE:67 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_hidden :::"Complex":::)  (Bool  "for" (Set (Var "X")) "being"   ($#l1_csspace :::"ComplexUnitarySpace":::)  (Bool  "for" (Set (Var "seq")) "being"   ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X")) "holds"  (Bool (Set (Set  "(" (Set (Var "a"))  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "b")) ")" )  ($#k6_clvect_1 :::"*"::: )  (Set (Var "seq")))  ($#r2_funct_2 :::"="::: )  (Set (Set  "(" (Set (Var "a"))  ($#k6_clvect_1 :::"*"::: )  (Set (Var "seq")) ")" )  ($#k16_csspace :::"+"::: )  (Set  "(" (Set (Var "b"))  ($#k6_clvect_1 :::"*"::: )  (Set (Var "seq")) ")" )))))) ; 
 
theorem :: CSSPACE:68 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_hidden :::"Complex":::)  (Bool  "for" (Set (Var "X")) "being"   ($#l1_csspace :::"ComplexUnitarySpace":::)  (Bool  "for" (Set (Var "seq")) "being"   ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X")) "holds"  (Bool (Set (Set  "(" (Set (Var "a"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "b")) ")" )  ($#k6_clvect_1 :::"*"::: )  (Set (Var "seq")))  ($#r2_funct_2 :::"="::: )  (Set (Set (Var "a"))  ($#k6_clvect_1 :::"*"::: )  (Set  "(" (Set (Var "b"))  ($#k6_clvect_1 :::"*"::: )  (Set (Var "seq")) ")" )))))) ; 
 
theorem :: CSSPACE:69 (Bool  "for" (Set (Var "X")) "being"   ($#l1_csspace :::"ComplexUnitarySpace":::)  (Bool  "for" (Set (Var "seq")) "being"   ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X")) "holds"  (Bool (Set (Set  ($#k6_complex1 :::"1r"::: ) )  ($#k6_clvect_1 :::"*"::: )  (Set (Var "seq")))  ($#r2_funct_2 :::"="::: )  (Set (Var "seq"))))) ; 
 
theorem :: CSSPACE:70 (Bool  "for" (Set (Var "X")) "being"   ($#l1_csspace :::"ComplexUnitarySpace":::)  (Bool  "for" (Set (Var "seq")) "being"   ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X")) "holds"  (Bool (Set (Set  "("  ($#k10_complex1 :::"-"::: )  (Set  ($#k6_complex1 :::"1r"::: ) ) ")" )  ($#k6_clvect_1 :::"*"::: )  (Set (Var "seq")))  ($#r2_funct_2 :::"="::: )  (Set   ($#k5_vfunct_1 :::"-"::: )  (Set (Var "seq")))))) ; 
 
theorem :: CSSPACE:71 (Bool  "for" (Set (Var "X")) "being"   ($#l1_csspace :::"ComplexUnitarySpace":::)  (Bool  "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X"))  (Bool  "for" (Set (Var "seq")) "being"   ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X")) "holds"  (Bool (Set (Set (Var "seq"))  ($#k4_normsp_1 :::"-"::: )  (Set (Var "x")))  ($#r2_funct_2 :::"="::: )  (Set (Set (Var "seq"))  ($#k5_bhsp_1 :::"+"::: )  (Set  "("  ($#k4_algstr_0 :::"-"::: )  (Set (Var "x")) ")" )))))) ; 
 
theorem :: CSSPACE:72 (Bool  "for" (Set (Var "X")) "being"   ($#l1_csspace :::"ComplexUnitarySpace":::)  (Bool  "for" (Set (Var "seq1")) "," (Set (Var "seq2")) "being"   ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X")) "holds"  (Bool (Set (Set (Var "seq1"))  ($#k3_normsp_1 :::"-"::: )  (Set (Var "seq2")))  ($#r2_funct_2 :::"="::: )  (Set   ($#k5_vfunct_1 :::"-"::: )  (Set  "(" (Set (Var "seq2"))  ($#k3_normsp_1 :::"-"::: )  (Set (Var "seq1")) ")" ))))) ; 
 
theorem :: CSSPACE:73 (Bool  "for" (Set (Var "X")) "being"   ($#l1_csspace :::"ComplexUnitarySpace":::)  (Bool  "for" (Set (Var "seq")) "being"   ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X")) "holds"  (Bool (Set (Var "seq"))  ($#r2_funct_2 :::"="::: )  (Set (Set (Var "seq"))  ($#k4_normsp_1 :::"-"::: )  (Set  "("  ($#k4_struct_0 :::"0."::: )  (Set (Var "X")) ")" ))))) ; 
 
theorem :: CSSPACE:74 (Bool  "for" (Set (Var "X")) "being"   ($#l1_csspace :::"ComplexUnitarySpace":::)  (Bool  "for" (Set (Var "seq")) "being"   ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X")) "holds"  (Bool (Set (Var "seq"))  ($#r2_funct_2 :::"="::: )  (Set   ($#k5_vfunct_1 :::"-"::: )  (Set  "("  ($#k5_vfunct_1 :::"-"::: )  (Set (Var "seq")) ")" ))))) ; 
 
theorem :: CSSPACE:75 (Bool  "for" (Set (Var "X")) "being"   ($#l1_csspace :::"ComplexUnitarySpace":::)  (Bool  "for" (Set (Var "seq1")) "," (Set (Var "seq2")) "," (Set (Var "seq3")) "being"   ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X")) "holds"  (Bool (Set (Set (Var "seq1"))  ($#k3_normsp_1 :::"-"::: )  (Set  "(" (Set (Var "seq2"))  ($#k16_csspace :::"+"::: )  (Set (Var "seq3")) ")" ))  ($#r2_funct_2 :::"="::: )  (Set (Set  "(" (Set (Var "seq1"))  ($#k3_normsp_1 :::"-"::: )  (Set (Var "seq2")) ")" )  ($#k3_normsp_1 :::"-"::: )  (Set (Var "seq3")))))) ; 
 
theorem :: CSSPACE:76 (Bool  "for" (Set (Var "X")) "being"   ($#l1_csspace :::"ComplexUnitarySpace":::)  (Bool  "for" (Set (Var "seq1")) "," (Set (Var "seq2")) "," (Set (Var "seq3")) "being"   ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X")) "holds"  (Bool (Set (Set  "(" (Set (Var "seq1"))  ($#k16_csspace :::"+"::: )  (Set (Var "seq2")) ")" )  ($#k3_normsp_1 :::"-"::: )  (Set (Var "seq3")))  ($#r2_funct_2 :::"="::: )  (Set (Set (Var "seq1"))  ($#k16_csspace :::"+"::: )  (Set  "(" (Set (Var "seq2"))  ($#k3_normsp_1 :::"-"::: )  (Set (Var "seq3")) ")" ))))) ; 
 
theorem :: CSSPACE:77 (Bool  "for" (Set (Var "X")) "being"   ($#l1_csspace :::"ComplexUnitarySpace":::)  (Bool  "for" (Set (Var "seq1")) "," (Set (Var "seq2")) "," (Set (Var "seq3")) "being"   ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X")) "holds"  (Bool (Set (Set (Var "seq1"))  ($#k3_normsp_1 :::"-"::: )  (Set  "(" (Set (Var "seq2"))  ($#k3_normsp_1 :::"-"::: )  (Set (Var "seq3")) ")" ))  ($#r2_funct_2 :::"="::: )  (Set (Set  "(" (Set (Var "seq1"))  ($#k3_normsp_1 :::"-"::: )  (Set (Var "seq2")) ")" )  ($#k16_csspace :::"+"::: )  (Set (Var "seq3")))))) ; 
 
theorem :: CSSPACE:78 (Bool  "for" (Set (Var "a")) "being"   ($#m1_hidden :::"Complex":::)  (Bool  "for" (Set (Var "X")) "being"   ($#l1_csspace :::"ComplexUnitarySpace":::)  (Bool  "for" (Set (Var "seq1")) "," (Set (Var "seq2")) "being"   ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X")) "holds"  (Bool (Set (Set (Var "a"))  ($#k6_clvect_1 :::"*"::: )  (Set  "(" (Set (Var "seq1"))  ($#k3_normsp_1 :::"-"::: )  (Set (Var "seq2")) ")" ))  ($#r2_funct_2 :::"="::: )  (Set (Set  "(" (Set (Var "a"))  ($#k6_clvect_1 :::"*"::: )  (Set (Var "seq1")) ")" )  ($#k3_normsp_1 :::"-"::: )  (Set  "(" (Set (Var "a"))  ($#k6_clvect_1 :::"*"::: )  (Set (Var "seq2")) ")" )))))) ; 
 begin  definitionfunc  :::"cl_scalar":::  ->   ($#m1_subset_1 :::"Function":::) "of" (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set  ($#k11_csspace :::"the_set_of_l2ComplexSequences"::: ) ) "," (Set  ($#k11_csspace :::"the_set_of_l2ComplexSequences"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set  ($#k2_numbers :::"COMPLEX"::: ) ) means :: CSSPACE:def 17 (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set   ($#k11_csspace :::"the_set_of_l2ComplexSequences"::: )  )) & (Bool (Set (Var "y"))  ($#r2_hidden :::"in"::: )  (Set   ($#k11_csspace :::"the_set_of_l2ComplexSequences"::: )  ))) "holds"  (Bool (Set it  ($#k1_binop_1 :::"."::: )   "(" (Set (Var "x")) "," (Set (Var "y")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k11_comseq_3 :::"Sum"::: )  (Set  "(" (Set  "("  ($#k2_csspace :::"seq_id"::: )  (Set (Var "x")) ")" )  ($#k19_valued_1 :::"(#)"::: )  (Set  "(" (Set  "("  ($#k2_csspace :::"seq_id"::: )  (Set (Var "y")) ")" )  ($#k2_comseq_2 :::"*'"::: )  ")" ) ")" )))); end; 




:: deftheorem    defines :::"cl_scalar"::: CSSPACE:def 17 :  (Bool  "for" (Set (Var "b1")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set  ($#k11_csspace :::"the_set_of_l2ComplexSequences"::: ) ) "," (Set  ($#k11_csspace :::"the_set_of_l2ComplexSequences"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set  ($#k2_numbers :::"COMPLEX"::: ) ) "holds"   (Bool  "("  (Bool (Set (Var "b1"))  ($#r1_hidden :::"="::: )  (Set   ($#k17_csspace :::"cl_scalar"::: )  )) "iff" (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set   ($#k11_csspace :::"the_set_of_l2ComplexSequences"::: )  )) & (Bool (Set (Var "y"))  ($#r2_hidden :::"in"::: )  (Set   ($#k11_csspace :::"the_set_of_l2ComplexSequences"::: )  ))) "holds"  (Bool (Set (Set (Var "b1"))  ($#k1_binop_1 :::"."::: )   "(" (Set (Var "x")) "," (Set (Var "y")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k11_comseq_3 :::"Sum"::: )  (Set  "(" (Set  "("  ($#k2_csspace :::"seq_id"::: )  (Set (Var "x")) ")" )  ($#k19_valued_1 :::"(#)"::: )  (Set  "(" (Set  "("  ($#k2_csspace :::"seq_id"::: )  (Set (Var "y")) ")" )  ($#k2_comseq_2 :::"*'"::: )  ")" ) ")" ))))  ")" )); 
 registration
cluster (Set   ($#g1_csspace :::"CUNITSTR"::: )  "(#"  (Set  ($#k11_csspace :::"the_set_of_l2ComplexSequences"::: ) ) "," (Set  "("  ($#k10_csspace :::"Zero_"::: )   "(" (Set  ($#k11_csspace :::"the_set_of_l2ComplexSequences"::: ) ) "," (Set  ($#k7_csspace :::"Linear_Space_of_ComplexSequences"::: ) ) ")"  ")" ) "," (Set  "("  ($#k8_csspace :::"Add_"::: )   "(" (Set  ($#k11_csspace :::"the_set_of_l2ComplexSequences"::: ) ) "," (Set  ($#k7_csspace :::"Linear_Space_of_ComplexSequences"::: ) ) ")"  ")" ) "," (Set  "("  ($#k9_csspace :::"Mult_"::: )   "(" (Set  ($#k11_csspace :::"the_set_of_l2ComplexSequences"::: ) ) "," (Set  ($#k7_csspace :::"Linear_Space_of_ComplexSequences"::: ) ) ")"  ")" ) "," (Set  ($#k17_csspace :::"cl_scalar"::: ) ) "#)" ) ->  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )  ; 
end; definitionfunc  :::"Complex_l2_Space":::  ->  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_csspace :::"CUNITSTR"::: )   equals :: CSSPACE:def 18 (Set   ($#g1_csspace :::"CUNITSTR"::: )  "(#"  (Set  ($#k11_csspace :::"the_set_of_l2ComplexSequences"::: ) ) "," (Set  "("  ($#k10_csspace :::"Zero_"::: )   "(" (Set  ($#k11_csspace :::"the_set_of_l2ComplexSequences"::: ) ) "," (Set  ($#k7_csspace :::"Linear_Space_of_ComplexSequences"::: ) ) ")"  ")" ) "," (Set  "("  ($#k8_csspace :::"Add_"::: )   "(" (Set  ($#k11_csspace :::"the_set_of_l2ComplexSequences"::: ) ) "," (Set  ($#k7_csspace :::"Linear_Space_of_ComplexSequences"::: ) ) ")"  ")" ) "," (Set  "("  ($#k9_csspace :::"Mult_"::: )   "(" (Set  ($#k11_csspace :::"the_set_of_l2ComplexSequences"::: ) ) "," (Set  ($#k7_csspace :::"Linear_Space_of_ComplexSequences"::: ) ) ")"  ")" ) "," (Set  ($#k17_csspace :::"cl_scalar"::: ) ) "#)" ); end; 




:: deftheorem    defines :::"Complex_l2_Space"::: CSSPACE:def 18 :  (Bool (Set   ($#k18_csspace :::"Complex_l2_Space"::: )  )  ($#r1_hidden :::"="::: )  (Set   ($#g1_csspace :::"CUNITSTR"::: )  "(#"  (Set  ($#k11_csspace :::"the_set_of_l2ComplexSequences"::: ) ) "," (Set  "("  ($#k10_csspace :::"Zero_"::: )   "(" (Set  ($#k11_csspace :::"the_set_of_l2ComplexSequences"::: ) ) "," (Set  ($#k7_csspace :::"Linear_Space_of_ComplexSequences"::: ) ) ")"  ")" ) "," (Set  "("  ($#k8_csspace :::"Add_"::: )   "(" (Set  ($#k11_csspace :::"the_set_of_l2ComplexSequences"::: ) ) "," (Set  ($#k7_csspace :::"Linear_Space_of_ComplexSequences"::: ) ) ")"  ")" ) "," (Set  "("  ($#k9_csspace :::"Mult_"::: )   "(" (Set  ($#k11_csspace :::"the_set_of_l2ComplexSequences"::: ) ) "," (Set  ($#k7_csspace :::"Linear_Space_of_ComplexSequences"::: ) ) ")"  ")" ) "," (Set  ($#k17_csspace :::"cl_scalar"::: ) ) "#)" )); 
 
theorem :: CSSPACE:79 (Bool  "for" (Set (Var "l")) "being"    ($#l1_clvect_1 :::"CLSStruct"::: )    "st" (Bool (Bool (Set   ($#g1_clvect_1 :::"CLSStruct"::: )  "(#"  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "l"))) "," (Set  "the"  ($#u2_struct_0 :::"ZeroF"::: )  "of" (Set (Var "l"))) "," (Set  "the"  ($#u1_algstr_0 :::"addF"::: )  "of" (Set (Var "l"))) "," (Set  "the"  ($#u1_clvect_1 :::"Mult"::: )  "of" (Set (Var "l"))) "#)" ) "is"   ($#l1_clvect_1 :::"ComplexLinearSpace":::))) "holds"  (Bool (Set (Var "l")) "is"   ($#l1_clvect_1 :::"ComplexLinearSpace":::))) ; 
 
theorem :: CSSPACE:80 (Bool  "for" (Set (Var "seq")) "being"   ($#m1_subset_1 :::"Complex_Sequence":::)  "st" (Bool (Bool  "("   "for" (Set (Var "n")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"  (Bool (Set (Set (Var "seq"))  ($#k8_nat_1 :::"."::: )  (Set (Var "n")))  ($#r1_hidden :::"="::: )  (Set   ($#k5_complex1 :::"0c"::: )  ))  ")" )) "holds"  (Bool  "("  (Bool (Set (Var "seq")) "is"   ($#v1_comseq_3 :::"summable"::: )  ) & (Bool (Set   ($#k11_comseq_3 :::"Sum"::: )  (Set (Var "seq")))  ($#r1_hidden :::"="::: )  (Set   ($#k5_complex1 :::"0c"::: )  ))  ")" )) ; 
 registration
cluster (Set   ($#k18_csspace :::"Complex_l2_Space"::: )  ) ->  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v13_algstr_0 :::"right_complementable"::: )     ($#v2_rlvect_1 :::"Abelian"::: )     ($#v3_rlvect_1 :::"add-associative"::: )     ($#v4_rlvect_1 :::"right_zeroed"::: )     ($#v2_clvect_1 :::"vector-distributive"::: )     ($#v3_clvect_1 :::"scalar-distributive"::: )     ($#v4_clvect_1 :::"scalar-associative"::: )     ($#v5_clvect_1 :::"scalar-unital"::: )   ; 
end;