:: CFUNCDOM semantic presentation

begin


definition
let A be non empty set ;
func ComplexFuncAdd A ->  BinOp of (Funcs (A,COMPLEX)) means :Def1: :: CFUNCDOM:def 1
 for f, g being Element of Funcs (A,COMPLEX) holds it . (f,g) = addcomplex .: (f,g);
existence
 ex b1 being BinOp of (Funcs (A,COMPLEX)) st
for f, g being Element of Funcs (A,COMPLEX) holds b1 . (f,g) = addcomplex .: (f,g)
proof
deffunc H1( Element of Funcs (A,COMPLEX), Element of Funcs (A,COMPLEX)) ->  Element of Funcs (A,COMPLEX) = addcomplex .: ($1,$2);
consider F being BinOp of (Funcs (A,COMPLEX)) such that
A1: for x, y being Element of Funcs (A,COMPLEX) holds F . (x,y) = H1(x,y) from BINOP_1:sch_4();
take  F ; ::_thesis: for f, g being Element of Funcs (A,COMPLEX) holds F . (f,g) = addcomplex .: (f,g)
let f, g be Element of Funcs (A,COMPLEX); ::_thesis: F . (f,g) = addcomplex .: (f,g)
thus  F . (f,g) = addcomplex .: (f,g) by A1; ::_thesis: verum
end;
uniqueness
 for b1, b2 being BinOp of (Funcs (A,COMPLEX)) st ( for f, g being Element of Funcs (A,COMPLEX) holds b1 . (f,g) = addcomplex .: (f,g) ) & ( for f, g being Element of Funcs (A,COMPLEX) holds b2 . (f,g) = addcomplex .: (f,g) ) holds
b1 = b2
proof
let it1, it2 be BinOp of (Funcs (A,COMPLEX)); ::_thesis: ( ( for f, g being Element of Funcs (A,COMPLEX) holds it1 . (f,g) = addcomplex .: (f,g) ) & ( for f, g being Element of Funcs (A,COMPLEX) holds it2 . (f,g) = addcomplex .: (f,g) ) implies it1 = it2 )
assume that
A2: for f, g being Element of Funcs (A,COMPLEX) holds it1 . (f,g) = addcomplex .: (f,g) and
A3: for f, g being Element of Funcs (A,COMPLEX) holds it2 . (f,g) = addcomplex .: (f,g) ; ::_thesis: it1 = it2
now__::_thesis:_for_f,_g_being_Element_of_Funcs_(A,COMPLEX)_holds_it1_._(f,g)_=_it2_._(f,g)
let f, g be Element of Funcs (A,COMPLEX); ::_thesis: it1 . (f,g) = it2 . (f,g)
thus it1 . (f,g) = addcomplex .: (f,g) by A2
.= it2 . (f,g) by A3 ; ::_thesis: verum
end;
hence  it1 = it2 by BINOP_1:2; ::_thesis: verum
end;
end;

:: deftheorem Def1 defines ComplexFuncAdd CFUNCDOM:def_1_:_
 for A being non empty set
for b2 being BinOp of (Funcs (A,COMPLEX)) holds
( b2 = ComplexFuncAdd A iff for f, g being Element of Funcs (A,COMPLEX) holds b2 . (f,g) = addcomplex .: (f,g) );

definition
let A be non empty set ;
func ComplexFuncMult A ->  BinOp of (Funcs (A,COMPLEX)) means :Def2: :: CFUNCDOM:def 2
 for f, g being Element of Funcs (A,COMPLEX) holds it . (f,g) = multcomplex .: (f,g);
existence
 ex b1 being BinOp of (Funcs (A,COMPLEX)) st
for f, g being Element of Funcs (A,COMPLEX) holds b1 . (f,g) = multcomplex .: (f,g)
proof
deffunc H1( Element of Funcs (A,COMPLEX), Element of Funcs (A,COMPLEX)) ->  Element of Funcs (A,COMPLEX) = multcomplex .: ($1,$2);
consider F being BinOp of (Funcs (A,COMPLEX)) such that
A1: for x, y being Element of Funcs (A,COMPLEX) holds F . (x,y) = H1(x,y) from BINOP_1:sch_4();
take  F ; ::_thesis: for f, g being Element of Funcs (A,COMPLEX) holds F . (f,g) = multcomplex .: (f,g)
let f, g be Element of Funcs (A,COMPLEX); ::_thesis: F . (f,g) = multcomplex .: (f,g)
thus  F . (f,g) = multcomplex .: (f,g) by A1; ::_thesis: verum
end;
uniqueness
 for b1, b2 being BinOp of (Funcs (A,COMPLEX)) st ( for f, g being Element of Funcs (A,COMPLEX) holds b1 . (f,g) = multcomplex .: (f,g) ) & ( for f, g being Element of Funcs (A,COMPLEX) holds b2 . (f,g) = multcomplex .: (f,g) ) holds
b1 = b2
proof
let it1, it2 be BinOp of (Funcs (A,COMPLEX)); ::_thesis: ( ( for f, g being Element of Funcs (A,COMPLEX) holds it1 . (f,g) = multcomplex .: (f,g) ) & ( for f, g being Element of Funcs (A,COMPLEX) holds it2 . (f,g) = multcomplex .: (f,g) ) implies it1 = it2 )
assume that
A2: for f, g being Element of Funcs (A,COMPLEX) holds it1 . (f,g) = multcomplex .: (f,g) and
A3: for f, g being Element of Funcs (A,COMPLEX) holds it2 . (f,g) = multcomplex .: (f,g) ; ::_thesis: it1 = it2
now__::_thesis:_for_f,_g_being_Element_of_Funcs_(A,COMPLEX)_holds_it1_._(f,g)_=_it2_._(f,g)
let f, g be Element of Funcs (A,COMPLEX); ::_thesis: it1 . (f,g) = it2 . (f,g)
thus it1 . (f,g) = multcomplex .: (f,g) by A2
.= it2 . (f,g) by A3 ; ::_thesis: verum
end;
hence  it1 = it2 by BINOP_1:2; ::_thesis: verum
end;
end;

:: deftheorem Def2 defines ComplexFuncMult CFUNCDOM:def_2_:_
 for A being non empty set
for b2 being BinOp of (Funcs (A,COMPLEX)) holds
( b2 = ComplexFuncMult A iff for f, g being Element of Funcs (A,COMPLEX) holds b2 . (f,g) = multcomplex .: (f,g) );

definition
let A be non empty set ;
func ComplexFuncExtMult A ->  Function of [:COMPLEX,(Funcs (A,COMPLEX)):],(Funcs (A,COMPLEX)) means :Def3: :: CFUNCDOM:def 3
 for z being Element of COMPLEX
for f being Element of Funcs (A,COMPLEX)
for x being Element of A holds (it . [z,f]) . x = z * (f . x);
existence
 ex b1 being Function of [:COMPLEX,(Funcs (A,COMPLEX)):],(Funcs (A,COMPLEX)) st
for z being Element of COMPLEX
for f being Element of Funcs (A,COMPLEX)
for x being Element of A holds (b1 . [z,f]) . x = z * (f . x)
proof
deffunc H1( Element of COMPLEX , Element of Funcs (A,COMPLEX)) ->  Element of Funcs (A,COMPLEX) = multcomplex [;] ($1,$2);
consider F being Function of [:COMPLEX,(Funcs (A,COMPLEX)):],(Funcs (A,COMPLEX)) such that
A1: for z being Element of COMPLEX
for f being Element of Funcs (A,COMPLEX) holds F . (z,f) = H1(z,f) from BINOP_1:sch_4();
take  F ; ::_thesis: for z being Element of COMPLEX
for f being Element of Funcs (A,COMPLEX)
for x being Element of A holds (F . [z,f]) . x = z * (f . x)
let z be Element of COMPLEX ; ::_thesis: for f being Element of Funcs (A,COMPLEX)
for x being Element of A holds (F . [z,f]) . x = z * (f . x)
let f be Element of Funcs (A,COMPLEX); ::_thesis: for x being Element of A holds (F . [z,f]) . x = z * (f . x)
let x be Element of A; ::_thesis: (F . [z,f]) . x = z * (f . x)
 F . (z,f) = multcomplex [;] (z,f) by A1;
hence (F . [z,f]) . x = multcomplex . (z,(f . x)) by FUNCOP_1:53
.= z * (f . x) by BINOP_2:def_5 ;
::_thesis: verum
end;
uniqueness
 for b1, b2 being Function of [:COMPLEX,(Funcs (A,COMPLEX)):],(Funcs (A,COMPLEX)) st ( for z being Element of COMPLEX
for f being Element of Funcs (A,COMPLEX)
for x being Element of A holds (b1 . [z,f]) . x = z * (f . x) ) & ( for z being Element of COMPLEX
for f being Element of Funcs (A,COMPLEX)
for x being Element of A holds (b2 . [z,f]) . x = z * (f . x) ) holds
b1 = b2
proof
let it1, it2 be Function of [:COMPLEX,(Funcs (A,COMPLEX)):],(Funcs (A,COMPLEX)); ::_thesis: ( ( for z being Element of COMPLEX
for f being Element of Funcs (A,COMPLEX)
for x being Element of A holds (it1 . [z,f]) . x = z * (f . x) ) & ( for z being Element of COMPLEX
for f being Element of Funcs (A,COMPLEX)
for x being Element of A holds (it2 . [z,f]) . x = z * (f . x) ) implies it1 = it2 )
assume that
A2: for z being Element of COMPLEX
for f being Element of Funcs (A,COMPLEX)
for x being Element of A holds (it1 . [z,f]) . x = z * (f . x) and
A3: for z being Element of COMPLEX
for f being Element of Funcs (A,COMPLEX)
for x being Element of A holds (it2 . [z,f]) . x = z * (f . x) ; ::_thesis: it1 = it2
now__::_thesis:_for_z_being_Element_of_COMPLEX_
for_f_being_Element_of_Funcs_(A,COMPLEX)_holds_it1_._(z,f)_=_it2_._(z,f)
let z be Element of COMPLEX ; ::_thesis: for f being Element of Funcs (A,COMPLEX) holds it1 . (z,f) = it2 . (z,f)
let f be Element of Funcs (A,COMPLEX); ::_thesis: it1 . (z,f) = it2 . (z,f)
now__::_thesis:_for_x_being_Element_of_A_holds_(it1_._[z,f])_._x_=_(it2_._[z,f])_._x
let x be Element of A; ::_thesis: (it1 . [z,f]) . x = (it2 . [z,f]) . x
thus (it1 . [z,f]) . x = z * (f . x) by A2
.= (it2 . [z,f]) . x by A3 ; ::_thesis: verum
end;
hence  it1 . (z,f) = it2 . (z,f) by FUNCT_2:63; ::_thesis: verum
end;
hence  it1 = it2 by BINOP_1:2; ::_thesis: verum
end;
end;

:: deftheorem Def3 defines ComplexFuncExtMult CFUNCDOM:def_3_:_
 for A being non empty set
for b2 being Function of [:COMPLEX,(Funcs (A,COMPLEX)):],(Funcs (A,COMPLEX)) holds
( b2 = ComplexFuncExtMult A iff for z being Element of COMPLEX
for f being Element of Funcs (A,COMPLEX)
for x being Element of A holds (b2 . [z,f]) . x = z * (f . x) );

definition
let A be non empty set ;
func ComplexFuncZero A ->  Element of Funcs (A,COMPLEX) equals :: CFUNCDOM:def 4
A --> 0;
coherence
 A --> 0 is Element of Funcs (A,COMPLEX)
proof
 A --> 0c is Function of A,COMPLEX ;
hence  A --> 0 is Element of Funcs (A,COMPLEX) by FUNCT_2:8; ::_thesis: verum
end;
end;

:: deftheorem  defines ComplexFuncZero CFUNCDOM:def_4_:_
 for A being non empty set holds ComplexFuncZero A = A --> 0;

definition
let A be non empty set ;
func ComplexFuncUnit A ->  Element of Funcs (A,COMPLEX) equals :: CFUNCDOM:def 5
A --> 1r;
coherence
 A --> 1r is Element of Funcs (A,COMPLEX) by FUNCT_2:8;
end;

:: deftheorem  defines ComplexFuncUnit CFUNCDOM:def_5_:_
 for A being non empty set holds ComplexFuncUnit A = A --> 1r;

Lm1:  for A, B being non empty set
for x being Element of A
for f being Function of A,B holds x in dom f
proof
let A, B be non empty set ; ::_thesis: for x being Element of A
for f being Function of A,B holds x in dom f
let x be Element of A; ::_thesis: for f being Function of A,B holds x in dom f
let f be Function of A,B; ::_thesis: x in dom f
 x in A ;
hence  x in dom f by FUNCT_2:def_1; ::_thesis: verum
end;

theorem Th1: :: CFUNCDOM:1
for A being non empty set
for h, f, g being Element of Funcs (A,COMPLEX) holds
( h = (ComplexFuncAdd A) . (f,g) iff for x being Element of A holds h . x = (f . x) + (g . x) )
proof
let A be non empty set ; ::_thesis: for h, f, g being Element of Funcs (A,COMPLEX) holds
( h = (ComplexFuncAdd A) . (f,g) iff for x being Element of A holds h . x = (f . x) + (g . x) )
let h, f, g be Element of Funcs (A,COMPLEX); ::_thesis: ( h = (ComplexFuncAdd A) . (f,g) iff for x being Element of A holds h . x = (f . x) + (g . x) )
A1: now__::_thesis:_(_(_for_x_being_Element_of_A_holds_h_._x_=_(f_._x)_+_(g_._x)_)_implies_h_=_(ComplexFuncAdd_A)_._(f,g)_)
assume A2: for x being Element of A holds h . x = (f . x) + (g . x) ; ::_thesis: h = (ComplexFuncAdd A) . (f,g)
now__::_thesis:_for_x_being_Element_of_A_holds_((ComplexFuncAdd_A)_._(f,g))_._x_=_h_._x
let x be Element of A; ::_thesis: ((ComplexFuncAdd A) . (f,g)) . x = h . x
A3: x in dom (addcomplex .: (f,g)) by Lm1;
thus ((ComplexFuncAdd A) . (f,g)) . x = (addcomplex .: (f,g)) . x by Def1
.= addcomplex . ((f . x),(g . x)) by A3, FUNCOP_1:22
.= (f . x) + (g . x) by BINOP_2:def_3
.= h . x by A2 ; ::_thesis: verum
end;
hence  h = (ComplexFuncAdd A) . (f,g) by FUNCT_2:63; ::_thesis: verum
end;
now__::_thesis:_(_h_=_(ComplexFuncAdd_A)_._(f,g)_implies_for_x_being_Element_of_A_holds_h_._x_=_(f_._x)_+_(g_._x)_)
assume A4: h = (ComplexFuncAdd A) . (f,g) ; ::_thesis: for x being Element of A holds h . x = (f . x) + (g . x)
let x be Element of A; ::_thesis: h . x = (f . x) + (g . x)
A5: x in dom (addcomplex .: (f,g)) by Lm1;
thus h . x = (addcomplex .: (f,g)) . x by A4, Def1
.= addcomplex . ((f . x),(g . x)) by A5, FUNCOP_1:22
.= (f . x) + (g . x) by BINOP_2:def_3 ; ::_thesis: verum
end;
hence  ( h = (ComplexFuncAdd A) . (f,g) iff for x being Element of A holds h . x = (f . x) + (g . x) ) by A1; ::_thesis: verum
end;

theorem Th2: :: CFUNCDOM:2
for A being non empty set
for h, f, g being Element of Funcs (A,COMPLEX) holds
( h = (ComplexFuncMult A) . (f,g) iff for x being Element of A holds h . x = (f . x) * (g . x) )
proof
let A be non empty set ; ::_thesis: for h, f, g being Element of Funcs (A,COMPLEX) holds
( h = (ComplexFuncMult A) . (f,g) iff for x being Element of A holds h . x = (f . x) * (g . x) )
let h, f, g be Element of Funcs (A,COMPLEX); ::_thesis: ( h = (ComplexFuncMult A) . (f,g) iff for x being Element of A holds h . x = (f . x) * (g . x) )
A1: now__::_thesis:_(_(_for_x_being_Element_of_A_holds_h_._x_=_(f_._x)_*_(g_._x)_)_implies_h_=_(ComplexFuncMult_A)_._(f,g)_)
assume A2: for x being Element of A holds h . x = (f . x) * (g . x) ; ::_thesis: h = (ComplexFuncMult A) . (f,g)
now__::_thesis:_for_x_being_Element_of_A_holds_((ComplexFuncMult_A)_._(f,g))_._x_=_h_._x
let x be Element of A; ::_thesis: ((ComplexFuncMult A) . (f,g)) . x = h . x
A3: x in dom (multcomplex .: (f,g)) by Lm1;
thus ((ComplexFuncMult A) . (f,g)) . x = (multcomplex .: (f,g)) . x by Def2
.= multcomplex . ((f . x),(g . x)) by A3, FUNCOP_1:22
.= (f . x) * (g . x) by BINOP_2:def_5
.= h . x by A2 ; ::_thesis: verum
end;
hence  h = (ComplexFuncMult A) . (f,g) by FUNCT_2:63; ::_thesis: verum
end;
now__::_thesis:_(_h_=_(ComplexFuncMult_A)_._(f,g)_implies_for_x_being_Element_of_A_holds_h_._x_=_(f_._x)_*_(g_._x)_)
assume A4: h = (ComplexFuncMult A) . (f,g) ; ::_thesis: for x being Element of A holds h . x = (f . x) * (g . x)
let x be Element of A; ::_thesis: h . x = (f . x) * (g . x)
A5: x in dom (multcomplex .: (f,g)) by Lm1;
thus h . x = (multcomplex .: (f,g)) . x by A4, Def2
.= multcomplex . ((f . x),(g . x)) by A5, FUNCOP_1:22
.= (f . x) * (g . x) by BINOP_2:def_5 ; ::_thesis: verum
end;
hence  ( h = (ComplexFuncMult A) . (f,g) iff for x being Element of A holds h . x = (f . x) * (g . x) ) by A1; ::_thesis: verum
end;

theorem :: CFUNCDOM:3
for A being non empty set holds ComplexFuncZero A <> ComplexFuncUnit A
proof
let A be non empty set ; ::_thesis: ComplexFuncZero A <> ComplexFuncUnit A
set a = the Element of A;
 (ComplexFuncZero A) . the Element of A = 0c by FUNCOP_1:7;
hence  ComplexFuncZero A <> ComplexFuncUnit A by COMPLEX1:def_4, FUNCOP_1:7; ::_thesis: verum
end;


theorem Th4: :: CFUNCDOM:4
for A being non empty set
for h, f being Element of Funcs (A,COMPLEX)
for a being Element of COMPLEX holds
( h = (ComplexFuncExtMult A) . [a,f] iff for x being Element of A holds h . x = a * (f . x) )
proof
let A be non empty set ; ::_thesis: for h, f being Element of Funcs (A,COMPLEX)
for a being Element of COMPLEX holds
( h = (ComplexFuncExtMult A) . [a,f] iff for x being Element of A holds h . x = a * (f . x) )
let h, f be Element of Funcs (A,COMPLEX); ::_thesis: for a being Element of COMPLEX holds
( h = (ComplexFuncExtMult A) . [a,f] iff for x being Element of A holds h . x = a * (f . x) )
let a be Element of COMPLEX ; ::_thesis: ( h = (ComplexFuncExtMult A) . [a,f] iff for x being Element of A holds h . x = a * (f . x) )
thus  ( h = (ComplexFuncExtMult A) . [a,f] implies for x being Element of A holds h . x = a * (f . x) ) by Def3; ::_thesis: ( ( for x being Element of A holds h . x = a * (f . x) ) implies h = (ComplexFuncExtMult A) . [a,f] )
now__::_thesis:_(_(_for_x_being_Element_of_A_holds_h_._x_=_a_*_(f_._x)_)_implies_h_=_(ComplexFuncExtMult_A)_._[a,f]_)
assume A1: for x being Element of A holds h . x = a * (f . x) ; ::_thesis: h = (ComplexFuncExtMult A) . [a,f]
 for x being Element of A holds h . x = ((ComplexFuncExtMult A) . [a,f]) . x
proof
let x be Element of A; ::_thesis: h . x = ((ComplexFuncExtMult A) . [a,f]) . x
thus h . x = a * (f . x) by A1
.= ((ComplexFuncExtMult A) . [a,f]) . x by Def3 ; ::_thesis: verum
end;
hence  h = (ComplexFuncExtMult A) . [a,f] by FUNCT_2:63; ::_thesis: verum
end;
hence  ( ( for x being Element of A holds h . x = a * (f . x) ) implies h = (ComplexFuncExtMult A) . [a,f] ) ; ::_thesis: verum
end;

theorem Th5: :: CFUNCDOM:5
for A being non empty set
for f, g being Element of Funcs (A,COMPLEX) holds (ComplexFuncAdd A) . (f,g) = (ComplexFuncAdd A) . (g,f)
proof
let A be non empty set ; ::_thesis: for f, g being Element of Funcs (A,COMPLEX) holds (ComplexFuncAdd A) . (f,g) = (ComplexFuncAdd A) . (g,f)
let f, g be Element of Funcs (A,COMPLEX); ::_thesis: (ComplexFuncAdd A) . (f,g) = (ComplexFuncAdd A) . (g,f)
now__::_thesis:_for_x_being_Element_of_A_holds_((ComplexFuncAdd_A)_._(f,g))_._x_=_((ComplexFuncAdd_A)_._(g,f))_._x
let x be Element of A; ::_thesis: ((ComplexFuncAdd A) . (f,g)) . x = ((ComplexFuncAdd A) . (g,f)) . x
thus ((ComplexFuncAdd A) . (f,g)) . x = (g . x) + (f . x) by Th1
.= ((ComplexFuncAdd A) . (g,f)) . x by Th1 ; ::_thesis: verum
end;
hence  (ComplexFuncAdd A) . (f,g) = (ComplexFuncAdd A) . (g,f) by FUNCT_2:63; ::_thesis: verum
end;

theorem Th6: :: CFUNCDOM:6
for A being non empty set
for f, g, h being Element of Funcs (A,COMPLEX) holds (ComplexFuncAdd A) . (f,((ComplexFuncAdd A) . (g,h))) = (ComplexFuncAdd A) . (((ComplexFuncAdd A) . (f,g)),h)
proof
let A be non empty set ; ::_thesis: for f, g, h being Element of Funcs (A,COMPLEX) holds (ComplexFuncAdd A) . (f,((ComplexFuncAdd A) . (g,h))) = (ComplexFuncAdd A) . (((ComplexFuncAdd A) . (f,g)),h)
let f, g, h be Element of Funcs (A,COMPLEX); ::_thesis: (ComplexFuncAdd A) . (f,((ComplexFuncAdd A) . (g,h))) = (ComplexFuncAdd A) . (((ComplexFuncAdd A) . (f,g)),h)
now__::_thesis:_for_x_being_Element_of_A_holds_((ComplexFuncAdd_A)_._(f,((ComplexFuncAdd_A)_._(g,h))))_._x_=_((ComplexFuncAdd_A)_._(((ComplexFuncAdd_A)_._(f,g)),h))_._x
let x be Element of A; ::_thesis: ((ComplexFuncAdd A) . (f,((ComplexFuncAdd A) . (g,h)))) . x = ((ComplexFuncAdd A) . (((ComplexFuncAdd A) . (f,g)),h)) . x
thus ((ComplexFuncAdd A) . (f,((ComplexFuncAdd A) . (g,h)))) . x = (f . x) + (((ComplexFuncAdd A) . (g,h)) . x) by Th1
.= (f . x) + ((g . x) + (h . x)) by Th1
.= ((f . x) + (g . x)) + (h . x)
.= (((ComplexFuncAdd A) . (f,g)) . x) + (h . x) by Th1
.= ((ComplexFuncAdd A) . (((ComplexFuncAdd A) . (f,g)),h)) . x by Th1 ; ::_thesis: verum
end;
hence  (ComplexFuncAdd A) . (f,((ComplexFuncAdd A) . (g,h))) = (ComplexFuncAdd A) . (((ComplexFuncAdd A) . (f,g)),h) by FUNCT_2:63; ::_thesis: verum
end;

theorem Th7: :: CFUNCDOM:7
for A being non empty set
for f, g being Element of Funcs (A,COMPLEX) holds (ComplexFuncMult A) . (f,g) = (ComplexFuncMult A) . (g,f)
proof
let A be non empty set ; ::_thesis: for f, g being Element of Funcs (A,COMPLEX) holds (ComplexFuncMult A) . (f,g) = (ComplexFuncMult A) . (g,f)
let f, g be Element of Funcs (A,COMPLEX); ::_thesis: (ComplexFuncMult A) . (f,g) = (ComplexFuncMult A) . (g,f)
now__::_thesis:_for_x_being_Element_of_A_holds_((ComplexFuncMult_A)_._(f,g))_._x_=_((ComplexFuncMult_A)_._(g,f))_._x
let x be Element of A; ::_thesis: ((ComplexFuncMult A) . (f,g)) . x = ((ComplexFuncMult A) . (g,f)) . x
thus ((ComplexFuncMult A) . (f,g)) . x = (g . x) * (f . x) by Th2
.= ((ComplexFuncMult A) . (g,f)) . x by Th2 ; ::_thesis: verum
end;
hence  (ComplexFuncMult A) . (f,g) = (ComplexFuncMult A) . (g,f) by FUNCT_2:63; ::_thesis: verum
end;

theorem Th8: :: CFUNCDOM:8
for A being non empty set
for f, g, h being Element of Funcs (A,COMPLEX) holds (ComplexFuncMult A) . (f,((ComplexFuncMult A) . (g,h))) = (ComplexFuncMult A) . (((ComplexFuncMult A) . (f,g)),h)
proof
let A be non empty set ; ::_thesis: for f, g, h being Element of Funcs (A,COMPLEX) holds (ComplexFuncMult A) . (f,((ComplexFuncMult A) . (g,h))) = (ComplexFuncMult A) . (((ComplexFuncMult A) . (f,g)),h)
let f, g, h be Element of Funcs (A,COMPLEX); ::_thesis: (ComplexFuncMult A) . (f,((ComplexFuncMult A) . (g,h))) = (ComplexFuncMult A) . (((ComplexFuncMult A) . (f,g)),h)
now__::_thesis:_for_x_being_Element_of_A_holds_((ComplexFuncMult_A)_._(f,((ComplexFuncMult_A)_._(g,h))))_._x_=_((ComplexFuncMult_A)_._(((ComplexFuncMult_A)_._(f,g)),h))_._x
let x be Element of A; ::_thesis: ((ComplexFuncMult A) . (f,((ComplexFuncMult A) . (g,h)))) . x = ((ComplexFuncMult A) . (((ComplexFuncMult A) . (f,g)),h)) . x
thus ((ComplexFuncMult A) . (f,((ComplexFuncMult A) . (g,h)))) . x = (f . x) * (((ComplexFuncMult A) . (g,h)) . x) by Th2
.= (f . x) * ((g . x) * (h . x)) by Th2
.= ((f . x) * (g . x)) * (h . x)
.= (((ComplexFuncMult A) . (f,g)) . x) * (h . x) by Th2
.= ((ComplexFuncMult A) . (((ComplexFuncMult A) . (f,g)),h)) . x by Th2 ; ::_thesis: verum
end;
hence  (ComplexFuncMult A) . (f,((ComplexFuncMult A) . (g,h))) = (ComplexFuncMult A) . (((ComplexFuncMult A) . (f,g)),h) by FUNCT_2:63; ::_thesis: verum
end;

theorem Th9: :: CFUNCDOM:9
for A being non empty set
for f being Element of Funcs (A,COMPLEX) holds (ComplexFuncMult A) . ((ComplexFuncUnit A),f) = f
proof
let A be non empty set ; ::_thesis: for f being Element of Funcs (A,COMPLEX) holds (ComplexFuncMult A) . ((ComplexFuncUnit A),f) = f
let f be Element of Funcs (A,COMPLEX); ::_thesis: (ComplexFuncMult A) . ((ComplexFuncUnit A),f) = f
now__::_thesis:_for_x_being_Element_of_A_holds_((ComplexFuncMult_A)_._((ComplexFuncUnit_A),f))_._x_=_f_._x
let x be Element of A; ::_thesis: ((ComplexFuncMult A) . ((ComplexFuncUnit A),f)) . x = f . x
thus ((ComplexFuncMult A) . ((ComplexFuncUnit A),f)) . x = ((ComplexFuncUnit A) . x) * (f . x) by Th2
.= 1r * (f . x) by FUNCOP_1:7
.= f . x by COMPLEX1:def_4 ; ::_thesis: verum
end;
hence  (ComplexFuncMult A) . ((ComplexFuncUnit A),f) = f by FUNCT_2:63; ::_thesis: verum
end;

theorem Th10: :: CFUNCDOM:10
for A being non empty set
for f being Element of Funcs (A,COMPLEX) holds (ComplexFuncAdd A) . ((ComplexFuncZero A),f) = f
proof
let A be non empty set ; ::_thesis: for f being Element of Funcs (A,COMPLEX) holds (ComplexFuncAdd A) . ((ComplexFuncZero A),f) = f
let f be Element of Funcs (A,COMPLEX); ::_thesis: (ComplexFuncAdd A) . ((ComplexFuncZero A),f) = f
now__::_thesis:_for_x_being_Element_of_A_holds_((ComplexFuncAdd_A)_._((ComplexFuncZero_A),f))_._x_=_f_._x
let x be Element of A; ::_thesis: ((ComplexFuncAdd A) . ((ComplexFuncZero A),f)) . x = f . x
thus ((ComplexFuncAdd A) . ((ComplexFuncZero A),f)) . x = ((ComplexFuncZero A) . x) + (f . x) by Th1
.= 0c + (f . x) by FUNCOP_1:7
.= f . x ; ::_thesis: verum
end;
hence  (ComplexFuncAdd A) . ((ComplexFuncZero A),f) = f by FUNCT_2:63; ::_thesis: verum
end;

theorem Th11: :: CFUNCDOM:11
for A being non empty set
for f being Element of Funcs (A,COMPLEX) holds (ComplexFuncAdd A) . (f,((ComplexFuncExtMult A) . [(- 1r),f])) = ComplexFuncZero A
proof
let A be non empty set ; ::_thesis: for f being Element of Funcs (A,COMPLEX) holds (ComplexFuncAdd A) . (f,((ComplexFuncExtMult A) . [(- 1r),f])) = ComplexFuncZero A
let f be Element of Funcs (A,COMPLEX); ::_thesis: (ComplexFuncAdd A) . (f,((ComplexFuncExtMult A) . [(- 1r),f])) = ComplexFuncZero A
now__::_thesis:_for_x_being_Element_of_A_holds_((ComplexFuncAdd_A)_._(f,((ComplexFuncExtMult_A)_._[(-_1r),f])))_._x_=_(ComplexFuncZero_A)_._x
let x be Element of A; ::_thesis: ((ComplexFuncAdd A) . (f,((ComplexFuncExtMult A) . [(- 1r),f]))) . x = (ComplexFuncZero A) . x
set y = f . x;
thus ((ComplexFuncAdd A) . (f,((ComplexFuncExtMult A) . [(- 1r),f]))) . x = (f . x) + (((ComplexFuncExtMult A) . [(- 1r),f]) . x) by Th1
.= (f . x) + ((- 1r) * (f . x)) by Th4
.= (ComplexFuncZero A) . x by COMPLEX1:def_4, FUNCOP_1:7 ; ::_thesis: verum
end;
hence  (ComplexFuncAdd A) . (f,((ComplexFuncExtMult A) . [(- 1r),f])) = ComplexFuncZero A by FUNCT_2:63; ::_thesis: verum
end;

theorem Th12: :: CFUNCDOM:12
for A being non empty set
for f being Element of Funcs (A,COMPLEX) holds (ComplexFuncExtMult A) . [1r,f] = f
proof
let A be non empty set ; ::_thesis: for f being Element of Funcs (A,COMPLEX) holds (ComplexFuncExtMult A) . [1r,f] = f
let f be Element of Funcs (A,COMPLEX); ::_thesis: (ComplexFuncExtMult A) . [1r,f] = f
now__::_thesis:_for_x_being_Element_of_A_holds_((ComplexFuncExtMult_A)_._[1r,f])_._x_=_f_._x
let x be Element of A; ::_thesis: ((ComplexFuncExtMult A) . [1r,f]) . x = f . x
thus ((ComplexFuncExtMult A) . [1r,f]) . x = 1r * (f . x) by Th4
.= f . x by COMPLEX1:def_4 ; ::_thesis: verum
end;
hence  (ComplexFuncExtMult A) . [1r,f] = f by FUNCT_2:63; ::_thesis: verum
end;

theorem Th13: :: CFUNCDOM:13
for A being non empty set
for f being Element of Funcs (A,COMPLEX)
for a, b being Complex holds (ComplexFuncExtMult A) . [a,((ComplexFuncExtMult A) . [b,f])] = (ComplexFuncExtMult A) . [(a * b),f]
proof
let A be non empty set ; ::_thesis: for f being Element of Funcs (A,COMPLEX)
for a, b being Complex holds (ComplexFuncExtMult A) . [a,((ComplexFuncExtMult A) . [b,f])] = (ComplexFuncExtMult A) . [(a * b),f]
let f be Element of Funcs (A,COMPLEX); ::_thesis: for a, b being Complex holds (ComplexFuncExtMult A) . [a,((ComplexFuncExtMult A) . [b,f])] = (ComplexFuncExtMult A) . [(a * b),f]
let a, b be Complex; ::_thesis: (ComplexFuncExtMult A) . [a,((ComplexFuncExtMult A) . [b,f])] = (ComplexFuncExtMult A) . [(a * b),f]
reconsider a = a, b = b as Element of COMPLEX by XCMPLX_0:def_2;
now__::_thesis:_for_x_being_Element_of_A_holds_((ComplexFuncExtMult_A)_._[a,((ComplexFuncExtMult_A)_._[b,f])])_._x_=_((ComplexFuncExtMult_A)_._[(a_*_b),f])_._x
let x be Element of A; ::_thesis: ((ComplexFuncExtMult A) . [a,((ComplexFuncExtMult A) . [b,f])]) . x = ((ComplexFuncExtMult A) . [(a * b),f]) . x
thus ((ComplexFuncExtMult A) . [a,((ComplexFuncExtMult A) . [b,f])]) . x = a * (((ComplexFuncExtMult A) . [b,f]) . x) by Th4
.= a * (b * (f . x)) by Th4
.= (a * b) * (f . x)
.= ((ComplexFuncExtMult A) . [(a * b),f]) . x by Th4 ; ::_thesis: verum
end;
hence  (ComplexFuncExtMult A) . [a,((ComplexFuncExtMult A) . [b,f])] = (ComplexFuncExtMult A) . [(a * b),f] by FUNCT_2:63; ::_thesis: verum
end;

theorem Th14: :: CFUNCDOM:14
for A being non empty set
for f being Element of Funcs (A,COMPLEX)
for a, b being Complex holds (ComplexFuncAdd A) . (((ComplexFuncExtMult A) . [a,f]),((ComplexFuncExtMult A) . [b,f])) = (ComplexFuncExtMult A) . [(a + b),f]
proof
let A be non empty set ; ::_thesis: for f being Element of Funcs (A,COMPLEX)
for a, b being Complex holds (ComplexFuncAdd A) . (((ComplexFuncExtMult A) . [a,f]),((ComplexFuncExtMult A) . [b,f])) = (ComplexFuncExtMult A) . [(a + b),f]
let f be Element of Funcs (A,COMPLEX); ::_thesis: for a, b being Complex holds (ComplexFuncAdd A) . (((ComplexFuncExtMult A) . [a,f]),((ComplexFuncExtMult A) . [b,f])) = (ComplexFuncExtMult A) . [(a + b),f]
let a, b be Complex; ::_thesis: (ComplexFuncAdd A) . (((ComplexFuncExtMult A) . [a,f]),((ComplexFuncExtMult A) . [b,f])) = (ComplexFuncExtMult A) . [(a + b),f]
reconsider a = a, b = b as Element of COMPLEX by XCMPLX_0:def_2;
now__::_thesis:_for_x_being_Element_of_A_holds_((ComplexFuncAdd_A)_._(((ComplexFuncExtMult_A)_._[a,f]),((ComplexFuncExtMult_A)_._[b,f])))_._x_=_((ComplexFuncExtMult_A)_._[(a_+_b),f])_._x
let x be Element of A; ::_thesis: ((ComplexFuncAdd A) . (((ComplexFuncExtMult A) . [a,f]),((ComplexFuncExtMult A) . [b,f]))) . x = ((ComplexFuncExtMult A) . [(a + b),f]) . x
thus ((ComplexFuncAdd A) . (((ComplexFuncExtMult A) . [a,f]),((ComplexFuncExtMult A) . [b,f]))) . x = (((ComplexFuncExtMult A) . [a,f]) . x) + (((ComplexFuncExtMult A) . [b,f]) . x) by Th1
.= (a * (f . x)) + (((ComplexFuncExtMult A) . [b,f]) . x) by Th4
.= (a * (f . x)) + (b * (f . x)) by Th4
.= (a + b) * (f . x)
.= ((ComplexFuncExtMult A) . [(a + b),f]) . x by Th4 ; ::_thesis: verum
end;
hence  (ComplexFuncAdd A) . (((ComplexFuncExtMult A) . [a,f]),((ComplexFuncExtMult A) . [b,f])) = (ComplexFuncExtMult A) . [(a + b),f] by FUNCT_2:63; ::_thesis: verum
end;

Lm2:  for A being non empty set
for f, g being Element of Funcs (A,COMPLEX)
for a being Complex holds (ComplexFuncAdd A) . (((ComplexFuncExtMult A) . [a,f]),((ComplexFuncExtMult A) . [a,g])) = (ComplexFuncExtMult A) . [a,((ComplexFuncAdd A) . (f,g))]
proof
let A be non empty set ; ::_thesis: for f, g being Element of Funcs (A,COMPLEX)
for a being Complex holds (ComplexFuncAdd A) . (((ComplexFuncExtMult A) . [a,f]),((ComplexFuncExtMult A) . [a,g])) = (ComplexFuncExtMult A) . [a,((ComplexFuncAdd A) . (f,g))]
let f, g be Element of Funcs (A,COMPLEX); ::_thesis: for a being Complex holds (ComplexFuncAdd A) . (((ComplexFuncExtMult A) . [a,f]),((ComplexFuncExtMult A) . [a,g])) = (ComplexFuncExtMult A) . [a,((ComplexFuncAdd A) . (f,g))]
let a be Complex; ::_thesis: (ComplexFuncAdd A) . (((ComplexFuncExtMult A) . [a,f]),((ComplexFuncExtMult A) . [a,g])) = (ComplexFuncExtMult A) . [a,((ComplexFuncAdd A) . (f,g))]
reconsider a = a as Element of COMPLEX by XCMPLX_0:def_2;
now__::_thesis:_for_x_being_Element_of_A_holds_((ComplexFuncAdd_A)_._(((ComplexFuncExtMult_A)_._[a,f]),((ComplexFuncExtMult_A)_._[a,g])))_._x_=_((ComplexFuncExtMult_A)_._[a,((ComplexFuncAdd_A)_._(f,g))])_._x
let x be Element of A; ::_thesis: ((ComplexFuncAdd A) . (((ComplexFuncExtMult A) . [a,f]),((ComplexFuncExtMult A) . [a,g]))) . x = ((ComplexFuncExtMult A) . [a,((ComplexFuncAdd A) . (f,g))]) . x
thus ((ComplexFuncAdd A) . (((ComplexFuncExtMult A) . [a,f]),((ComplexFuncExtMult A) . [a,g]))) . x = (((ComplexFuncExtMult A) . [a,f]) . x) + (((ComplexFuncExtMult A) . [a,g]) . x) by Th1
.= (a * (f . x)) + (((ComplexFuncExtMult A) . [a,g]) . x) by Th4
.= (a * (f . x)) + (a * (g . x)) by Th4
.= a * ((f . x) + (g . x))
.= a * (((ComplexFuncAdd A) . (f,g)) . x) by Th1
.= ((ComplexFuncExtMult A) . [a,((ComplexFuncAdd A) . (f,g))]) . x by Th4 ; ::_thesis: verum
end;
hence  (ComplexFuncAdd A) . (((ComplexFuncExtMult A) . [a,f]),((ComplexFuncExtMult A) . [a,g])) = (ComplexFuncExtMult A) . [a,((ComplexFuncAdd A) . (f,g))] by FUNCT_2:63; ::_thesis: verum
end;

theorem Th15: :: CFUNCDOM:15
for A being non empty set
for f, g, h being Element of Funcs (A,COMPLEX) holds (ComplexFuncMult A) . (f,((ComplexFuncAdd A) . (g,h))) = (ComplexFuncAdd A) . (((ComplexFuncMult A) . (f,g)),((ComplexFuncMult A) . (f,h)))
proof
let A be non empty set ; ::_thesis: for f, g, h being Element of Funcs (A,COMPLEX) holds (ComplexFuncMult A) . (f,((ComplexFuncAdd A) . (g,h))) = (ComplexFuncAdd A) . (((ComplexFuncMult A) . (f,g)),((ComplexFuncMult A) . (f,h)))
let f, g, h be Element of Funcs (A,COMPLEX); ::_thesis: (ComplexFuncMult A) . (f,((ComplexFuncAdd A) . (g,h))) = (ComplexFuncAdd A) . (((ComplexFuncMult A) . (f,g)),((ComplexFuncMult A) . (f,h)))
now__::_thesis:_for_x_being_Element_of_A_holds_((ComplexFuncMult_A)_._(f,((ComplexFuncAdd_A)_._(g,h))))_._x_=_((ComplexFuncAdd_A)_._(((ComplexFuncMult_A)_._(f,g)),((ComplexFuncMult_A)_._(f,h))))_._x
let x be Element of A; ::_thesis: ((ComplexFuncMult A) . (f,((ComplexFuncAdd A) . (g,h)))) . x = ((ComplexFuncAdd A) . (((ComplexFuncMult A) . (f,g)),((ComplexFuncMult A) . (f,h)))) . x
thus ((ComplexFuncMult A) . (f,((ComplexFuncAdd A) . (g,h)))) . x = (f . x) * (((ComplexFuncAdd A) . (g,h)) . x) by Th2
.= (f . x) * ((g . x) + (h . x)) by Th1
.= ((f . x) * (g . x)) + ((f . x) * (h . x))
.= (((ComplexFuncMult A) . (f,g)) . x) + ((f . x) * (h . x)) by Th2
.= (((ComplexFuncMult A) . (f,g)) . x) + (((ComplexFuncMult A) . (f,h)) . x) by Th2
.= ((ComplexFuncAdd A) . (((ComplexFuncMult A) . (f,g)),((ComplexFuncMult A) . (f,h)))) . x by Th1 ; ::_thesis: verum
end;
hence  (ComplexFuncMult A) . (f,((ComplexFuncAdd A) . (g,h))) = (ComplexFuncAdd A) . (((ComplexFuncMult A) . (f,g)),((ComplexFuncMult A) . (f,h))) by FUNCT_2:63; ::_thesis: verum
end;

theorem Th16: :: CFUNCDOM:16
for A being non empty set
for f, g being Element of Funcs (A,COMPLEX)
for a being Element of COMPLEX holds (ComplexFuncMult A) . (((ComplexFuncExtMult A) . [a,f]),g) = (ComplexFuncExtMult A) . [a,((ComplexFuncMult A) . (f,g))]
proof
let A be non empty set ; ::_thesis: for f, g being Element of Funcs (A,COMPLEX)
for a being Element of COMPLEX holds (ComplexFuncMult A) . (((ComplexFuncExtMult A) . [a,f]),g) = (ComplexFuncExtMult A) . [a,((ComplexFuncMult A) . (f,g))]
let f, g be Element of Funcs (A,COMPLEX); ::_thesis: for a being Element of COMPLEX holds (ComplexFuncMult A) . (((ComplexFuncExtMult A) . [a,f]),g) = (ComplexFuncExtMult A) . [a,((ComplexFuncMult A) . (f,g))]
let a be Element of COMPLEX ; ::_thesis: (ComplexFuncMult A) . (((ComplexFuncExtMult A) . [a,f]),g) = (ComplexFuncExtMult A) . [a,((ComplexFuncMult A) . (f,g))]
now__::_thesis:_for_x_being_Element_of_A_holds_((ComplexFuncMult_A)_._(((ComplexFuncExtMult_A)_._[a,f]),g))_._x_=_((ComplexFuncExtMult_A)_._[a,((ComplexFuncMult_A)_._(f,g))])_._x
let x be Element of A; ::_thesis: ((ComplexFuncMult A) . (((ComplexFuncExtMult A) . [a,f]),g)) . x = ((ComplexFuncExtMult A) . [a,((ComplexFuncMult A) . (f,g))]) . x
thus ((ComplexFuncMult A) . (((ComplexFuncExtMult A) . [a,f]),g)) . x = (((ComplexFuncExtMult A) . [a,f]) . x) * (g . x) by Th2
.= (a * (f . x)) * (g . x) by Th4
.= a * ((f . x) * (g . x))
.= a * (((ComplexFuncMult A) . (f,g)) . x) by Th2
.= ((ComplexFuncExtMult A) . [a,((ComplexFuncMult A) . (f,g))]) . x by Th4 ; ::_thesis: verum
end;
hence  (ComplexFuncMult A) . (((ComplexFuncExtMult A) . [a,f]),g) = (ComplexFuncExtMult A) . [a,((ComplexFuncMult A) . (f,g))] by FUNCT_2:63; ::_thesis: verum
end;

begin

theorem Th17: :: CFUNCDOM:17
for x1 being set
for A being non empty set ex f, g being Element of Funcs (A,COMPLEX) st
( ( for z being set st z in A holds
( ( z = x1 implies f . z = 1r ) & ( z <> x1 implies f . z = 0 ) ) ) & ( for z being set st z in A holds
( ( z = x1 implies g . z = 0 ) & ( z <> x1 implies g . z = 1r ) ) ) )
proof
let x1 be set ; ::_thesis: for A being non empty set ex f, g being Element of Funcs (A,COMPLEX) st
( ( for z being set st z in A holds
( ( z = x1 implies f . z = 1r ) & ( z <> x1 implies f . z = 0 ) ) ) & ( for z being set st z in A holds
( ( z = x1 implies g . z = 0 ) & ( z <> x1 implies g . z = 1r ) ) ) )
let A be non empty set ; ::_thesis: ex f, g being Element of Funcs (A,COMPLEX) st
( ( for z being set st z in A holds
( ( z = x1 implies f . z = 1r ) & ( z <> x1 implies f . z = 0 ) ) ) & ( for z being set st z in A holds
( ( z = x1 implies g . z = 0 ) & ( z <> x1 implies g . z = 1r ) ) ) )
deffunc H1( set ) ->  Element of COMPLEX = 1r ;
deffunc H2( set ) ->  Element of COMPLEX = 0c ;
defpred S1[ set ] means $1 = x1;
A1: for z being set st z in A holds
( ( S1[z] implies H1(z) in COMPLEX ) & ( not S1[z] implies H2(z) in COMPLEX ) ) ;
consider f being Function of A,COMPLEX such that
A2: for z being set st z in A holds
( ( S1[z] implies f . z = H1(z) ) & ( not S1[z] implies f . z = H2(z) ) ) from FUNCT_2:sch_5(A1);
A3: for z being set st z in A holds
( ( S1[z] implies H2(z) in COMPLEX ) & ( not S1[z] implies H1(z) in COMPLEX ) ) ;
consider g being Function of A,COMPLEX such that
A4: for z being set st z in A holds
( ( S1[z] implies g . z = H2(z) ) & ( not S1[z] implies g . z = H1(z) ) ) from FUNCT_2:sch_5(A3);
reconsider f = f, g = g as Element of Funcs (A,COMPLEX) by FUNCT_2:8;
take  f ; ::_thesis: ex g being Element of Funcs (A,COMPLEX) st
( ( for z being set st z in A holds
( ( z = x1 implies f . z = 1r ) & ( z <> x1 implies f . z = 0 ) ) ) & ( for z being set st z in A holds
( ( z = x1 implies g . z = 0 ) & ( z <> x1 implies g . z = 1r ) ) ) )
take  g ; ::_thesis: ( ( for z being set st z in A holds
( ( z = x1 implies f . z = 1r ) & ( z <> x1 implies f . z = 0 ) ) ) & ( for z being set st z in A holds
( ( z = x1 implies g . z = 0 ) & ( z <> x1 implies g . z = 1r ) ) ) )
thus  ( ( for z being set st z in A holds
( ( z = x1 implies f . z = 1r ) & ( z <> x1 implies f . z = 0 ) ) ) & ( for z being set st z in A holds
( ( z = x1 implies g . z = 0 ) & ( z <> x1 implies g . z = 1r ) ) ) ) by A2, A4; ::_thesis: verum
end;

theorem Th18: :: CFUNCDOM:18
for x1, x2 being set
for A being non empty set
for f, g being Element of Funcs (A,COMPLEX) st x1 in A & x2 in A & x1 <> x2 & ( for z being set st z in A holds
( ( z = x1 implies f . z = 1r ) & ( z <> x1 implies f . z = 0 ) ) ) & ( for z being set st z in A holds
( ( z = x1 implies g . z = 0 ) & ( z <> x1 implies g . z = 1r ) ) ) holds
for a, b being Element of COMPLEX st (ComplexFuncAdd A) . (((ComplexFuncExtMult A) . [a,f]),((ComplexFuncExtMult A) . [b,g])) = ComplexFuncZero A holds
( a = 0c & b = 0c )
proof
let x1, x2 be set ; ::_thesis: for A being non empty set
for f, g being Element of Funcs (A,COMPLEX) st x1 in A & x2 in A & x1 <> x2 & ( for z being set st z in A holds
( ( z = x1 implies f . z = 1r ) & ( z <> x1 implies f . z = 0 ) ) ) & ( for z being set st z in A holds
( ( z = x1 implies g . z = 0 ) & ( z <> x1 implies g . z = 1r ) ) ) holds
for a, b being Element of COMPLEX st (ComplexFuncAdd A) . (((ComplexFuncExtMult A) . [a,f]),((ComplexFuncExtMult A) . [b,g])) = ComplexFuncZero A holds
( a = 0c & b = 0c )
let A be non empty set ; ::_thesis: for f, g being Element of Funcs (A,COMPLEX) st x1 in A & x2 in A & x1 <> x2 & ( for z being set st z in A holds
( ( z = x1 implies f . z = 1r ) & ( z <> x1 implies f . z = 0 ) ) ) & ( for z being set st z in A holds
( ( z = x1 implies g . z = 0 ) & ( z <> x1 implies g . z = 1r ) ) ) holds
for a, b being Element of COMPLEX st (ComplexFuncAdd A) . (((ComplexFuncExtMult A) . [a,f]),((ComplexFuncExtMult A) . [b,g])) = ComplexFuncZero A holds
( a = 0c & b = 0c )
let f, g be Element of Funcs (A,COMPLEX); ::_thesis: ( x1 in A & x2 in A & x1 <> x2 & ( for z being set st z in A holds
( ( z = x1 implies f . z = 1r ) & ( z <> x1 implies f . z = 0 ) ) ) & ( for z being set st z in A holds
( ( z = x1 implies g . z = 0 ) & ( z <> x1 implies g . z = 1r ) ) ) implies for a, b being Element of COMPLEX st (ComplexFuncAdd A) . (((ComplexFuncExtMult A) . [a,f]),((ComplexFuncExtMult A) . [b,g])) = ComplexFuncZero A holds
( a = 0c & b = 0c ) )
assume that
A1: x1 in A and
A2: x2 in A and
A3: x1 <> x2 and
A4: ( ( for z being set st z in A holds
( ( z = x1 implies f . z = 1r ) & ( z <> x1 implies f . z = 0 ) ) ) & ( for z being set st z in A holds
( ( z = x1 implies g . z = 0 ) & ( z <> x1 implies g . z = 1r ) ) ) ) ; ::_thesis: for a, b being Element of COMPLEX st (ComplexFuncAdd A) . (((ComplexFuncExtMult A) . [a,f]),((ComplexFuncExtMult A) . [b,g])) = ComplexFuncZero A holds
( a = 0c & b = 0c )
A5: ( f . x2 = 0c & g . x2 = 1r ) by A2, A3, A4;
A6: ( f . x1 = 1r & g . x1 = 0c ) by A1, A4;
let a, b be Element of COMPLEX ; ::_thesis: ( (ComplexFuncAdd A) . (((ComplexFuncExtMult A) . [a,f]),((ComplexFuncExtMult A) . [b,g])) = ComplexFuncZero A implies ( a = 0c & b = 0c ) )
reconsider x1 = x1, x2 = x2 as Element of A by A1, A2;
assume A7: (ComplexFuncAdd A) . (((ComplexFuncExtMult A) . [a,f]),((ComplexFuncExtMult A) . [b,g])) = ComplexFuncZero A ; ::_thesis: ( a = 0c & b = 0c )
then A8: 0c = ((ComplexFuncAdd A) . (((ComplexFuncExtMult A) . [a,f]),((ComplexFuncExtMult A) . [b,g]))) . x2 by FUNCOP_1:7
.= (((ComplexFuncExtMult A) . [a,f]) . x2) + (((ComplexFuncExtMult A) . [b,g]) . x2) by Th1
.= (a * (f . x2)) + (((ComplexFuncExtMult A) . [b,g]) . x2) by Th4
.= 0c + (b * 1r) by A5, Th4
.= b by COMPLEX1:def_4 ;
0c = ((ComplexFuncAdd A) . (((ComplexFuncExtMult A) . [a,f]),((ComplexFuncExtMult A) . [b,g]))) . x1 by A7, FUNCOP_1:7
.= (((ComplexFuncExtMult A) . [a,f]) . x1) + (((ComplexFuncExtMult A) . [b,g]) . x1) by Th1
.= (a * (f . x1)) + (((ComplexFuncExtMult A) . [b,g]) . x1) by Th4
.= a + (b * 0c) by A6, Th4, COMPLEX1:def_4
.= a ;
hence  ( a = 0c & b = 0c ) by A8; ::_thesis: verum
end;

theorem :: CFUNCDOM:19
for x1, x2 being set
for A being non empty set st x1 in A & x2 in A & x1 <> x2 holds
ex f, g being Element of Funcs (A,COMPLEX) st
for a, b being Element of COMPLEX st (ComplexFuncAdd A) . (((ComplexFuncExtMult A) . [a,f]),((ComplexFuncExtMult A) . [b,g])) = ComplexFuncZero A holds
( a = 0 & b = 0 )
proof
let x1, x2 be set ; ::_thesis: for A being non empty set st x1 in A & x2 in A & x1 <> x2 holds
ex f, g being Element of Funcs (A,COMPLEX) st
for a, b being Element of COMPLEX st (ComplexFuncAdd A) . (((ComplexFuncExtMult A) . [a,f]),((ComplexFuncExtMult A) . [b,g])) = ComplexFuncZero A holds
( a = 0 & b = 0 )
let A be non empty set ; ::_thesis: ( x1 in A & x2 in A & x1 <> x2 implies ex f, g being Element of Funcs (A,COMPLEX) st
for a, b being Element of COMPLEX st (ComplexFuncAdd A) . (((ComplexFuncExtMult A) . [a,f]),((ComplexFuncExtMult A) . [b,g])) = ComplexFuncZero A holds
( a = 0 & b = 0 ) )
assume A1: ( x1 in A & x2 in A & x1 <> x2 ) ; ::_thesis: ex f, g being Element of Funcs (A,COMPLEX) st
for a, b being Element of COMPLEX st (ComplexFuncAdd A) . (((ComplexFuncExtMult A) . [a,f]),((ComplexFuncExtMult A) . [b,g])) = ComplexFuncZero A holds
( a = 0 & b = 0 )
consider f, g being Element of Funcs (A,COMPLEX) such that
A2: ( ( for z being set st z in A holds
( ( z = x1 implies f . z = 1r ) & ( z <> x1 implies f . z = 0c ) ) ) & ( for z being set st z in A holds
( ( z = x1 implies g . z = 0c ) & ( z <> x1 implies g . z = 1r ) ) ) ) by Th17;
take  f ; ::_thesis: ex g being Element of Funcs (A,COMPLEX) st
for a, b being Element of COMPLEX st (ComplexFuncAdd A) . (((ComplexFuncExtMult A) . [a,f]),((ComplexFuncExtMult A) . [b,g])) = ComplexFuncZero A holds
( a = 0 & b = 0 )
take  g ; ::_thesis: for a, b being Element of COMPLEX st (ComplexFuncAdd A) . (((ComplexFuncExtMult A) . [a,f]),((ComplexFuncExtMult A) . [b,g])) = ComplexFuncZero A holds
( a = 0 & b = 0 )
let a, b be Element of COMPLEX ; ::_thesis: ( (ComplexFuncAdd A) . (((ComplexFuncExtMult A) . [a,f]),((ComplexFuncExtMult A) . [b,g])) = ComplexFuncZero A implies ( a = 0 & b = 0 ) )
assume  (ComplexFuncAdd A) . (((ComplexFuncExtMult A) . [a,f]),((ComplexFuncExtMult A) . [b,g])) = ComplexFuncZero A ; ::_thesis: ( a = 0 & b = 0 )
hence  ( a = 0 & b = 0 ) by A1, A2, Th18; ::_thesis: verum
end;

theorem Th20: :: CFUNCDOM:20
for x1, x2 being set
for A being non empty set
for f, g being Element of Funcs (A,COMPLEX) st A = {x1,x2} & x1 <> x2 & ( for z being set st z in A holds
( ( z = x1 implies f . z = 1r ) & ( z <> x1 implies f . z = 0 ) ) ) & ( for z being set st z in A holds
( ( z = x1 implies g . z = 0 ) & ( z <> x1 implies g . z = 1r ) ) ) holds
for h being Element of Funcs (A,COMPLEX) ex a, b being Element of COMPLEX st h = (ComplexFuncAdd A) . (((ComplexFuncExtMult A) . [a,f]),((ComplexFuncExtMult A) . [b,g]))
proof
let x1, x2 be set ; ::_thesis: for A being non empty set
for f, g being Element of Funcs (A,COMPLEX) st A = {x1,x2} & x1 <> x2 & ( for z being set st z in A holds
( ( z = x1 implies f . z = 1r ) & ( z <> x1 implies f . z = 0 ) ) ) & ( for z being set st z in A holds
( ( z = x1 implies g . z = 0 ) & ( z <> x1 implies g . z = 1r ) ) ) holds
for h being Element of Funcs (A,COMPLEX) ex a, b being Element of COMPLEX st h = (ComplexFuncAdd A) . (((ComplexFuncExtMult A) . [a,f]),((ComplexFuncExtMult A) . [b,g]))
let A be non empty set ; ::_thesis: for f, g being Element of Funcs (A,COMPLEX) st A = {x1,x2} & x1 <> x2 & ( for z being set st z in A holds
( ( z = x1 implies f . z = 1r ) & ( z <> x1 implies f . z = 0 ) ) ) & ( for z being set st z in A holds
( ( z = x1 implies g . z = 0 ) & ( z <> x1 implies g . z = 1r ) ) ) holds
for h being Element of Funcs (A,COMPLEX) ex a, b being Element of COMPLEX st h = (ComplexFuncAdd A) . (((ComplexFuncExtMult A) . [a,f]),((ComplexFuncExtMult A) . [b,g]))
let f, g be Element of Funcs (A,COMPLEX); ::_thesis: ( A = {x1,x2} & x1 <> x2 & ( for z being set st z in A holds
( ( z = x1 implies f . z = 1r ) & ( z <> x1 implies f . z = 0 ) ) ) & ( for z being set st z in A holds
( ( z = x1 implies g . z = 0 ) & ( z <> x1 implies g . z = 1r ) ) ) implies for h being Element of Funcs (A,COMPLEX) ex a, b being Element of COMPLEX st h = (ComplexFuncAdd A) . (((ComplexFuncExtMult A) . [a,f]),((ComplexFuncExtMult A) . [b,g])) )
assume that
A1: A = {x1,x2} and
A2: x1 <> x2 and
A3: ( ( for z being set st z in A holds
( ( z = x1 implies f . z = 1r ) & ( z <> x1 implies f . z = 0 ) ) ) & ( for z being set st z in A holds
( ( z = x1 implies g . z = 0 ) & ( z <> x1 implies g . z = 1r ) ) ) ) ; ::_thesis: for h being Element of Funcs (A,COMPLEX) ex a, b being Element of COMPLEX st h = (ComplexFuncAdd A) . (((ComplexFuncExtMult A) . [a,f]),((ComplexFuncExtMult A) . [b,g]))
 x2 in A by A1, TARSKI:def_2;
then A4: ( f . x2 = 0c & g . x2 = 1r ) by A2, A3;
 x1 in A by A1, TARSKI:def_2;
then A5: ( f . x1 = 1r & g . x1 = 0c ) by A3;
let h be Element of Funcs (A,COMPLEX); ::_thesis: ex a, b being Element of COMPLEX st h = (ComplexFuncAdd A) . (((ComplexFuncExtMult A) . [a,f]),((ComplexFuncExtMult A) . [b,g]))
reconsider x1 = x1, x2 = x2 as Element of A by A1, TARSKI:def_2;
take a = h . x1; ::_thesis: ex b being Element of COMPLEX st h = (ComplexFuncAdd A) . (((ComplexFuncExtMult A) . [a,f]),((ComplexFuncExtMult A) . [b,g]))
take b = h . x2; ::_thesis: h = (ComplexFuncAdd A) . (((ComplexFuncExtMult A) . [a,f]),((ComplexFuncExtMult A) . [b,g]))
now__::_thesis:_for_x_being_Element_of_A_holds_h_._x_=_((ComplexFuncAdd_A)_._(((ComplexFuncExtMult_A)_._[a,f]),((ComplexFuncExtMult_A)_._[b,g])))_._x
let x be Element of A; ::_thesis: h . x = ((ComplexFuncAdd A) . (((ComplexFuncExtMult A) . [a,f]),((ComplexFuncExtMult A) . [b,g]))) . x
A6: ( x = x1 or x = x2 ) by A1, TARSKI:def_2;
A7: ((ComplexFuncAdd A) . (((ComplexFuncExtMult A) . [a,f]),((ComplexFuncExtMult A) . [b,g]))) . x2 = (((ComplexFuncExtMult A) . [a,f]) . x2) + (((ComplexFuncExtMult A) . [b,g]) . x2) by Th1
.= (a * (f . x2)) + (((ComplexFuncExtMult A) . [b,g]) . x2) by Th4
.= 0c + (b * 1r) by A4, Th4
.= h . x2 by COMPLEX1:def_4 ;
((ComplexFuncAdd A) . (((ComplexFuncExtMult A) . [a,f]),((ComplexFuncExtMult A) . [b,g]))) . x1 = (((ComplexFuncExtMult A) . [a,f]) . x1) + (((ComplexFuncExtMult A) . [b,g]) . x1) by Th1
.= (a * (f . x1)) + (((ComplexFuncExtMult A) . [b,g]) . x1) by Th4
.= a + (b * 0c) by A5, Th4, COMPLEX1:def_4
.= h . x1 ;
hence  h . x = ((ComplexFuncAdd A) . (((ComplexFuncExtMult A) . [a,f]),((ComplexFuncExtMult A) . [b,g]))) . x by A6, A7; ::_thesis: verum
end;
hence  h = (ComplexFuncAdd A) . (((ComplexFuncExtMult A) . [a,f]),((ComplexFuncExtMult A) . [b,g])) by FUNCT_2:63; ::_thesis: verum
end;

theorem :: CFUNCDOM:21
for x1, x2 being set
for A being non empty set st A = {x1,x2} & x1 <> x2 holds
ex f, g being Element of Funcs (A,COMPLEX) st
for h being Element of Funcs (A,COMPLEX) ex a, b being Element of COMPLEX st h = (ComplexFuncAdd A) . (((ComplexFuncExtMult A) . [a,f]),((ComplexFuncExtMult A) . [b,g]))
proof
let x1, x2 be set ; ::_thesis: for A being non empty set st A = {x1,x2} & x1 <> x2 holds
ex f, g being Element of Funcs (A,COMPLEX) st
for h being Element of Funcs (A,COMPLEX) ex a, b being Element of COMPLEX st h = (ComplexFuncAdd A) . (((ComplexFuncExtMult A) . [a,f]),((ComplexFuncExtMult A) . [b,g]))
let A be non empty set ; ::_thesis: ( A = {x1,x2} & x1 <> x2 implies ex f, g being Element of Funcs (A,COMPLEX) st
for h being Element of Funcs (A,COMPLEX) ex a, b being Element of COMPLEX st h = (ComplexFuncAdd A) . (((ComplexFuncExtMult A) . [a,f]),((ComplexFuncExtMult A) . [b,g])) )
assume A1: ( A = {x1,x2} & x1 <> x2 ) ; ::_thesis: ex f, g being Element of Funcs (A,COMPLEX) st
for h being Element of Funcs (A,COMPLEX) ex a, b being Element of COMPLEX st h = (ComplexFuncAdd A) . (((ComplexFuncExtMult A) . [a,f]),((ComplexFuncExtMult A) . [b,g]))
consider f, g being Element of Funcs (A,COMPLEX) such that
A2: ( ( for z being set st z in A holds
( ( z = x1 implies f . z = 1r ) & ( z <> x1 implies f . z = 0c ) ) ) & ( for z being set st z in A holds
( ( z = x1 implies g . z = 0c ) & ( z <> x1 implies g . z = 1r ) ) ) ) by Th17;
take  f ; ::_thesis: ex g being Element of Funcs (A,COMPLEX) st
for h being Element of Funcs (A,COMPLEX) ex a, b being Element of COMPLEX st h = (ComplexFuncAdd A) . (((ComplexFuncExtMult A) . [a,f]),((ComplexFuncExtMult A) . [b,g]))
take  g ; ::_thesis: for h being Element of Funcs (A,COMPLEX) ex a, b being Element of COMPLEX st h = (ComplexFuncAdd A) . (((ComplexFuncExtMult A) . [a,f]),((ComplexFuncExtMult A) . [b,g]))
let h be Element of Funcs (A,COMPLEX); ::_thesis: ex a, b being Element of COMPLEX st h = (ComplexFuncAdd A) . (((ComplexFuncExtMult A) . [a,f]),((ComplexFuncExtMult A) . [b,g]))
thus  ex a, b being Element of COMPLEX st h = (ComplexFuncAdd A) . (((ComplexFuncExtMult A) . [a,f]),((ComplexFuncExtMult A) . [b,g])) by A1, A2, Th20; ::_thesis: verum
end;

theorem Th22: :: CFUNCDOM:22
for x1, x2 being set
for A being non empty set st A = {x1,x2} & x1 <> x2 holds
ex f, g being Element of Funcs (A,COMPLEX) st
( ( for a, b being Element of COMPLEX st (ComplexFuncAdd A) . (((ComplexFuncExtMult A) . [a,f]),((ComplexFuncExtMult A) . [b,g])) = ComplexFuncZero A holds
( a = 0 & b = 0 ) ) & ( for h being Element of Funcs (A,COMPLEX) ex a, b being Element of COMPLEX st h = (ComplexFuncAdd A) . (((ComplexFuncExtMult A) . [a,f]),((ComplexFuncExtMult A) . [b,g])) ) )
proof
let x1, x2 be set ; ::_thesis: for A being non empty set st A = {x1,x2} & x1 <> x2 holds
ex f, g being Element of Funcs (A,COMPLEX) st
( ( for a, b being Element of COMPLEX st (ComplexFuncAdd A) . (((ComplexFuncExtMult A) . [a,f]),((ComplexFuncExtMult A) . [b,g])) = ComplexFuncZero A holds
( a = 0 & b = 0 ) ) & ( for h being Element of Funcs (A,COMPLEX) ex a, b being Element of COMPLEX st h = (ComplexFuncAdd A) . (((ComplexFuncExtMult A) . [a,f]),((ComplexFuncExtMult A) . [b,g])) ) )
let A be non empty set ; ::_thesis: ( A = {x1,x2} & x1 <> x2 implies ex f, g being Element of Funcs (A,COMPLEX) st
( ( for a, b being Element of COMPLEX st (ComplexFuncAdd A) . (((ComplexFuncExtMult A) . [a,f]),((ComplexFuncExtMult A) . [b,g])) = ComplexFuncZero A holds
( a = 0 & b = 0 ) ) & ( for h being Element of Funcs (A,COMPLEX) ex a, b being Element of COMPLEX st h = (ComplexFuncAdd A) . (((ComplexFuncExtMult A) . [a,f]),((ComplexFuncExtMult A) . [b,g])) ) ) )
assume that
A1: A = {x1,x2} and
A2: x1 <> x2 ; ::_thesis: ex f, g being Element of Funcs (A,COMPLEX) st
( ( for a, b being Element of COMPLEX st (ComplexFuncAdd A) . (((ComplexFuncExtMult A) . [a,f]),((ComplexFuncExtMult A) . [b,g])) = ComplexFuncZero A holds
( a = 0 & b = 0 ) ) & ( for h being Element of Funcs (A,COMPLEX) ex a, b being Element of COMPLEX st h = (ComplexFuncAdd A) . (((ComplexFuncExtMult A) . [a,f]),((ComplexFuncExtMult A) . [b,g])) ) )
consider f, g being Element of Funcs (A,COMPLEX) such that
A3: ( ( for z being set st z in A holds
( ( z = x1 implies f . z = 1r ) & ( z <> x1 implies f . z = 0c ) ) ) & ( for z being set st z in A holds
( ( z = x1 implies g . z = 0c ) & ( z <> x1 implies g . z = 1r ) ) ) ) by Th17;
take  f ; ::_thesis: ex g being Element of Funcs (A,COMPLEX) st
( ( for a, b being Element of COMPLEX st (ComplexFuncAdd A) . (((ComplexFuncExtMult A) . [a,f]),((ComplexFuncExtMult A) . [b,g])) = ComplexFuncZero A holds
( a = 0 & b = 0 ) ) & ( for h being Element of Funcs (A,COMPLEX) ex a, b being Element of COMPLEX st h = (ComplexFuncAdd A) . (((ComplexFuncExtMult A) . [a,f]),((ComplexFuncExtMult A) . [b,g])) ) )
take  g ; ::_thesis: ( ( for a, b being Element of COMPLEX st (ComplexFuncAdd A) . (((ComplexFuncExtMult A) . [a,f]),((ComplexFuncExtMult A) . [b,g])) = ComplexFuncZero A holds
( a = 0 & b = 0 ) ) & ( for h being Element of Funcs (A,COMPLEX) ex a, b being Element of COMPLEX st h = (ComplexFuncAdd A) . (((ComplexFuncExtMult A) . [a,f]),((ComplexFuncExtMult A) . [b,g])) ) )
 ( x1 in A & x2 in A ) by A1, TARSKI:def_2;
hence  ( ( for a, b being Element of COMPLEX st (ComplexFuncAdd A) . (((ComplexFuncExtMult A) . [a,f]),((ComplexFuncExtMult A) . [b,g])) = ComplexFuncZero A holds
( a = 0 & b = 0 ) ) & ( for h being Element of Funcs (A,COMPLEX) ex a, b being Element of COMPLEX st h = (ComplexFuncAdd A) . (((ComplexFuncExtMult A) . [a,f]),((ComplexFuncExtMult A) . [b,g])) ) ) by A1, A2, A3, Th18, Th20; ::_thesis: verum
end;

definition
let A be non empty set ;
func ComplexVectSpace A ->  non empty strict CLSStruct  equals :: CFUNCDOM:def 6
 CLSStruct(# (Funcs (A,COMPLEX)),(ComplexFuncZero A),(ComplexFuncAdd A),(ComplexFuncExtMult A) #);
coherence
 CLSStruct(# (Funcs (A,COMPLEX)),(ComplexFuncZero A),(ComplexFuncAdd A),(ComplexFuncExtMult A) #) is non empty strict CLSStruct ;
end;

:: deftheorem  defines ComplexVectSpace CFUNCDOM:def_6_:_
 for A being non empty set holds ComplexVectSpace A = CLSStruct(# (Funcs (A,COMPLEX)),(ComplexFuncZero A),(ComplexFuncAdd A),(ComplexFuncExtMult A) #);


registration
let A be non empty set ;
cluster ComplexVectSpace A ->  non empty right_complementable Abelian add-associative right_zeroed strict vector-distributive scalar-distributive scalar-associative scalar-unital for non empty strict CLSStruct ;
coherence
 for b1 being non empty strict CLSStruct st b1 = ComplexVectSpace A holds
( b1 is Abelian & b1 is add-associative & b1 is right_zeroed & b1 is right_complementable & b1 is vector-distributive & b1 is scalar-distributive & b1 is scalar-associative & b1 is scalar-unital )
proof
let C be non empty strict CLSStruct ; ::_thesis: ( C = ComplexVectSpace A implies ( C is Abelian & C is add-associative & C is right_zeroed & C is right_complementable & C is vector-distributive & C is scalar-distributive & C is scalar-associative & C is scalar-unital ) )
assume A1: C = ComplexVectSpace A ; ::_thesis: ( C is Abelian & C is add-associative & C is right_zeroed & C is right_complementable & C is vector-distributive & C is scalar-distributive & C is scalar-associative & C is scalar-unital )
thus  for u, v being Element of C holds u + v = v + u by Th5, A1; :: according to RLVECT_1:def_2 ::_thesis: ( C is add-associative & C is right_zeroed & C is right_complementable & C is vector-distributive & C is scalar-distributive & C is scalar-associative & C is scalar-unital )
thus  for u, v, w being Element of C holds (u + v) + w = u + (v + w) by Th6, A1; :: according to RLVECT_1:def_3 ::_thesis: ( C is right_zeroed & C is right_complementable & C is vector-distributive & C is scalar-distributive & C is scalar-associative & C is scalar-unital )
thus  for u being Element of C holds u + (0. C) = u :: according to RLVECT_1:def_4 ::_thesis: ( C is right_complementable & C is vector-distributive & C is scalar-distributive & C is scalar-associative & C is scalar-unital )
proof
let u be Element of C; ::_thesis: u + (0. C) = u
reconsider v = u as Element of Funcs (A,COMPLEX) by A1;
thus u + (0. C) = (ComplexFuncAdd A) . ((ComplexFuncZero A),v) by Th5, A1
.= u by Th10 ; ::_thesis: verum
end;
thus  for u being Element of C holds u is right_complementable :: according to ALGSTR_0:def_16 ::_thesis: ( C is vector-distributive & C is scalar-distributive & C is scalar-associative & C is scalar-unital )
proof
let u be Element of C; ::_thesis: u is right_complementable
reconsider v = u as Element of Funcs (A,COMPLEX) by A1;
reconsider w = (ComplexFuncExtMult A) . [(- 1r),v] as VECTOR of C by A1;
take  w ; :: according to ALGSTR_0:def_11 ::_thesis: u + w = 0. C
thus  u + w = 0. C by Th11, A1; ::_thesis: verum
end;
thus  for a being Complex
for u, v being VECTOR of C holds a * (u + v) = (a * u) + (a * v) by Lm2, A1; :: according to CLVECT_1:def_2 ::_thesis: ( C is scalar-distributive & C is scalar-associative & C is scalar-unital )
thus  for a, b being Complex
for v being VECTOR of C holds (a + b) * v = (a * v) + (b * v) by Th14, A1; :: according to CLVECT_1:def_3 ::_thesis: ( C is scalar-associative & C is scalar-unital )
thus  for a, b being Complex
for v being VECTOR of C holds (a * b) * v = a * (b * v) by Th13, A1; :: according to CLVECT_1:def_4 ::_thesis: C is scalar-unital
thus  for v being Element of C holds 1r * v = v by Th12, A1; :: according to CLVECT_1:def_5 ::_thesis: verum
end;
end;

Lm3:  ex A being non empty set ex x1, x2 being set st
( A = {x1,x2} & x1 <> x2 )
proof
reconsider A = {1,2} as non empty set ;
take  A ; ::_thesis: ex x1, x2 being set st
( A = {x1,x2} & x1 <> x2 )
thus  ex x1, x2 being set st
( A = {x1,x2} & x1 <> x2 ) ; ::_thesis: verum
end;

theorem :: CFUNCDOM:23
ex V being strict ComplexLinearSpace ex u, v being VECTOR of V st
( ( for a, b being Element of COMPLEX st (a * u) + (b * v) = 0. V holds
( a = 0 & b = 0 ) ) & ( for w being VECTOR of V ex a, b being Element of COMPLEX st w = (a * u) + (b * v) ) )
proof
consider A being non empty set , x1, x2 being set  such that
A1: ( A = {x1,x2} & x1 <> x2 ) by Lm3;
take V = ComplexVectSpace A; ::_thesis: ex u, v being VECTOR of V st
( ( for a, b being Element of COMPLEX st (a * u) + (b * v) = 0. V holds
( a = 0 & b = 0 ) ) & ( for w being VECTOR of V ex a, b being Element of COMPLEX st w = (a * u) + (b * v) ) )
consider f, g being Element of Funcs (A,COMPLEX) such that
A2: for a, b being Element of COMPLEX st (ComplexFuncAdd A) . (((ComplexFuncExtMult A) . [a,f]),((ComplexFuncExtMult A) . [b,g])) = ComplexFuncZero A holds
( a = 0c & b = 0c ) and
A3: for h being Element of Funcs (A,COMPLEX) ex a, b being Element of COMPLEX st h = (ComplexFuncAdd A) . (((ComplexFuncExtMult A) . [a,f]),((ComplexFuncExtMult A) . [b,g])) by A1, Th22;
reconsider u = f, v = g as VECTOR of V ;
take  u ; ::_thesis: ex v being VECTOR of V st
( ( for a, b being Element of COMPLEX st (a * u) + (b * v) = 0. V holds
( a = 0 & b = 0 ) ) & ( for w being VECTOR of V ex a, b being Element of COMPLEX st w = (a * u) + (b * v) ) )
take  v ; ::_thesis: ( ( for a, b being Element of COMPLEX st (a * u) + (b * v) = 0. V holds
( a = 0 & b = 0 ) ) & ( for w being VECTOR of V ex a, b being Element of COMPLEX st w = (a * u) + (b * v) ) )
thus  for a, b being Element of COMPLEX st (a * u) + (b * v) = 0. V holds
( a = 0 & b = 0 ) by A2; ::_thesis: for w being VECTOR of V ex a, b being Element of COMPLEX st w = (a * u) + (b * v)
thus  for w being VECTOR of V ex a, b being Element of COMPLEX st w = (a * u) + (b * v) ::_thesis: verum
proof
let w be VECTOR of V; ::_thesis: ex a, b being Element of COMPLEX st w = (a * u) + (b * v)
reconsider h = w as Element of Funcs (A,COMPLEX) ;
consider a, b being Element of COMPLEX  such that
A4: h = (ComplexFuncAdd A) . (((ComplexFuncExtMult A) . [a,f]),((ComplexFuncExtMult A) . [b,g])) by A3;
 h = (a * u) + (b * v) by A4;
hence  ex a, b being Element of COMPLEX st w = (a * u) + (b * v) ; ::_thesis: verum
end;
end;

definition
let A be non empty set ;
func CRing A ->  doubleLoopStr  equals :: CFUNCDOM:def 7
 doubleLoopStr(# (Funcs (A,COMPLEX)),(ComplexFuncAdd A),(ComplexFuncMult A),(ComplexFuncUnit A),(ComplexFuncZero A) #);
correctness
coherence
doubleLoopStr(# (Funcs (A,COMPLEX)),(ComplexFuncAdd A),(ComplexFuncMult A),(ComplexFuncUnit A),(ComplexFuncZero A) #) is doubleLoopStr ;
;
end;

:: deftheorem  defines CRing CFUNCDOM:def_7_:_
 for A being non empty set holds CRing A = doubleLoopStr(# (Funcs (A,COMPLEX)),(ComplexFuncAdd A),(ComplexFuncMult A),(ComplexFuncUnit A),(ComplexFuncZero A) #);

registration
let A be non empty set ;
cluster CRing A ->  non empty strict ;
coherence
 ( not CRing A is empty & CRing A is strict ) ;
end;

Lm4: now__::_thesis:_for_A_being_non_empty_set_
for_x,_e_being_Element_of_(CRing_A)_st_e_=_ComplexFuncUnit_A_holds_
(_e_*_x_=_x_&_x_*_e_=_x_)
let A be non empty set ; ::_thesis: for x, e being Element of (CRing A) st e = ComplexFuncUnit A holds
( e * x = x & x * e = x )
let x, e be Element of (CRing A); ::_thesis: ( e = ComplexFuncUnit A implies ( e * x = x & x * e = x ) )
assume  e = ComplexFuncUnit A ; ::_thesis: ( e * x = x & x * e = x )
hence  e * x = x by Th9; ::_thesis: x * e = x
hence  x * e = x by Th7; ::_thesis: verum
end;

registration
let A be non empty set ;
cluster CRing A ->  unital ;
coherence
 CRing A is unital
proof
reconsider e = ComplexFuncUnit A as Element of (CRing A) ;
take  e ; :: according to GROUP_1:def_1 ::_thesis: for b1 being Element of the carrier of (CRing A) holds
( b1 * e = b1 & e * b1 = b1 )
thus  for b1 being Element of the carrier of (CRing A) holds
( b1 * e = b1 & e * b1 = b1 ) by Lm4; ::_thesis: verum
end;
end;

theorem Th24: :: CFUNCDOM:24
for A being non empty set
for x, y, z being Element of (CRing A) holds
( x + y = y + x & (x + y) + z = x + (y + z) & x + (0. (CRing A)) = x & x is right_complementable & x * y = y * x & (x * y) * z = x * (y * z) & x * (1. (CRing A)) = x & (1. (CRing A)) * x = x & x * (y + z) = (x * y) + (x * z) & (y + z) * x = (y * x) + (z * x) )
proof
let A be non empty set ; ::_thesis: for x, y, z being Element of (CRing A) holds
( x + y = y + x & (x + y) + z = x + (y + z) & x + (0. (CRing A)) = x & x is right_complementable & x * y = y * x & (x * y) * z = x * (y * z) & x * (1. (CRing A)) = x & (1. (CRing A)) * x = x & x * (y + z) = (x * y) + (x * z) & (y + z) * x = (y * x) + (z * x) )
let x, y, z be Element of (CRing A); ::_thesis: ( x + y = y + x & (x + y) + z = x + (y + z) & x + (0. (CRing A)) = x & x is right_complementable & x * y = y * x & (x * y) * z = x * (y * z) & x * (1. (CRing A)) = x & (1. (CRing A)) * x = x & x * (y + z) = (x * y) + (x * z) & (y + z) * x = (y * x) + (z * x) )
set IT = CRing A;
reconsider f = x as Element of Funcs (A,COMPLEX) ;
thus  x + y = y + x by Th5; ::_thesis: ( (x + y) + z = x + (y + z) & x + (0. (CRing A)) = x & x is right_complementable & x * y = y * x & (x * y) * z = x * (y * z) & x * (1. (CRing A)) = x & (1. (CRing A)) * x = x & x * (y + z) = (x * y) + (x * z) & (y + z) * x = (y * x) + (z * x) )
thus  (x + y) + z = x + (y + z) by Th6; ::_thesis: ( x + (0. (CRing A)) = x & x is right_complementable & x * y = y * x & (x * y) * z = x * (y * z) & x * (1. (CRing A)) = x & (1. (CRing A)) * x = x & x * (y + z) = (x * y) + (x * z) & (y + z) * x = (y * x) + (z * x) )
thus x + (0. (CRing A)) = (ComplexFuncAdd A) . ((ComplexFuncZero A),f) by Th5
.= x by Th10 ; ::_thesis: ( x is right_complementable & x * y = y * x & (x * y) * z = x * (y * z) & x * (1. (CRing A)) = x & (1. (CRing A)) * x = x & x * (y + z) = (x * y) + (x * z) & (y + z) * x = (y * x) + (z * x) )
thus  ex t being Element of (CRing A) st x + t = 0. (CRing A) :: according to ALGSTR_0:def_11 ::_thesis: ( x * y = y * x & (x * y) * z = x * (y * z) & x * (1. (CRing A)) = x & (1. (CRing A)) * x = x & x * (y + z) = (x * y) + (x * z) & (y + z) * x = (y * x) + (z * x) )
proof
set h = (ComplexFuncExtMult A) . [(- 1r),f];
reconsider t = (ComplexFuncExtMult A) . [(- 1r),f] as Element of (CRing A) ;
take  t ; ::_thesis: x + t = 0. (CRing A)
thus  x + t = 0. (CRing A) by Th11; ::_thesis: verum
end;
thus  x * y = y * x by Th7; ::_thesis: ( (x * y) * z = x * (y * z) & x * (1. (CRing A)) = x & (1. (CRing A)) * x = x & x * (y + z) = (x * y) + (x * z) & (y + z) * x = (y * x) + (z * x) )
thus  (x * y) * z = x * (y * z) by Th8; ::_thesis: ( x * (1. (CRing A)) = x & (1. (CRing A)) * x = x & x * (y + z) = (x * y) + (x * z) & (y + z) * x = (y * x) + (z * x) )
thus x * (1. (CRing A)) = (ComplexFuncMult A) . ((ComplexFuncUnit A),f) by Th7
.= x by Th9 ; ::_thesis: ( (1. (CRing A)) * x = x & x * (y + z) = (x * y) + (x * z) & (y + z) * x = (y * x) + (z * x) )
hence  (1. (CRing A)) * x = x by Th7; ::_thesis: ( x * (y + z) = (x * y) + (x * z) & (y + z) * x = (y * x) + (z * x) )
thus  x * (y + z) = (x * y) + (x * z) by Th15; ::_thesis: (y + z) * x = (y * x) + (z * x)
hence (y + z) * x = (x * y) + (x * z) by Th7
.= (y * x) + (x * z) by Th7
.= (y * x) + (z * x) by Th7 ;
::_thesis: verum
end;

theorem :: CFUNCDOM:25
for A being non empty set holds CRing A is commutative Ring
proof
let A be non empty set ; ::_thesis: CRing A is commutative Ring
 for x, y, z being Element of (CRing A) holds
( x + y = y + x & (x + y) + z = x + (y + z) & x + (0. (CRing A)) = x & x is right_complementable & x * y = y * x & (x * y) * z = x * (y * z) & x * (1. (CRing A)) = x & (1. (CRing A)) * x = x & x * (y + z) = (x * y) + (x * z) & (y + z) * x = (y * x) + (z * x) ) by Th24;
hence  CRing A is commutative Ring by ALGSTR_0:def_16, GROUP_1:def_3, GROUP_1:def_12, RLVECT_1:def_2, RLVECT_1:def_3, RLVECT_1:def_4, VECTSP_1:def_6, VECTSP_1:def_7; ::_thesis: verum
end;

definition
attrc1 is strict ;
struct ComplexAlgebraStr  ->  doubleLoopStr , CLSStruct ;
aggrComplexAlgebraStr(# carrier, multF, addF, Mult, OneF, ZeroF #) ->  ComplexAlgebraStr ;
end;

registration
cluster non empty for ComplexAlgebraStr ;
existence
 not for b1 being ComplexAlgebraStr holds b1 is empty
proof
set X = the non empty set ;
set m = the BinOp of the non empty set ;
set M = the Function of [:COMPLEX, the non empty set :], the non empty set ;
set u = the Element of the non empty set ;
take  ComplexAlgebraStr(# the non empty set , the BinOp of the non empty set , the BinOp of the non empty set , the Function of [:COMPLEX, the non empty set :], the non empty set , the Element of the non empty set , the Element of the non empty set #) ; ::_thesis: not ComplexAlgebraStr(# the non empty set , the BinOp of the non empty set , the BinOp of the non empty set , the Function of [:COMPLEX, the non empty set :], the non empty set , the Element of the non empty set , the Element of the non empty set #) is empty
thus  not the carrier of ComplexAlgebraStr(# the non empty set , the BinOp of the non empty set , the BinOp of the non empty set , the Function of [:COMPLEX, the non empty set :], the non empty set , the Element of the non empty set , the Element of the non empty set #) is empty ; :: according to STRUCT_0:def_1 ::_thesis: verum
end;
end;

definition
let A be non empty set ;
func CAlgebra A ->  strict ComplexAlgebraStr  equals :: CFUNCDOM:def 8
 ComplexAlgebraStr(# (Funcs (A,COMPLEX)),(ComplexFuncMult A),(ComplexFuncAdd A),(ComplexFuncExtMult A),(ComplexFuncUnit A),(ComplexFuncZero A) #);
correctness
coherence
ComplexAlgebraStr(# (Funcs (A,COMPLEX)),(ComplexFuncMult A),(ComplexFuncAdd A),(ComplexFuncExtMult A),(ComplexFuncUnit A),(ComplexFuncZero A) #) is strict ComplexAlgebraStr ;
;
end;

:: deftheorem  defines CAlgebra CFUNCDOM:def_8_:_
 for A being non empty set holds CAlgebra A = ComplexAlgebraStr(# (Funcs (A,COMPLEX)),(ComplexFuncMult A),(ComplexFuncAdd A),(ComplexFuncExtMult A),(ComplexFuncUnit A),(ComplexFuncZero A) #);

registration
let A be non empty set ;
cluster CAlgebra A ->  non empty strict ;
coherence
 not CAlgebra A is empty
proof
thus  not the carrier of (CAlgebra A) is empty ; :: according to STRUCT_0:def_1 ::_thesis: verum
end;
end;

Lm5: now__::_thesis:_for_A_being_non_empty_set_
for_x,_e_being_Element_of_(CAlgebra_A)_st_e_=_ComplexFuncUnit_A_holds_
(_e_*_x_=_x_&_x_*_e_=_x_)
let A be non empty set ; ::_thesis: for x, e being Element of (CAlgebra A) st e = ComplexFuncUnit A holds
( e * x = x & x * e = x )
let x, e be Element of (CAlgebra A); ::_thesis: ( e = ComplexFuncUnit A implies ( e * x = x & x * e = x ) )
assume  e = ComplexFuncUnit A ; ::_thesis: ( e * x = x & x * e = x )
hence  e * x = x by Th9; ::_thesis: x * e = x
hence  x * e = x by Th7; ::_thesis: verum
end;

registration
let A be non empty set ;
cluster CAlgebra A ->  unital strict ;
coherence
 CAlgebra A is unital
proof
reconsider e = ComplexFuncUnit A as Element of (CAlgebra A) ;
take  e ; :: according to GROUP_1:def_1 ::_thesis: for b1 being Element of the carrier of (CAlgebra A) holds
( b1 * e = b1 & e * b1 = b1 )
thus  for b1 being Element of the carrier of (CAlgebra A) holds
( b1 * e = b1 & e * b1 = b1 ) by Lm5; ::_thesis: verum
end;
end;

theorem :: CFUNCDOM:26
for A being non empty set
for x, y, z being Element of (CAlgebra A)
for a, b being Element of COMPLEX holds
( x + y = y + x & (x + y) + z = x + (y + z) & x + (0. (CAlgebra A)) = x & x is right_complementable & x * y = y * x & (x * y) * z = x * (y * z) & x * (1. (CAlgebra A)) = x & x * (y + z) = (x * y) + (x * z) & a * (x * y) = (a * x) * y & a * (x + y) = (a * x) + (a * y) & (a + b) * x = (a * x) + (b * x) & (a * b) * x = a * (b * x) )
proof
let A be non empty set ; ::_thesis: for x, y, z being Element of (CAlgebra A)
for a, b being Element of COMPLEX holds
( x + y = y + x & (x + y) + z = x + (y + z) & x + (0. (CAlgebra A)) = x & x is right_complementable & x * y = y * x & (x * y) * z = x * (y * z) & x * (1. (CAlgebra A)) = x & x * (y + z) = (x * y) + (x * z) & a * (x * y) = (a * x) * y & a * (x + y) = (a * x) + (a * y) & (a + b) * x = (a * x) + (b * x) & (a * b) * x = a * (b * x) )
let x, y, z be Element of (CAlgebra A); ::_thesis: for a, b being Element of COMPLEX holds
( x + y = y + x & (x + y) + z = x + (y + z) & x + (0. (CAlgebra A)) = x & x is right_complementable & x * y = y * x & (x * y) * z = x * (y * z) & x * (1. (CAlgebra A)) = x & x * (y + z) = (x * y) + (x * z) & a * (x * y) = (a * x) * y & a * (x + y) = (a * x) + (a * y) & (a + b) * x = (a * x) + (b * x) & (a * b) * x = a * (b * x) )
let a, b be Element of COMPLEX ; ::_thesis: ( x + y = y + x & (x + y) + z = x + (y + z) & x + (0. (CAlgebra A)) = x & x is right_complementable & x * y = y * x & (x * y) * z = x * (y * z) & x * (1. (CAlgebra A)) = x & x * (y + z) = (x * y) + (x * z) & a * (x * y) = (a * x) * y & a * (x + y) = (a * x) + (a * y) & (a + b) * x = (a * x) + (b * x) & (a * b) * x = a * (b * x) )
set IT = CAlgebra A;
reconsider f = x as Element of Funcs (A,COMPLEX) ;
thus  x + y = y + x by Th5; ::_thesis: ( (x + y) + z = x + (y + z) & x + (0. (CAlgebra A)) = x & x is right_complementable & x * y = y * x & (x * y) * z = x * (y * z) & x * (1. (CAlgebra A)) = x & x * (y + z) = (x * y) + (x * z) & a * (x * y) = (a * x) * y & a * (x + y) = (a * x) + (a * y) & (a + b) * x = (a * x) + (b * x) & (a * b) * x = a * (b * x) )
thus  (x + y) + z = x + (y + z) by Th6; ::_thesis: ( x + (0. (CAlgebra A)) = x & x is right_complementable & x * y = y * x & (x * y) * z = x * (y * z) & x * (1. (CAlgebra A)) = x & x * (y + z) = (x * y) + (x * z) & a * (x * y) = (a * x) * y & a * (x + y) = (a * x) + (a * y) & (a + b) * x = (a * x) + (b * x) & (a * b) * x = a * (b * x) )
thus x + (0. (CAlgebra A)) = (ComplexFuncAdd A) . ((ComplexFuncZero A),f) by Th5
.= x by Th10 ; ::_thesis: ( x is right_complementable & x * y = y * x & (x * y) * z = x * (y * z) & x * (1. (CAlgebra A)) = x & x * (y + z) = (x * y) + (x * z) & a * (x * y) = (a * x) * y & a * (x + y) = (a * x) + (a * y) & (a + b) * x = (a * x) + (b * x) & (a * b) * x = a * (b * x) )
thus  ex t being Element of (CAlgebra A) st x + t = 0. (CAlgebra A) :: according to ALGSTR_0:def_11 ::_thesis: ( x * y = y * x & (x * y) * z = x * (y * z) & x * (1. (CAlgebra A)) = x & x * (y + z) = (x * y) + (x * z) & a * (x * y) = (a * x) * y & a * (x + y) = (a * x) + (a * y) & (a + b) * x = (a * x) + (b * x) & (a * b) * x = a * (b * x) )
proof
set h = (ComplexFuncExtMult A) . [(- 1r),f];
reconsider t = (ComplexFuncExtMult A) . [(- 1r),f] as Element of (CAlgebra A) ;
take  t ; ::_thesis: x + t = 0. (CAlgebra A)
thus  x + t = 0. (CAlgebra A) by Th11; ::_thesis: verum
end;
thus  x * y = y * x by Th7; ::_thesis: ( (x * y) * z = x * (y * z) & x * (1. (CAlgebra A)) = x & x * (y + z) = (x * y) + (x * z) & a * (x * y) = (a * x) * y & a * (x + y) = (a * x) + (a * y) & (a + b) * x = (a * x) + (b * x) & (a * b) * x = a * (b * x) )
thus  (x * y) * z = x * (y * z) by Th8; ::_thesis: ( x * (1. (CAlgebra A)) = x & x * (y + z) = (x * y) + (x * z) & a * (x * y) = (a * x) * y & a * (x + y) = (a * x) + (a * y) & (a + b) * x = (a * x) + (b * x) & (a * b) * x = a * (b * x) )
thus x * (1. (CAlgebra A)) = (ComplexFuncMult A) . ((ComplexFuncUnit A),f) by Th7
.= x by Th9 ; ::_thesis: ( x * (y + z) = (x * y) + (x * z) & a * (x * y) = (a * x) * y & a * (x + y) = (a * x) + (a * y) & (a + b) * x = (a * x) + (b * x) & (a * b) * x = a * (b * x) )
thus  x * (y + z) = (x * y) + (x * z) by Th15; ::_thesis: ( a * (x * y) = (a * x) * y & a * (x + y) = (a * x) + (a * y) & (a + b) * x = (a * x) + (b * x) & (a * b) * x = a * (b * x) )
thus  a * (x * y) = (a * x) * y by Th16; ::_thesis: ( a * (x + y) = (a * x) + (a * y) & (a + b) * x = (a * x) + (b * x) & (a * b) * x = a * (b * x) )
thus  a * (x + y) = (a * x) + (a * y) by Lm2; ::_thesis: ( (a + b) * x = (a * x) + (b * x) & (a * b) * x = a * (b * x) )
thus  (a + b) * x = (a * x) + (b * x) by Th14; ::_thesis: (a * b) * x = a * (b * x)
thus  (a * b) * x = a * (b * x) by Th13; ::_thesis: verum
end;

definition
let IT be non empty ComplexAlgebraStr ;
attrIT is vector-associative  means :: CFUNCDOM:def 9
 for x, y being Element of IT
for a being Element of COMPLEX holds a * (x * y) = (a * x) * y;
end;

:: deftheorem  defines vector-associative CFUNCDOM:def_9_:_
 for IT being non empty ComplexAlgebraStr holds
( IT is vector-associative iff for x, y being Element of IT
for a being Element of COMPLEX holds a * (x * y) = (a * x) * y );

registration
let A be non empty set ;
cluster CAlgebra A ->  right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative associative commutative right-distributive right_unital strict vector-associative ;
coherence
 ( CAlgebra A is strict & CAlgebra A is Abelian & CAlgebra A is add-associative & CAlgebra A is right_zeroed & CAlgebra A is right_complementable & CAlgebra A is commutative & CAlgebra A is associative & CAlgebra A is right_unital & CAlgebra A is right-distributive & CAlgebra A is vector-distributive & CAlgebra A is scalar-distributive & CAlgebra A is scalar-associative & CAlgebra A is vector-associative )
proof
set C = CAlgebra A;
thus  CAlgebra A is strict ; ::_thesis: ( CAlgebra A is Abelian & CAlgebra A is add-associative & CAlgebra A is right_zeroed & CAlgebra A is right_complementable & CAlgebra A is commutative & CAlgebra A is associative & CAlgebra A is right_unital & CAlgebra A is right-distributive & CAlgebra A is vector-distributive & CAlgebra A is scalar-distributive & CAlgebra A is scalar-associative & CAlgebra A is vector-associative )
thus  CAlgebra A is Abelian ::_thesis: ( CAlgebra A is add-associative & CAlgebra A is right_zeroed & CAlgebra A is right_complementable & CAlgebra A is commutative & CAlgebra A is associative & CAlgebra A is right_unital & CAlgebra A is right-distributive & CAlgebra A is vector-distributive & CAlgebra A is scalar-distributive & CAlgebra A is scalar-associative & CAlgebra A is vector-associative )
proof
let x, y be Element of (CAlgebra A); :: according to RLVECT_1:def_2 ::_thesis: x + y = y + x
thus  x + y = y + x by Th5; ::_thesis: verum
end;
thus  CAlgebra A is add-associative ::_thesis: ( CAlgebra A is right_zeroed & CAlgebra A is right_complementable & CAlgebra A is commutative & CAlgebra A is associative & CAlgebra A is right_unital & CAlgebra A is right-distributive & CAlgebra A is vector-distributive & CAlgebra A is scalar-distributive & CAlgebra A is scalar-associative & CAlgebra A is vector-associative )
proof
let x, y, z be Element of (CAlgebra A); :: according to RLVECT_1:def_3 ::_thesis: (x + y) + z = x + (y + z)
thus  (x + y) + z = x + (y + z) by Th6; ::_thesis: verum
end;
thus  CAlgebra A is right_zeroed ::_thesis: ( CAlgebra A is right_complementable & CAlgebra A is commutative & CAlgebra A is associative & CAlgebra A is right_unital & CAlgebra A is right-distributive & CAlgebra A is vector-distributive & CAlgebra A is scalar-distributive & CAlgebra A is scalar-associative & CAlgebra A is vector-associative )
proof
let x be Element of (CAlgebra A); :: according to RLVECT_1:def_4 ::_thesis: x + (0. (CAlgebra A)) = x
reconsider f = x as Element of Funcs (A,COMPLEX) ;
thus x + (0. (CAlgebra A)) = (ComplexFuncAdd A) . ((ComplexFuncZero A),f) by Th5
.= x by Th10 ; ::_thesis: verum
end;
thus  CAlgebra A is right_complementable ::_thesis: ( CAlgebra A is commutative & CAlgebra A is associative & CAlgebra A is right_unital & CAlgebra A is right-distributive & CAlgebra A is vector-distributive & CAlgebra A is scalar-distributive & CAlgebra A is scalar-associative & CAlgebra A is vector-associative )
proof
let x be Element of (CAlgebra A); :: according to ALGSTR_0:def_16 ::_thesis: x is right_complementable
reconsider f = x as Element of Funcs (A,COMPLEX) ;
reconsider t = (ComplexFuncExtMult A) . [(- 1r),f] as Element of (CAlgebra A) ;
take  t ; :: according to ALGSTR_0:def_11 ::_thesis: x + t = 0. (CAlgebra A)
thus  x + t = 0. (CAlgebra A) by Th11; ::_thesis: verum
end;
thus  CAlgebra A is commutative ::_thesis: ( CAlgebra A is associative & CAlgebra A is right_unital & CAlgebra A is right-distributive & CAlgebra A is vector-distributive & CAlgebra A is scalar-distributive & CAlgebra A is scalar-associative & CAlgebra A is vector-associative )
proof
let x, y be Element of (CAlgebra A); :: according to GROUP_1:def_12 ::_thesis: x * y = y * x
thus  x * y = y * x by Th7; ::_thesis: verum
end;
thus  CAlgebra A is associative ::_thesis: ( CAlgebra A is right_unital & CAlgebra A is right-distributive & CAlgebra A is vector-distributive & CAlgebra A is scalar-distributive & CAlgebra A is scalar-associative & CAlgebra A is vector-associative )
proof
let x, y, z be Element of (CAlgebra A); :: according to GROUP_1:def_3 ::_thesis: (x * y) * z = x * (y * z)
thus  (x * y) * z = x * (y * z) by Th8; ::_thesis: verum
end;
thus  CAlgebra A is right_unital ::_thesis: ( CAlgebra A is right-distributive & CAlgebra A is vector-distributive & CAlgebra A is scalar-distributive & CAlgebra A is scalar-associative & CAlgebra A is vector-associative )
proof
let x be Element of (CAlgebra A); :: according to VECTSP_1:def_4 ::_thesis: x * (1. (CAlgebra A)) = x
reconsider f = x as Element of Funcs (A,COMPLEX) ;
thus x * (1. (CAlgebra A)) = (ComplexFuncMult A) . ((ComplexFuncUnit A),f) by Th7
.= x by Th9 ; ::_thesis: verum
end;
thus  CAlgebra A is right-distributive ::_thesis: ( CAlgebra A is vector-distributive & CAlgebra A is scalar-distributive & CAlgebra A is scalar-associative & CAlgebra A is vector-associative )
proof
let x, y, z be Element of (CAlgebra A); :: according to VECTSP_1:def_2 ::_thesis: x * (y + z) = (x * y) + (x * z)
thus  x * (y + z) = (x * y) + (x * z) by Th15; ::_thesis: verum
end;
thus  CAlgebra A is vector-distributive ::_thesis: ( CAlgebra A is scalar-distributive & CAlgebra A is scalar-associative & CAlgebra A is vector-associative )
proof
let a be Complex; :: according to CLVECT_1:def_2 ::_thesis: for b1, b2 being Element of the carrier of (CAlgebra A) holds a * (b1 + b2) = (a * b1) + (a * b2)
let x, y be Element of (CAlgebra A); ::_thesis: a * (x + y) = (a * x) + (a * y)
thus  a * (x + y) = (a * x) + (a * y) by Lm2; ::_thesis: verum
end;
thus  CAlgebra A is scalar-distributive ::_thesis: ( CAlgebra A is scalar-associative & CAlgebra A is vector-associative )
proof
let a, b be Complex; :: according to CLVECT_1:def_3 ::_thesis: for b1 being Element of the carrier of (CAlgebra A) holds K110(a,b) * b1 = (a * b1) + (b * b1)
let x be Element of (CAlgebra A); ::_thesis: K110(a,b) * x = (a * x) + (b * x)
thus  (a + b) * x = (a * x) + (b * x) by Th14; ::_thesis: verum
end;
thus  CAlgebra A is scalar-associative ::_thesis: CAlgebra A is vector-associative
proof
let a, b be Complex; :: according to CLVECT_1:def_4 ::_thesis: for b1 being Element of the carrier of (CAlgebra A) holds K111(a,b) * b1 = a * (b * b1)
let x be Element of (CAlgebra A); ::_thesis: K111(a,b) * x = a * (b * x)
thus  a * (b * x) = (a * b) * x by Th13; ::_thesis: verum
end;
let x, y be Element of (CAlgebra A); :: according to CFUNCDOM:def_9 ::_thesis: for a being Element of COMPLEX holds a * (x * y) = (a * x) * y
let a be Element of COMPLEX ; ::_thesis: a * (x * y) = (a * x) * y
thus  a * (x * y) = (a * x) * y by Th16; ::_thesis: verum
end;
end;

registration
cluster non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative associative commutative right-distributive right_unital strict vector-associative for ComplexAlgebraStr ;
existence
 ex b1 being non empty ComplexAlgebraStr st
( b1 is strict & b1 is Abelian & b1 is add-associative & b1 is right_zeroed & b1 is right_complementable & b1 is commutative & b1 is associative & b1 is right_unital & b1 is right-distributive & b1 is vector-distributive & b1 is scalar-distributive & b1 is scalar-associative & b1 is vector-associative )
proof
take  CAlgebra 1 ; ::_thesis: ( CAlgebra 1 is strict & CAlgebra 1 is Abelian & CAlgebra 1 is add-associative & CAlgebra 1 is right_zeroed & CAlgebra 1 is right_complementable & CAlgebra 1 is commutative & CAlgebra 1 is associative & CAlgebra 1 is right_unital & CAlgebra 1 is right-distributive & CAlgebra 1 is vector-distributive & CAlgebra 1 is scalar-distributive & CAlgebra 1 is scalar-associative & CAlgebra 1 is vector-associative )
thus  ( CAlgebra 1 is strict & CAlgebra 1 is Abelian & CAlgebra 1 is add-associative & CAlgebra 1 is right_zeroed & CAlgebra 1 is right_complementable & CAlgebra 1 is commutative & CAlgebra 1 is associative & CAlgebra 1 is right_unital & CAlgebra 1 is right-distributive & CAlgebra 1 is vector-distributive & CAlgebra 1 is scalar-distributive & CAlgebra 1 is scalar-associative & CAlgebra 1 is vector-associative ) ; ::_thesis: verum
end;
end;

definition
mode ComplexAlgebra is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative associative commutative right-distributive right_unital vector-associative ComplexAlgebraStr ;
end;

theorem :: CFUNCDOM:27
for A being non empty set holds CAlgebra A is ComplexAlgebra ;

theorem :: CFUNCDOM:28
for A being non empty set holds 1. (CRing A) = ComplexFuncUnit A ;

theorem :: CFUNCDOM:29
for A being non empty set holds 1. (CAlgebra A) = ComplexFuncUnit A ;