:: CFUNCDOM semantic presentation begin definitionlet "A" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; func :::"ComplexFuncAdd"::: "A" -> ($#m1_subset_1 :::"BinOp":::) "of" (Set "(" ($#k9_funct_2 :::"Funcs"::: ) "(" "A" "," (Set ($#k2_numbers :::"COMPLEX"::: ) ) ")" ")" ) means :: CFUNCDOM:def 1 (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k9_funct_2 :::"Funcs"::: ) "(" "A" "," (Set ($#k2_numbers :::"COMPLEX"::: ) ) ")" ) "holds" (Bool (Set it ($#k1_funcsdom :::"."::: ) "(" (Set (Var "f")) "," (Set (Var "g")) ")" ) ($#r2_funct_2 :::"="::: ) (Set (Set ($#k27_binop_2 :::"addcomplex"::: ) ) ($#k3_funcsdom :::".:"::: ) "(" (Set (Var "f")) "," (Set (Var "g")) ")" ))); end; :: deftheorem defines :::"ComplexFuncAdd"::: CFUNCDOM:def 1 : (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "b2")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set "(" ($#k9_funct_2 :::"Funcs"::: ) "(" (Set (Var "A")) "," (Set ($#k2_numbers :::"COMPLEX"::: ) ) ")" ")" ) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k1_cfuncdom :::"ComplexFuncAdd"::: ) (Set (Var "A")))) "iff" (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k9_funct_2 :::"Funcs"::: ) "(" (Set (Var "A")) "," (Set ($#k2_numbers :::"COMPLEX"::: ) ) ")" ) "holds" (Bool (Set (Set (Var "b2")) ($#k1_funcsdom :::"."::: ) "(" (Set (Var "f")) "," (Set (Var "g")) ")" ) ($#r2_funct_2 :::"="::: ) (Set (Set ($#k27_binop_2 :::"addcomplex"::: ) ) ($#k3_funcsdom :::".:"::: ) "(" (Set (Var "f")) "," (Set (Var "g")) ")" ))) ")" ))); definitionlet "A" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; func :::"ComplexFuncMult"::: "A" -> ($#m1_subset_1 :::"BinOp":::) "of" (Set "(" ($#k9_funct_2 :::"Funcs"::: ) "(" "A" "," (Set ($#k2_numbers :::"COMPLEX"::: ) ) ")" ")" ) means :: CFUNCDOM:def 2 (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k9_funct_2 :::"Funcs"::: ) "(" "A" "," (Set ($#k2_numbers :::"COMPLEX"::: ) ) ")" ) "holds" (Bool (Set it ($#k1_funcsdom :::"."::: ) "(" (Set (Var "f")) "," (Set (Var "g")) ")" ) ($#r2_funct_2 :::"="::: ) (Set (Set ($#k29_binop_2 :::"multcomplex"::: ) ) ($#k3_funcsdom :::".:"::: ) "(" (Set (Var "f")) "," (Set (Var "g")) ")" ))); end; :: deftheorem defines :::"ComplexFuncMult"::: CFUNCDOM:def 2 : (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "b2")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set "(" ($#k9_funct_2 :::"Funcs"::: ) "(" (Set (Var "A")) "," (Set ($#k2_numbers :::"COMPLEX"::: ) ) ")" ")" ) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k2_cfuncdom :::"ComplexFuncMult"::: ) (Set (Var "A")))) "iff" (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k9_funct_2 :::"Funcs"::: ) "(" (Set (Var "A")) "," (Set ($#k2_numbers :::"COMPLEX"::: ) ) ")" ) "holds" (Bool (Set (Set (Var "b2")) ($#k1_funcsdom :::"."::: ) "(" (Set (Var "f")) "," (Set (Var "g")) ")" ) ($#r2_funct_2 :::"="::: ) (Set (Set ($#k29_binop_2 :::"multcomplex"::: ) ) ($#k3_funcsdom :::".:"::: ) "(" (Set (Var "f")) "," (Set (Var "g")) ")" ))) ")" ))); definitionlet "A" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; func :::"ComplexFuncExtMult"::: "A" -> ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k2_numbers :::"COMPLEX"::: ) ) "," (Set "(" ($#k9_funct_2 :::"Funcs"::: ) "(" "A" "," (Set ($#k2_numbers :::"COMPLEX"::: ) ) ")" ")" ) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set "(" ($#k9_funct_2 :::"Funcs"::: ) "(" "A" "," (Set ($#k2_numbers :::"COMPLEX"::: ) ) ")" ")" ) means :: CFUNCDOM:def 3 (Bool "for" (Set (Var "z")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) (Bool "for" (Set (Var "f")) "being" ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k9_funct_2 :::"Funcs"::: ) "(" "A" "," (Set ($#k2_numbers :::"COMPLEX"::: ) ) ")" ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" "A" "holds" (Bool (Set (Set "(" it ($#k2_funcsdom :::"."::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "z")) "," (Set (Var "f")) ($#k1_domain_1 :::"]"::: ) ) ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "z")) ($#k9_complex1 :::"*"::: ) (Set "(" (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "x")) ")" )))))); end; :: deftheorem defines :::"ComplexFuncExtMult"::: CFUNCDOM:def 3 : (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "b2")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k2_numbers :::"COMPLEX"::: ) ) "," (Set "(" ($#k9_funct_2 :::"Funcs"::: ) "(" (Set (Var "A")) "," (Set ($#k2_numbers :::"COMPLEX"::: ) ) ")" ")" ) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set "(" ($#k9_funct_2 :::"Funcs"::: ) "(" (Set (Var "A")) "," (Set ($#k2_numbers :::"COMPLEX"::: ) ) ")" ")" ) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k3_cfuncdom :::"ComplexFuncExtMult"::: ) (Set (Var "A")))) "iff" (Bool "for" (Set (Var "z")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) (Bool "for" (Set (Var "f")) "being" ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k9_funct_2 :::"Funcs"::: ) "(" (Set (Var "A")) "," (Set ($#k2_numbers :::"COMPLEX"::: ) ) ")" ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "A")) "holds" (Bool (Set (Set "(" (Set (Var "b2")) ($#k2_funcsdom :::"."::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "z")) "," (Set (Var "f")) ($#k1_domain_1 :::"]"::: ) ) ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "z")) ($#k9_complex1 :::"*"::: ) (Set "(" (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "x")) ")" )))))) ")" ))); definitionlet "A" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; func :::"ComplexFuncZero"::: "A" -> ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k9_funct_2 :::"Funcs"::: ) "(" "A" "," (Set ($#k2_numbers :::"COMPLEX"::: ) ) ")" ) equals :: CFUNCDOM:def 4 (Set "A" ($#k8_funcop_1 :::"-->"::: ) (Set ($#k6_numbers :::"0"::: ) )); end; :: deftheorem defines :::"ComplexFuncZero"::: CFUNCDOM:def 4 : (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k4_cfuncdom :::"ComplexFuncZero"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "A")) ($#k8_funcop_1 :::"-->"::: ) (Set ($#k6_numbers :::"0"::: ) )))); definitionlet "A" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; func :::"ComplexFuncUnit"::: "A" -> ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k9_funct_2 :::"Funcs"::: ) "(" "A" "," (Set ($#k2_numbers :::"COMPLEX"::: ) ) ")" ) equals :: CFUNCDOM:def 5 (Set "A" ($#k8_funcop_1 :::"-->"::: ) (Set ($#k6_complex1 :::"1r"::: ) )); end; :: deftheorem defines :::"ComplexFuncUnit"::: CFUNCDOM:def 5 : (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k5_cfuncdom :::"ComplexFuncUnit"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "A")) ($#k8_funcop_1 :::"-->"::: ) (Set ($#k6_complex1 :::"1r"::: ) )))); theorem :: CFUNCDOM:1 (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "h")) "," (Set (Var "f")) "," (Set (Var "g")) "being" ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k9_funct_2 :::"Funcs"::: ) "(" (Set (Var "A")) "," (Set ($#k2_numbers :::"COMPLEX"::: ) ) ")" ) "holds" (Bool "(" (Bool (Set (Var "h")) ($#r2_funct_2 :::"="::: ) (Set (Set "(" ($#k1_cfuncdom :::"ComplexFuncAdd"::: ) (Set (Var "A")) ")" ) ($#k1_funcsdom :::"."::: ) "(" (Set (Var "f")) "," (Set (Var "g")) ")" )) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "A")) "holds" (Bool (Set (Set (Var "h")) ($#k3_funct_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "x")) ")" ) ($#k8_complex1 :::"+"::: ) (Set "(" (Set (Var "g")) ($#k3_funct_2 :::"."::: ) (Set (Var "x")) ")" )))) ")" ))) ; theorem :: CFUNCDOM:2 (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "h")) "," (Set (Var "f")) "," (Set (Var "g")) "being" ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k9_funct_2 :::"Funcs"::: ) "(" (Set (Var "A")) "," (Set ($#k2_numbers :::"COMPLEX"::: ) ) ")" ) "holds" (Bool "(" (Bool (Set (Var "h")) ($#r2_funct_2 :::"="::: ) (Set (Set "(" ($#k2_cfuncdom :::"ComplexFuncMult"::: ) (Set (Var "A")) ")" ) ($#k1_funcsdom :::"."::: ) "(" (Set (Var "f")) "," (Set (Var "g")) ")" )) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "A")) "holds" (Bool (Set (Set (Var "h")) ($#k3_funct_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "x")) ")" ) ($#k9_complex1 :::"*"::: ) (Set "(" (Set (Var "g")) ($#k3_funct_2 :::"."::: ) (Set (Var "x")) ")" )))) ")" ))) ; theorem :: CFUNCDOM:3 (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k4_cfuncdom :::"ComplexFuncZero"::: ) (Set (Var "A"))) ($#r1_hidden :::"<>"::: ) (Set ($#k5_cfuncdom :::"ComplexFuncUnit"::: ) (Set (Var "A"))))) ; theorem :: CFUNCDOM:4 (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "h")) "," (Set (Var "f")) "being" ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k9_funct_2 :::"Funcs"::: ) "(" (Set (Var "A")) "," (Set ($#k2_numbers :::"COMPLEX"::: ) ) ")" ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) "holds" (Bool "(" (Bool (Set (Var "h")) ($#r2_funct_2 :::"="::: ) (Set (Set "(" ($#k3_cfuncdom :::"ComplexFuncExtMult"::: ) (Set (Var "A")) ")" ) ($#k2_funcsdom :::"."::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "a")) "," (Set (Var "f")) ($#k1_domain_1 :::"]"::: ) ))) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "A")) "holds" (Bool (Set (Set (Var "h")) ($#k3_funct_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k9_complex1 :::"*"::: ) (Set "(" (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "x")) ")" )))) ")" )))) ; theorem :: CFUNCDOM:5 (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k9_funct_2 :::"Funcs"::: ) "(" (Set (Var "A")) "," (Set ($#k2_numbers :::"COMPLEX"::: ) ) ")" ) "holds" (Bool (Set (Set "(" ($#k1_cfuncdom :::"ComplexFuncAdd"::: ) (Set (Var "A")) ")" ) ($#k1_funcsdom :::"."::: ) "(" (Set (Var "f")) "," (Set (Var "g")) ")" ) ($#r2_funct_2 :::"="::: ) (Set (Set "(" ($#k1_cfuncdom :::"ComplexFuncAdd"::: ) (Set (Var "A")) ")" ) ($#k1_funcsdom :::"."::: ) "(" (Set (Var "g")) "," (Set (Var "f")) ")" )))) ; theorem :: CFUNCDOM:6 (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "," (Set (Var "h")) "being" ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k9_funct_2 :::"Funcs"::: ) "(" (Set (Var "A")) "," (Set ($#k2_numbers :::"COMPLEX"::: ) ) ")" ) "holds" (Bool (Set (Set "(" ($#k1_cfuncdom :::"ComplexFuncAdd"::: ) (Set (Var "A")) ")" ) ($#k1_funcsdom :::"."::: ) "(" (Set (Var "f")) "," (Set "(" (Set "(" ($#k1_cfuncdom :::"ComplexFuncAdd"::: ) (Set (Var "A")) ")" ) ($#k1_funcsdom :::"."::: ) "(" (Set (Var "g")) "," (Set (Var "h")) ")" ")" ) ")" ) ($#r2_funct_2 :::"="::: ) (Set (Set "(" ($#k1_cfuncdom :::"ComplexFuncAdd"::: ) (Set (Var "A")) ")" ) ($#k1_funcsdom :::"."::: ) "(" (Set "(" (Set "(" ($#k1_cfuncdom :::"ComplexFuncAdd"::: ) (Set (Var "A")) ")" ) ($#k1_funcsdom :::"."::: ) "(" (Set (Var "f")) "," (Set (Var "g")) ")" ")" ) "," (Set (Var "h")) ")" )))) ; theorem :: CFUNCDOM:7 (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k9_funct_2 :::"Funcs"::: ) "(" (Set (Var "A")) "," (Set ($#k2_numbers :::"COMPLEX"::: ) ) ")" ) "holds" (Bool (Set (Set "(" ($#k2_cfuncdom :::"ComplexFuncMult"::: ) (Set (Var "A")) ")" ) ($#k1_funcsdom :::"."::: ) "(" (Set (Var "f")) "," (Set (Var "g")) ")" ) ($#r2_funct_2 :::"="::: ) (Set (Set "(" ($#k2_cfuncdom :::"ComplexFuncMult"::: ) (Set (Var "A")) ")" ) ($#k1_funcsdom :::"."::: ) "(" (Set (Var "g")) "," (Set (Var "f")) ")" )))) ; theorem :: CFUNCDOM:8 (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "," (Set (Var "h")) "being" ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k9_funct_2 :::"Funcs"::: ) "(" (Set (Var "A")) "," (Set ($#k2_numbers :::"COMPLEX"::: ) ) ")" ) "holds" (Bool (Set (Set "(" ($#k2_cfuncdom :::"ComplexFuncMult"::: ) (Set (Var "A")) ")" ) ($#k1_funcsdom :::"."::: ) "(" (Set (Var "f")) "," (Set "(" (Set "(" ($#k2_cfuncdom :::"ComplexFuncMult"::: ) (Set (Var "A")) ")" ) ($#k1_funcsdom :::"."::: ) "(" (Set (Var "g")) "," (Set (Var "h")) ")" ")" ) ")" ) ($#r2_funct_2 :::"="::: ) (Set (Set "(" ($#k2_cfuncdom :::"ComplexFuncMult"::: ) (Set (Var "A")) ")" ) ($#k1_funcsdom :::"."::: ) "(" (Set "(" (Set "(" ($#k2_cfuncdom :::"ComplexFuncMult"::: ) (Set (Var "A")) ")" ) ($#k1_funcsdom :::"."::: ) "(" (Set (Var "f")) "," (Set (Var "g")) ")" ")" ) "," (Set (Var "h")) ")" )))) ; theorem :: CFUNCDOM:9 (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k9_funct_2 :::"Funcs"::: ) "(" (Set (Var "A")) "," (Set ($#k2_numbers :::"COMPLEX"::: ) ) ")" ) "holds" (Bool (Set (Set "(" ($#k2_cfuncdom :::"ComplexFuncMult"::: ) (Set (Var "A")) ")" ) ($#k1_funcsdom :::"."::: ) "(" (Set "(" ($#k5_cfuncdom :::"ComplexFuncUnit"::: ) (Set (Var "A")) ")" ) "," (Set (Var "f")) ")" ) ($#r2_funct_2 :::"="::: ) (Set (Var "f"))))) ; theorem :: CFUNCDOM:10 (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k9_funct_2 :::"Funcs"::: ) "(" (Set (Var "A")) "," (Set ($#k2_numbers :::"COMPLEX"::: ) ) ")" ) "holds" (Bool (Set (Set "(" ($#k1_cfuncdom :::"ComplexFuncAdd"::: ) (Set (Var "A")) ")" ) ($#k1_funcsdom :::"."::: ) "(" (Set "(" ($#k4_cfuncdom :::"ComplexFuncZero"::: ) (Set (Var "A")) ")" ) "," (Set (Var "f")) ")" ) ($#r2_funct_2 :::"="::: ) (Set (Var "f"))))) ; theorem :: CFUNCDOM:11 (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k9_funct_2 :::"Funcs"::: ) "(" (Set (Var "A")) "," (Set ($#k2_numbers :::"COMPLEX"::: ) ) ")" ) "holds" (Bool (Set (Set "(" ($#k1_cfuncdom :::"ComplexFuncAdd"::: ) (Set (Var "A")) ")" ) ($#k1_funcsdom :::"."::: ) "(" (Set (Var "f")) "," (Set "(" (Set "(" ($#k3_cfuncdom :::"ComplexFuncExtMult"::: ) (Set (Var "A")) ")" ) ($#k2_funcsdom :::"."::: ) (Set ($#k1_domain_1 :::"["::: ) (Set "(" ($#k10_complex1 :::"-"::: ) (Set ($#k6_complex1 :::"1r"::: ) ) ")" ) "," (Set (Var "f")) ($#k1_domain_1 :::"]"::: ) ) ")" ) ")" ) ($#r2_funct_2 :::"="::: ) (Set ($#k4_cfuncdom :::"ComplexFuncZero"::: ) (Set (Var "A")))))) ; theorem :: CFUNCDOM:12 (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k9_funct_2 :::"Funcs"::: ) "(" (Set (Var "A")) "," (Set ($#k2_numbers :::"COMPLEX"::: ) ) ")" ) "holds" (Bool (Set (Set "(" ($#k3_cfuncdom :::"ComplexFuncExtMult"::: ) (Set (Var "A")) ")" ) ($#k2_funcsdom :::"."::: ) (Set ($#k1_domain_1 :::"["::: ) (Set ($#k6_complex1 :::"1r"::: ) ) "," (Set (Var "f")) ($#k1_domain_1 :::"]"::: ) )) ($#r2_funct_2 :::"="::: ) (Set (Var "f"))))) ; theorem :: CFUNCDOM:13 (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k9_funct_2 :::"Funcs"::: ) "(" (Set (Var "A")) "," (Set ($#k2_numbers :::"COMPLEX"::: ) ) ")" ) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_hidden :::"Complex":::) "holds" (Bool (Set (Set "(" ($#k3_cfuncdom :::"ComplexFuncExtMult"::: ) (Set (Var "A")) ")" ) ($#k1_funct_1 :::"."::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "a")) "," (Set "(" (Set "(" ($#k3_cfuncdom :::"ComplexFuncExtMult"::: ) (Set (Var "A")) ")" ) ($#k1_funct_1 :::"."::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "b")) "," (Set (Var "f")) ($#k4_tarski :::"]"::: ) ) ")" ) ($#k4_tarski :::"]"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k3_cfuncdom :::"ComplexFuncExtMult"::: ) (Set (Var "A")) ")" ) ($#k2_funcsdom :::"."::: ) (Set ($#k1_domain_1 :::"["::: ) (Set "(" (Set (Var "a")) ($#k5_binop_2 :::"*"::: ) (Set (Var "b")) ")" ) "," (Set (Var "f")) ($#k1_domain_1 :::"]"::: ) )))))) ; theorem :: CFUNCDOM:14 (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k9_funct_2 :::"Funcs"::: ) "(" (Set (Var "A")) "," (Set ($#k2_numbers :::"COMPLEX"::: ) ) ")" ) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_hidden :::"Complex":::) "holds" (Bool (Set (Set "(" ($#k1_cfuncdom :::"ComplexFuncAdd"::: ) (Set (Var "A")) ")" ) ($#k1_binop_1 :::"."::: ) "(" (Set "(" (Set "(" ($#k3_cfuncdom :::"ComplexFuncExtMult"::: ) (Set (Var "A")) ")" ) ($#k1_funct_1 :::"."::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "a")) "," (Set (Var "f")) ($#k4_tarski :::"]"::: ) ) ")" ) "," (Set "(" (Set "(" ($#k3_cfuncdom :::"ComplexFuncExtMult"::: ) (Set (Var "A")) ")" ) ($#k1_funct_1 :::"."::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "b")) "," (Set (Var "f")) ($#k4_tarski :::"]"::: ) ) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k3_cfuncdom :::"ComplexFuncExtMult"::: ) (Set (Var "A")) ")" ) ($#k2_funcsdom :::"."::: ) (Set ($#k1_domain_1 :::"["::: ) (Set "(" (Set (Var "a")) ($#k3_binop_2 :::"+"::: ) (Set (Var "b")) ")" ) "," (Set (Var "f")) ($#k1_domain_1 :::"]"::: ) )))))) ; theorem :: CFUNCDOM:15 (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "," (Set (Var "h")) "being" ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k9_funct_2 :::"Funcs"::: ) "(" (Set (Var "A")) "," (Set ($#k2_numbers :::"COMPLEX"::: ) ) ")" ) "holds" (Bool (Set (Set "(" ($#k2_cfuncdom :::"ComplexFuncMult"::: ) (Set (Var "A")) ")" ) ($#k1_funcsdom :::"."::: ) "(" (Set (Var "f")) "," (Set "(" (Set "(" ($#k1_cfuncdom :::"ComplexFuncAdd"::: ) (Set (Var "A")) ")" ) ($#k1_funcsdom :::"."::: ) "(" (Set (Var "g")) "," (Set (Var "h")) ")" ")" ) ")" ) ($#r2_funct_2 :::"="::: ) (Set (Set "(" ($#k1_cfuncdom :::"ComplexFuncAdd"::: ) (Set (Var "A")) ")" ) ($#k1_funcsdom :::"."::: ) "(" (Set "(" (Set "(" ($#k2_cfuncdom :::"ComplexFuncMult"::: ) (Set (Var "A")) ")" ) ($#k1_funcsdom :::"."::: ) "(" (Set (Var "f")) "," (Set (Var "g")) ")" ")" ) "," (Set "(" (Set "(" ($#k2_cfuncdom :::"ComplexFuncMult"::: ) (Set (Var "A")) ")" ) ($#k1_funcsdom :::"."::: ) "(" (Set (Var "f")) "," (Set (Var "h")) ")" ")" ) ")" )))) ; theorem :: CFUNCDOM:16 (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k9_funct_2 :::"Funcs"::: ) "(" (Set (Var "A")) "," (Set ($#k2_numbers :::"COMPLEX"::: ) ) ")" ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) "holds" (Bool (Set (Set "(" ($#k2_cfuncdom :::"ComplexFuncMult"::: ) (Set (Var "A")) ")" ) ($#k1_funcsdom :::"."::: ) "(" (Set "(" (Set "(" ($#k3_cfuncdom :::"ComplexFuncExtMult"::: ) (Set (Var "A")) ")" ) ($#k2_funcsdom :::"."::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "a")) "," (Set (Var "f")) ($#k1_domain_1 :::"]"::: ) ) ")" ) "," (Set (Var "g")) ")" ) ($#r2_funct_2 :::"="::: ) (Set (Set "(" ($#k3_cfuncdom :::"ComplexFuncExtMult"::: ) (Set (Var "A")) ")" ) ($#k2_funcsdom :::"."::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "a")) "," (Set "(" (Set "(" ($#k2_cfuncdom :::"ComplexFuncMult"::: ) (Set (Var "A")) ")" ) ($#k1_funcsdom :::"."::: ) "(" (Set (Var "f")) "," (Set (Var "g")) ")" ")" ) ($#k1_domain_1 :::"]"::: ) )))))) ; begin theorem :: CFUNCDOM:17 (Bool "for" (Set (Var "x1")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "ex" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k9_funct_2 :::"Funcs"::: ) "(" (Set (Var "A")) "," (Set ($#k2_numbers :::"COMPLEX"::: ) ) ")" ) "st" (Bool "(" (Bool "(" "for" (Set (Var "z")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "z")) ($#r2_hidden :::"in"::: ) (Set (Var "A")))) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "z")) ($#r1_hidden :::"="::: ) (Set (Var "x1")))) "implies" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "z"))) ($#r1_hidden :::"="::: ) (Set ($#k6_complex1 :::"1r"::: ) )) ")" & "(" (Bool (Bool (Set (Var "z")) ($#r1_hidden :::"<>"::: ) (Set (Var "x1")))) "implies" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "z"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" ")" ) ")" ) & (Bool "(" "for" (Set (Var "z")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "z")) ($#r2_hidden :::"in"::: ) (Set (Var "A")))) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "z")) ($#r1_hidden :::"="::: ) (Set (Var "x1")))) "implies" (Bool (Set (Set (Var "g")) ($#k1_funct_1 :::"."::: ) (Set (Var "z"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" & "(" (Bool (Bool (Set (Var "z")) ($#r1_hidden :::"<>"::: ) (Set (Var "x1")))) "implies" (Bool (Set (Set (Var "g")) ($#k1_funct_1 :::"."::: ) (Set (Var "z"))) ($#r1_hidden :::"="::: ) (Set ($#k6_complex1 :::"1r"::: ) )) ")" ")" ) ")" ) ")" )))) ; theorem :: CFUNCDOM:18 (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k9_funct_2 :::"Funcs"::: ) "(" (Set (Var "A")) "," (Set ($#k2_numbers :::"COMPLEX"::: ) ) ")" ) "st" (Bool (Bool (Set (Var "x1")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) & (Bool (Set (Var "x2")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) & (Bool (Set (Var "x1")) ($#r1_hidden :::"<>"::: ) (Set (Var "x2"))) & (Bool "(" "for" (Set (Var "z")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "z")) ($#r2_hidden :::"in"::: ) (Set (Var "A")))) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "z")) ($#r1_hidden :::"="::: ) (Set (Var "x1")))) "implies" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "z"))) ($#r1_hidden :::"="::: ) (Set ($#k6_complex1 :::"1r"::: ) )) ")" & "(" (Bool (Bool (Set (Var "z")) ($#r1_hidden :::"<>"::: ) (Set (Var "x1")))) "implies" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "z"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" ")" ) ")" ) & (Bool "(" "for" (Set (Var "z")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "z")) ($#r2_hidden :::"in"::: ) (Set (Var "A")))) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "z")) ($#r1_hidden :::"="::: ) (Set (Var "x1")))) "implies" (Bool (Set (Set (Var "g")) ($#k1_funct_1 :::"."::: ) (Set (Var "z"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" & "(" (Bool (Bool (Set (Var "z")) ($#r1_hidden :::"<>"::: ) (Set (Var "x1")))) "implies" (Bool (Set (Set (Var "g")) ($#k1_funct_1 :::"."::: ) (Set (Var "z"))) ($#r1_hidden :::"="::: ) (Set ($#k6_complex1 :::"1r"::: ) )) ")" ")" ) ")" )) "holds" (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) "st" (Bool (Bool (Set (Set "(" ($#k1_cfuncdom :::"ComplexFuncAdd"::: ) (Set (Var "A")) ")" ) ($#k1_funcsdom :::"."::: ) "(" (Set "(" (Set "(" ($#k3_cfuncdom :::"ComplexFuncExtMult"::: ) (Set (Var "A")) ")" ) ($#k2_funcsdom :::"."::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "a")) "," (Set (Var "f")) ($#k1_domain_1 :::"]"::: ) ) ")" ) "," (Set "(" (Set "(" ($#k3_cfuncdom :::"ComplexFuncExtMult"::: ) (Set (Var "A")) ")" ) ($#k2_funcsdom :::"."::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "b")) "," (Set (Var "g")) ($#k1_domain_1 :::"]"::: ) ) ")" ) ")" ) ($#r2_funct_2 :::"="::: ) (Set ($#k4_cfuncdom :::"ComplexFuncZero"::: ) (Set (Var "A"))))) "holds" (Bool "(" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set ($#k5_complex1 :::"0c"::: ) )) & (Bool (Set (Var "b")) ($#r1_hidden :::"="::: ) (Set ($#k5_complex1 :::"0c"::: ) )) ")" ))))) ; theorem :: CFUNCDOM:19 (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x1")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) & (Bool (Set (Var "x2")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) & (Bool (Set (Var "x1")) ($#r1_hidden :::"<>"::: ) (Set (Var "x2")))) "holds" (Bool "ex" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k9_funct_2 :::"Funcs"::: ) "(" (Set (Var "A")) "," (Set ($#k2_numbers :::"COMPLEX"::: ) ) ")" ) "st" (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) "st" (Bool (Bool (Set (Set "(" ($#k1_cfuncdom :::"ComplexFuncAdd"::: ) (Set (Var "A")) ")" ) ($#k1_funcsdom :::"."::: ) "(" (Set "(" (Set "(" ($#k3_cfuncdom :::"ComplexFuncExtMult"::: ) (Set (Var "A")) ")" ) ($#k2_funcsdom :::"."::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "a")) "," (Set (Var "f")) ($#k1_domain_1 :::"]"::: ) ) ")" ) "," (Set "(" (Set "(" ($#k3_cfuncdom :::"ComplexFuncExtMult"::: ) (Set (Var "A")) ")" ) ($#k2_funcsdom :::"."::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "b")) "," (Set (Var "g")) ($#k1_domain_1 :::"]"::: ) ) ")" ) ")" ) ($#r2_funct_2 :::"="::: ) (Set ($#k4_cfuncdom :::"ComplexFuncZero"::: ) (Set (Var "A"))))) "holds" (Bool "(" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "b")) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" ))))) ; theorem :: CFUNCDOM:20 (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k9_funct_2 :::"Funcs"::: ) "(" (Set (Var "A")) "," (Set ($#k2_numbers :::"COMPLEX"::: ) ) ")" ) "st" (Bool (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set ($#k2_tarski :::"{"::: ) (Set (Var "x1")) "," (Set (Var "x2")) ($#k2_tarski :::"}"::: ) )) & (Bool (Set (Var "x1")) ($#r1_hidden :::"<>"::: ) (Set (Var "x2"))) & (Bool "(" "for" (Set (Var "z")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "z")) ($#r2_hidden :::"in"::: ) (Set (Var "A")))) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "z")) ($#r1_hidden :::"="::: ) (Set (Var "x1")))) "implies" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "z"))) ($#r1_hidden :::"="::: ) (Set ($#k6_complex1 :::"1r"::: ) )) ")" & "(" (Bool (Bool (Set (Var "z")) ($#r1_hidden :::"<>"::: ) (Set (Var "x1")))) "implies" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "z"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" ")" ) ")" ) & (Bool "(" "for" (Set (Var "z")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "z")) ($#r2_hidden :::"in"::: ) (Set (Var "A")))) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "z")) ($#r1_hidden :::"="::: ) (Set (Var "x1")))) "implies" (Bool (Set (Set (Var "g")) ($#k1_funct_1 :::"."::: ) (Set (Var "z"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" & "(" (Bool (Bool (Set (Var "z")) ($#r1_hidden :::"<>"::: ) (Set (Var "x1")))) "implies" (Bool (Set (Set (Var "g")) ($#k1_funct_1 :::"."::: ) (Set (Var "z"))) ($#r1_hidden :::"="::: ) (Set ($#k6_complex1 :::"1r"::: ) )) ")" ")" ) ")" )) "holds" (Bool "for" (Set (Var "h")) "being" ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k9_funct_2 :::"Funcs"::: ) "(" (Set (Var "A")) "," (Set ($#k2_numbers :::"COMPLEX"::: ) ) ")" ) (Bool "ex" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) "st" (Bool (Set (Var "h")) ($#r2_funct_2 :::"="::: ) (Set (Set "(" ($#k1_cfuncdom :::"ComplexFuncAdd"::: ) (Set (Var "A")) ")" ) ($#k1_funcsdom :::"."::: ) "(" (Set "(" (Set "(" ($#k3_cfuncdom :::"ComplexFuncExtMult"::: ) (Set (Var "A")) ")" ) ($#k2_funcsdom :::"."::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "a")) "," (Set (Var "f")) ($#k1_domain_1 :::"]"::: ) ) ")" ) "," (Set "(" (Set "(" ($#k3_cfuncdom :::"ComplexFuncExtMult"::: ) (Set (Var "A")) ")" ) ($#k2_funcsdom :::"."::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "b")) "," (Set (Var "g")) ($#k1_domain_1 :::"]"::: ) ) ")" ) ")" ))))))) ; theorem :: CFUNCDOM:21 (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set ($#k2_tarski :::"{"::: ) (Set (Var "x1")) "," (Set (Var "x2")) ($#k2_tarski :::"}"::: ) )) & (Bool (Set (Var "x1")) ($#r1_hidden :::"<>"::: ) (Set (Var "x2")))) "holds" (Bool "ex" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k9_funct_2 :::"Funcs"::: ) "(" (Set (Var "A")) "," (Set ($#k2_numbers :::"COMPLEX"::: ) ) ")" ) "st" (Bool "for" (Set (Var "h")) "being" ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k9_funct_2 :::"Funcs"::: ) "(" (Set (Var "A")) "," (Set ($#k2_numbers :::"COMPLEX"::: ) ) ")" ) (Bool "ex" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) "st" (Bool (Set (Var "h")) ($#r2_funct_2 :::"="::: ) (Set (Set "(" ($#k1_cfuncdom :::"ComplexFuncAdd"::: ) (Set (Var "A")) ")" ) ($#k1_funcsdom :::"."::: ) "(" (Set "(" (Set "(" ($#k3_cfuncdom :::"ComplexFuncExtMult"::: ) (Set (Var "A")) ")" ) ($#k2_funcsdom :::"."::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "a")) "," (Set (Var "f")) ($#k1_domain_1 :::"]"::: ) ) ")" ) "," (Set "(" (Set "(" ($#k3_cfuncdom :::"ComplexFuncExtMult"::: ) (Set (Var "A")) ")" ) ($#k2_funcsdom :::"."::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "b")) "," (Set (Var "g")) ($#k1_domain_1 :::"]"::: ) ) ")" ) ")" ))))))) ; theorem :: CFUNCDOM:22 (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set ($#k2_tarski :::"{"::: ) (Set (Var "x1")) "," (Set (Var "x2")) ($#k2_tarski :::"}"::: ) )) & (Bool (Set (Var "x1")) ($#r1_hidden :::"<>"::: ) (Set (Var "x2")))) "holds" (Bool "ex" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k9_funct_2 :::"Funcs"::: ) "(" (Set (Var "A")) "," (Set ($#k2_numbers :::"COMPLEX"::: ) ) ")" ) "st" (Bool "(" (Bool "(" "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) "st" (Bool (Bool (Set (Set "(" ($#k1_cfuncdom :::"ComplexFuncAdd"::: ) (Set (Var "A")) ")" ) ($#k1_funcsdom :::"."::: ) "(" (Set "(" (Set "(" ($#k3_cfuncdom :::"ComplexFuncExtMult"::: ) (Set (Var "A")) ")" ) ($#k2_funcsdom :::"."::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "a")) "," (Set (Var "f")) ($#k1_domain_1 :::"]"::: ) ) ")" ) "," (Set "(" (Set "(" ($#k3_cfuncdom :::"ComplexFuncExtMult"::: ) (Set (Var "A")) ")" ) ($#k2_funcsdom :::"."::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "b")) "," (Set (Var "g")) ($#k1_domain_1 :::"]"::: ) ) ")" ) ")" ) ($#r2_funct_2 :::"="::: ) (Set ($#k4_cfuncdom :::"ComplexFuncZero"::: ) (Set (Var "A"))))) "holds" (Bool "(" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "b")) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" ) ")" ) & (Bool "(" "for" (Set (Var "h")) "being" ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k9_funct_2 :::"Funcs"::: ) "(" (Set (Var "A")) "," (Set ($#k2_numbers :::"COMPLEX"::: ) ) ")" ) (Bool "ex" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) "st" (Bool (Set (Var "h")) ($#r2_funct_2 :::"="::: ) (Set (Set "(" ($#k1_cfuncdom :::"ComplexFuncAdd"::: ) (Set (Var "A")) ")" ) ($#k1_funcsdom :::"."::: ) "(" (Set "(" (Set "(" ($#k3_cfuncdom :::"ComplexFuncExtMult"::: ) (Set (Var "A")) ")" ) ($#k2_funcsdom :::"."::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "a")) "," (Set (Var "f")) ($#k1_domain_1 :::"]"::: ) ) ")" ) "," (Set "(" (Set "(" ($#k3_cfuncdom :::"ComplexFuncExtMult"::: ) (Set (Var "A")) ")" ) ($#k2_funcsdom :::"."::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "b")) "," (Set (Var "g")) ($#k1_domain_1 :::"]"::: ) ) ")" ) ")" ))) ")" ) ")" )))) ; definitionlet "A" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; func :::"ComplexVectSpace"::: "A" -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_clvect_1 :::"strict"::: ) ($#l1_clvect_1 :::"CLSStruct"::: ) equals :: CFUNCDOM:def 6 (Set ($#g1_clvect_1 :::"CLSStruct"::: ) "(#" (Set "(" ($#k9_funct_2 :::"Funcs"::: ) "(" "A" "," (Set ($#k2_numbers :::"COMPLEX"::: ) ) ")" ")" ) "," (Set "(" ($#k4_cfuncdom :::"ComplexFuncZero"::: ) "A" ")" ) "," (Set "(" ($#k1_cfuncdom :::"ComplexFuncAdd"::: ) "A" ")" ) "," (Set "(" ($#k3_cfuncdom :::"ComplexFuncExtMult"::: ) "A" ")" ) "#)" ); end; :: deftheorem defines :::"ComplexVectSpace"::: CFUNCDOM:def 6 : (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k6_cfuncdom :::"ComplexVectSpace"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set ($#g1_clvect_1 :::"CLSStruct"::: ) "(#" (Set "(" ($#k9_funct_2 :::"Funcs"::: ) "(" (Set (Var "A")) "," (Set ($#k2_numbers :::"COMPLEX"::: ) ) ")" ")" ) "," (Set "(" ($#k4_cfuncdom :::"ComplexFuncZero"::: ) (Set (Var "A")) ")" ) "," (Set "(" ($#k1_cfuncdom :::"ComplexFuncAdd"::: ) (Set (Var "A")) ")" ) "," (Set "(" ($#k3_cfuncdom :::"ComplexFuncExtMult"::: ) (Set (Var "A")) ")" ) "#)" ))); registrationlet "A" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k6_cfuncdom :::"ComplexVectSpace"::: ) "A") -> ($#~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"::: ) for ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_clvect_1 :::"strict"::: ) ($#l1_clvect_1 :::"CLSStruct"::: ) ; end; theorem :: CFUNCDOM:23 (Bool "ex" (Set (Var "V")) "being" ($#v1_clvect_1 :::"strict"::: ) ($#l1_clvect_1 :::"ComplexLinearSpace":::)(Bool "ex" (Set (Var "u")) "," (Set (Var "v")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) "st" (Bool "(" (Bool "(" "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) "st" (Bool (Bool (Set (Set "(" (Set (Var "a")) ($#k1_clvect_1 :::"*"::: ) (Set (Var "u")) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "b")) ($#k1_clvect_1 :::"*"::: ) (Set (Var "v")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "V"))))) "holds" (Bool "(" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "b")) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" ) ")" ) & (Bool "(" "for" (Set (Var "w")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) (Bool "ex" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) "st" (Bool (Set (Var "w")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "a")) ($#k1_clvect_1 :::"*"::: ) (Set (Var "u")) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "b")) ($#k1_clvect_1 :::"*"::: ) (Set (Var "v")) ")" )))) ")" ) ")" ))) ; definitionlet "A" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; func :::"CRing"::: "A" -> ($#l6_algstr_0 :::"doubleLoopStr"::: ) equals :: CFUNCDOM:def 7 (Set ($#g6_algstr_0 :::"doubleLoopStr"::: ) "(#" (Set "(" ($#k9_funct_2 :::"Funcs"::: ) "(" "A" "," (Set ($#k2_numbers :::"COMPLEX"::: ) ) ")" ")" ) "," (Set "(" ($#k1_cfuncdom :::"ComplexFuncAdd"::: ) "A" ")" ) "," (Set "(" ($#k2_cfuncdom :::"ComplexFuncMult"::: ) "A" ")" ) "," (Set "(" ($#k5_cfuncdom :::"ComplexFuncUnit"::: ) "A" ")" ) "," (Set "(" ($#k4_cfuncdom :::"ComplexFuncZero"::: ) "A" ")" ) "#)" ); end; :: deftheorem defines :::"CRing"::: CFUNCDOM:def 7 : (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k7_cfuncdom :::"CRing"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set ($#g6_algstr_0 :::"doubleLoopStr"::: ) "(#" (Set "(" ($#k9_funct_2 :::"Funcs"::: ) "(" (Set (Var "A")) "," (Set ($#k2_numbers :::"COMPLEX"::: ) ) ")" ")" ) "," (Set "(" ($#k1_cfuncdom :::"ComplexFuncAdd"::: ) (Set (Var "A")) ")" ) "," (Set "(" ($#k2_cfuncdom :::"ComplexFuncMult"::: ) (Set (Var "A")) ")" ) "," (Set "(" ($#k5_cfuncdom :::"ComplexFuncUnit"::: ) (Set (Var "A")) ")" ) "," (Set "(" ($#k4_cfuncdom :::"ComplexFuncZero"::: ) (Set (Var "A")) ")" ) "#)" ))); registrationlet "A" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k7_cfuncdom :::"CRing"::: ) "A") -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v36_algstr_0 :::"strict"::: ) ; end; registrationlet "A" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k7_cfuncdom :::"CRing"::: ) "A") -> ($#v1_group_1 :::"unital"::: ) ; end; theorem :: CFUNCDOM:24 (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k7_cfuncdom :::"CRing"::: ) (Set (Var "A")) ")" ) "holds" (Bool "(" (Bool (Set (Set (Var "x")) ($#k1_algstr_0 :::"+"::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "y")) ($#k1_algstr_0 :::"+"::: ) (Set (Var "x")))) & (Bool (Set (Set "(" (Set (Var "x")) ($#k1_algstr_0 :::"+"::: ) (Set (Var "y")) ")" ) ($#k1_algstr_0 :::"+"::: ) (Set (Var "z"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k1_algstr_0 :::"+"::: ) (Set "(" (Set (Var "y")) ($#k1_algstr_0 :::"+"::: ) (Set (Var "z")) ")" ))) & (Bool (Set (Set (Var "x")) ($#k1_algstr_0 :::"+"::: ) (Set "(" ($#k4_struct_0 :::"0."::: ) (Set "(" ($#k7_cfuncdom :::"CRing"::: ) (Set (Var "A")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "x"))) & (Bool (Set (Var "x")) "is" ($#v10_algstr_0 :::"right_complementable"::: ) ) & (Bool (Set (Set (Var "x")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "y")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "x")))) & (Bool (Set (Set "(" (Set (Var "x")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "y")) ")" ) ($#k6_algstr_0 :::"*"::: ) (Set (Var "z"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k6_algstr_0 :::"*"::: ) (Set "(" (Set (Var "y")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "z")) ")" ))) & (Bool (Set (Set (Var "x")) ($#k6_algstr_0 :::"*"::: ) (Set "(" ($#k5_struct_0 :::"1."::: ) (Set "(" ($#k7_cfuncdom :::"CRing"::: ) (Set (Var "A")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "x"))) & (Bool (Set (Set "(" ($#k5_struct_0 :::"1."::: ) (Set "(" ($#k7_cfuncdom :::"CRing"::: ) (Set (Var "A")) ")" ) ")" ) ($#k6_algstr_0 :::"*"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Var "x"))) & (Bool (Set (Set (Var "x")) ($#k6_algstr_0 :::"*"::: ) (Set "(" (Set (Var "y")) ($#k1_algstr_0 :::"+"::: ) (Set (Var "z")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "x")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "y")) ")" ) ($#k1_algstr_0 :::"+"::: ) (Set "(" (Set (Var "x")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "z")) ")" ))) & (Bool (Set (Set "(" (Set (Var "y")) ($#k1_algstr_0 :::"+"::: ) (Set (Var "z")) ")" ) ($#k6_algstr_0 :::"*"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "y")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "x")) ")" ) ($#k1_algstr_0 :::"+"::: ) (Set "(" (Set (Var "z")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "x")) ")" ))) ")" ))) ; theorem :: CFUNCDOM:25 (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k7_cfuncdom :::"CRing"::: ) (Set (Var "A"))) "is" ($#v5_group_1 :::"commutative"::: ) ($#l6_algstr_0 :::"Ring":::))) ; definitionattr "c1" is :::"strict"::: ; struct :::"ComplexAlgebraStr"::: -> ($#l6_algstr_0 :::"doubleLoopStr"::: ) "," ($#l1_clvect_1 :::"CLSStruct"::: ) ; aggr :::"ComplexAlgebraStr":::(# :::"carrier":::, :::"multF":::, :::"addF":::, :::"Mult":::, :::"OneF":::, :::"ZeroF"::: #) -> ($#l1_cfuncdom :::"ComplexAlgebraStr"::: ) ; end; registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) for ($#l1_cfuncdom :::"ComplexAlgebraStr"::: ) ; end; definitionlet "A" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; func :::"CAlgebra"::: "A" -> ($#v1_cfuncdom :::"strict"::: ) ($#l1_cfuncdom :::"ComplexAlgebraStr"::: ) equals :: CFUNCDOM:def 8 (Set ($#g1_cfuncdom :::"ComplexAlgebraStr"::: ) "(#" (Set "(" ($#k9_funct_2 :::"Funcs"::: ) "(" "A" "," (Set ($#k2_numbers :::"COMPLEX"::: ) ) ")" ")" ) "," (Set "(" ($#k2_cfuncdom :::"ComplexFuncMult"::: ) "A" ")" ) "," (Set "(" ($#k1_cfuncdom :::"ComplexFuncAdd"::: ) "A" ")" ) "," (Set "(" ($#k3_cfuncdom :::"ComplexFuncExtMult"::: ) "A" ")" ) "," (Set "(" ($#k5_cfuncdom :::"ComplexFuncUnit"::: ) "A" ")" ) "," (Set "(" ($#k4_cfuncdom :::"ComplexFuncZero"::: ) "A" ")" ) "#)" ); end; :: deftheorem defines :::"CAlgebra"::: CFUNCDOM:def 8 : (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k8_cfuncdom :::"CAlgebra"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set ($#g1_cfuncdom :::"ComplexAlgebraStr"::: ) "(#" (Set "(" ($#k9_funct_2 :::"Funcs"::: ) "(" (Set (Var "A")) "," (Set ($#k2_numbers :::"COMPLEX"::: ) ) ")" ")" ) "," (Set "(" ($#k2_cfuncdom :::"ComplexFuncMult"::: ) (Set (Var "A")) ")" ) "," (Set "(" ($#k1_cfuncdom :::"ComplexFuncAdd"::: ) (Set (Var "A")) ")" ) "," (Set "(" ($#k3_cfuncdom :::"ComplexFuncExtMult"::: ) (Set (Var "A")) ")" ) "," (Set "(" ($#k5_cfuncdom :::"ComplexFuncUnit"::: ) (Set (Var "A")) ")" ) "," (Set "(" ($#k4_cfuncdom :::"ComplexFuncZero"::: ) (Set (Var "A")) ")" ) "#)" ))); registrationlet "A" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k8_cfuncdom :::"CAlgebra"::: ) "A") -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_cfuncdom :::"strict"::: ) ; end; registrationlet "A" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k8_cfuncdom :::"CAlgebra"::: ) "A") -> ($#v1_group_1 :::"unital"::: ) ($#v1_cfuncdom :::"strict"::: ) ; end; theorem :: CFUNCDOM:26 (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k8_cfuncdom :::"CAlgebra"::: ) (Set (Var "A")) ")" ) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) "holds" (Bool "(" (Bool (Set (Set (Var "x")) ($#k1_algstr_0 :::"+"::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "y")) ($#k1_algstr_0 :::"+"::: ) (Set (Var "x")))) & (Bool (Set (Set "(" (Set (Var "x")) ($#k1_algstr_0 :::"+"::: ) (Set (Var "y")) ")" ) ($#k1_algstr_0 :::"+"::: ) (Set (Var "z"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k1_algstr_0 :::"+"::: ) (Set "(" (Set (Var "y")) ($#k1_algstr_0 :::"+"::: ) (Set (Var "z")) ")" ))) & (Bool (Set (Set (Var "x")) ($#k1_algstr_0 :::"+"::: ) (Set "(" ($#k4_struct_0 :::"0."::: ) (Set "(" ($#k8_cfuncdom :::"CAlgebra"::: ) (Set (Var "A")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "x"))) & (Bool (Set (Var "x")) "is" ($#v10_algstr_0 :::"right_complementable"::: ) ) & (Bool (Set (Set (Var "x")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "y")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "x")))) & (Bool (Set (Set "(" (Set (Var "x")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "y")) ")" ) ($#k6_algstr_0 :::"*"::: ) (Set (Var "z"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k6_algstr_0 :::"*"::: ) (Set "(" (Set (Var "y")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "z")) ")" ))) & (Bool (Set (Set (Var "x")) ($#k6_algstr_0 :::"*"::: ) (Set "(" ($#k5_struct_0 :::"1."::: ) (Set "(" ($#k8_cfuncdom :::"CAlgebra"::: ) (Set (Var "A")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "x"))) & (Bool (Set (Set (Var "x")) ($#k6_algstr_0 :::"*"::: ) (Set "(" (Set (Var "y")) ($#k1_algstr_0 :::"+"::: ) (Set (Var "z")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "x")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "y")) ")" ) ($#k1_algstr_0 :::"+"::: ) (Set "(" (Set (Var "x")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "z")) ")" ))) & (Bool (Set (Set (Var "a")) ($#k1_clvect_1 :::"*"::: ) (Set "(" (Set (Var "x")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "y")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "a")) ($#k1_clvect_1 :::"*"::: ) (Set (Var "x")) ")" ) ($#k6_algstr_0 :::"*"::: ) (Set (Var "y")))) & (Bool (Set (Set (Var "a")) ($#k1_clvect_1 :::"*"::: ) (Set "(" (Set (Var "x")) ($#k1_algstr_0 :::"+"::: ) (Set (Var "y")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "a")) ($#k1_clvect_1 :::"*"::: ) (Set (Var "x")) ")" ) ($#k1_algstr_0 :::"+"::: ) (Set "(" (Set (Var "a")) ($#k1_clvect_1 :::"*"::: ) (Set (Var "y")) ")" ))) & (Bool (Set (Set "(" (Set (Var "a")) ($#k8_complex1 :::"+"::: ) (Set (Var "b")) ")" ) ($#k1_clvect_1 :::"*"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "a")) ($#k1_clvect_1 :::"*"::: ) (Set (Var "x")) ")" ) ($#k1_algstr_0 :::"+"::: ) (Set "(" (Set (Var "b")) ($#k1_clvect_1 :::"*"::: ) (Set (Var "x")) ")" ))) & (Bool (Set (Set "(" (Set (Var "a")) ($#k9_complex1 :::"*"::: ) (Set (Var "b")) ")" ) ($#k1_clvect_1 :::"*"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k1_clvect_1 :::"*"::: ) (Set "(" (Set (Var "b")) ($#k1_clvect_1 :::"*"::: ) (Set (Var "x")) ")" ))) ")" )))) ; definitionlet "IT" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_cfuncdom :::"ComplexAlgebraStr"::: ) ; attr "IT" is :::"vector-associative"::: means :: CFUNCDOM:def 9 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" "IT" (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) "holds" (Bool (Set (Set (Var "a")) ($#k1_clvect_1 :::"*"::: ) (Set "(" (Set (Var "x")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "y")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "a")) ($#k1_clvect_1 :::"*"::: ) (Set (Var "x")) ")" ) ($#k6_algstr_0 :::"*"::: ) (Set (Var "y")))))); end; :: deftheorem defines :::"vector-associative"::: CFUNCDOM:def 9 : (Bool "for" (Set (Var "IT")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_cfuncdom :::"ComplexAlgebraStr"::: ) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v2_cfuncdom :::"vector-associative"::: ) ) "iff" (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "IT")) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) "holds" (Bool (Set (Set (Var "a")) ($#k1_clvect_1 :::"*"::: ) (Set "(" (Set (Var "x")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "y")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "a")) ($#k1_clvect_1 :::"*"::: ) (Set (Var "x")) ")" ) ($#k6_algstr_0 :::"*"::: ) (Set (Var "y")))))) ")" )); registrationlet "A" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k8_cfuncdom :::"CAlgebra"::: ) "A") -> ($#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"::: ) ($#v3_group_1 :::"associative"::: ) ($#v5_group_1 :::"commutative"::: ) ($#v1_vectsp_1 :::"right-distributive"::: ) ($#v3_vectsp_1 :::"right_unital"::: ) ($#v1_cfuncdom :::"strict"::: ) ($#v2_cfuncdom :::"vector-associative"::: ) ; end; 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"::: ) ($#v3_group_1 :::"associative"::: ) ($#v5_group_1 :::"commutative"::: ) ($#v1_vectsp_1 :::"right-distributive"::: ) ($#v3_vectsp_1 :::"right_unital"::: ) ($#v1_cfuncdom :::"strict"::: ) ($#v2_cfuncdom :::"vector-associative"::: ) for ($#l1_cfuncdom :::"ComplexAlgebraStr"::: ) ; end; definitionmode ComplexAlgebra 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"::: ) ($#v3_group_1 :::"associative"::: ) ($#v5_group_1 :::"commutative"::: ) ($#v1_vectsp_1 :::"right-distributive"::: ) ($#v3_vectsp_1 :::"right_unital"::: ) ($#v2_cfuncdom :::"vector-associative"::: ) ($#l1_cfuncdom :::"ComplexAlgebraStr"::: ) ; end; theorem :: CFUNCDOM:27 (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k8_cfuncdom :::"CAlgebra"::: ) (Set (Var "A"))) "is" ($#l1_cfuncdom :::"ComplexAlgebra":::))) ; theorem :: CFUNCDOM:28 (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k5_struct_0 :::"1."::: ) (Set "(" ($#k7_cfuncdom :::"CRing"::: ) (Set (Var "A")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k5_cfuncdom :::"ComplexFuncUnit"::: ) (Set (Var "A"))))) ; theorem :: CFUNCDOM:29 (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k5_struct_0 :::"1."::: ) (Set "(" ($#k8_cfuncdom :::"CAlgebra"::: ) (Set (Var "A")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k5_cfuncdom :::"ComplexFuncUnit"::: ) (Set (Var "A"))))) ;