:: CFUNCDOM semantic presentation  Show TPTP formulae Show IDV graph for whole article:: Showing IDV graph ... (Click the Palm Trees again to close it)

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 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 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 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 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 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 Complex
for f being Element of Funcs A,COMPLEX
for x being Element of A holds (b1 . [z,f]) . x = z * (f . x)
proof end;
uniqueness
for b1, b2 being Function of [:COMPLEX ,(Funcs A,COMPLEX ):], Funcs A,COMPLEX st ( for z being 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 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 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 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 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
proof end;
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 end;

theorem Th1: :: CFUNCDOM:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

theorem Th2: :: CFUNCDOM:2  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

theorem Th3: :: CFUNCDOM:3  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being non empty set
for x being Element of A holds (ComplexFuncUnit A) . x = 1r by FUNCOP_1:13;

theorem Th4: :: CFUNCDOM:4  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being non empty set
for x being Element of A holds (ComplexFuncZero A) . x = 0 by FUNCOP_1:13;

theorem :: CFUNCDOM:5  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being non empty set holds ComplexFuncZero A <> ComplexFuncUnit A
proof end;

theorem Th6: :: CFUNCDOM:6  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being non empty set
for h, f being Element of Funcs A,COMPLEX
for a being Complex holds
( h = (ComplexFuncExtMult A) . [a,f] iff for x being Element of A holds h . x = a * (f . x) )
proof end;

theorem Th7: :: CFUNCDOM:7  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

theorem Th8: :: CFUNCDOM:8  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

theorem Th9: :: CFUNCDOM:9  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

theorem Th10: :: CFUNCDOM:10  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

theorem Th11: :: CFUNCDOM:11  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being non empty set
for f being Element of Funcs A,COMPLEX holds (ComplexFuncMult A) . (ComplexFuncUnit A),f = f
proof end;

theorem Th12: :: CFUNCDOM:12  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being non empty set
for f being Element of Funcs A,COMPLEX holds (ComplexFuncAdd A) . (ComplexFuncZero A),f = f
proof end;

theorem Th13: :: CFUNCDOM:13  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

theorem Th14: :: CFUNCDOM:14  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being non empty set
for f being Element of Funcs A,COMPLEX holds (ComplexFuncExtMult A) . [1r ,f] = f
proof end;

theorem Th15: :: CFUNCDOM:15  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

theorem Th16: :: CFUNCDOM:16  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 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 end;

theorem Th17: :: CFUNCDOM:17  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

theorem Th18: :: CFUNCDOM:18  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being non empty set
for f, g being Element of Funcs A,COMPLEX
for a being Complex holds (ComplexFuncMult A) . ((ComplexFuncExtMult A) . [a,f]),g = (ComplexFuncExtMult A) . [a,((ComplexFuncMult A) . f,g)]
proof end;

theorem Th19: :: CFUNCDOM:19  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

theorem Th20: :: CFUNCDOM:20  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 Complex st (ComplexFuncAdd A) . ((ComplexFuncExtMult A) . [a,f]),((ComplexFuncExtMult A) . [b,g]) = ComplexFuncZero A holds
( a = 0c & b = 0c )
proof end;

theorem :: CFUNCDOM:21  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 Complex st (ComplexFuncAdd A) . ((ComplexFuncExtMult A) . [a,f]),((ComplexFuncExtMult A) . [b,g]) = ComplexFuncZero A holds
( a = 0 & b = 0 )
proof end;

theorem Th22: :: CFUNCDOM:22  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 Complex st h = (ComplexFuncAdd A) . ((ComplexFuncExtMult A) . [a,f]),((ComplexFuncExtMult A) . [b,g])
proof end;

theorem :: CFUNCDOM:23  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 Complex st h = (ComplexFuncAdd A) . ((ComplexFuncExtMult A) . [a,f]),((ComplexFuncExtMult A) . [b,g])
proof end;

theorem Th24: :: CFUNCDOM:24  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 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 Complex st h = (ComplexFuncAdd A) . ((ComplexFuncExtMult A) . [a,f]),((ComplexFuncExtMult A) . [b,g]) ) )
proof end;

theorem Th25: :: CFUNCDOM:25  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being non empty set holds CLSStruct(# (Funcs A,COMPLEX ),(ComplexFuncZero A),(ComplexFuncAdd A),(ComplexFuncExtMult A) #) is ComplexLinearSpace
proof end;

definition
let A be non empty set ;
func ComplexVectSpace A -> strict ComplexLinearSpace 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 strict ComplexLinearSpace
by Th25;
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) #);

Lm3: ex A being non empty set ex x1, x2 being set st
( A = {x1,x2} & x1 <> x2 )
proof end;

theorem :: CFUNCDOM:26  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
ex V being strict ComplexLinearSpace ex u, v being VECTOR of V st
( ( for a, b being Complex st (a * u) + (b * v) = 0. V holds
( a = 0 & b = 0 ) ) & ( for w being VECTOR of V ex a, b being Complex st w = (a * u) + (b * v) ) )
proof end;

definition
let A be non empty set ;
func CRing A -> strict 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 strict 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
proof end;
end;

Lm4: for A being non empty set
for x, y being Element of (CRing A) holds x * y = y * x
by Th9;

Lm5: now
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 A1: e = ComplexFuncUnit A ; :: thesis: ( e * x = x & x * e = x )
reconsider a = x as Element of Funcs A,COMPLEX ;
thus A2: e * x = the mult of (CRing A) . e,x
.= (ComplexFuncMult A) . (ComplexFuncUnit A),a by A1
.= x by Th11 ; :: thesis: x * e = x
thus x * e = e * x by Lm4
.= x by A2 ; :: thesis: verum
end;

registration
let A be non empty set ;
cluster CRing A -> non empty unital strict ;
coherence
CRing A is unital
proof end;
end;

Lm6: now
let A be non empty set ; :: thesis: 1. (CRing A) = ComplexFuncUnit A
reconsider e = ComplexFuncUnit A as Element of (CRing A) ;
for x being Element of (CRing A) holds
( x * e = x & e * x = x ) by Lm5;
hence 1. (CRing A) = ComplexFuncUnit A by GROUP_1:def 5; :: thesis: verum
end;

theorem Th27: :: CFUNCDOM:27  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 & ex t being Element of (CRing A) st x + t = 0. (CRing A) & 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 end;

theorem :: CFUNCDOM:28  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being non empty set holds CRing A is commutative Ring
proof end;

definition
attr c1 is strict;
struct ComplexAlgebraStr -> doubleLoopStr , CLSStruct ;
aggr ComplexAlgebraStr(# carrier, mult, add, Mult, unity, Zero #) -> ComplexAlgebraStr ;
end;

registration
cluster non empty ComplexAlgebraStr ;
existence
not for b1 being ComplexAlgebraStr holds b1 is empty
proof 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 end;
end;

Lm7: for A being non empty set
for x, y being Element of (CAlgebra A) holds x * y = y * x
by Th9;

Lm8: now
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 A1: e = ComplexFuncUnit A ; :: thesis: ( e * x = x & x * e = x )
reconsider a = x as Element of Funcs A,COMPLEX ;
thus A2: e * x = the mult of (CAlgebra A) . e,x
.= (ComplexFuncMult A) . (ComplexFuncUnit A),a by A1
.= x by Th11 ; :: thesis: x * e = x
thus x * e = e * x by Lm7
.= x by A2 ; :: thesis: verum
end;

registration
let A be non empty set ;
cluster CAlgebra A -> non empty unital strict ;
coherence
CAlgebra A is unital
proof end;
end;

Lm9: now
let A be non empty set ; :: thesis: 1. (CAlgebra A) = ComplexFuncUnit A
reconsider e = ComplexFuncUnit A as Element of (CAlgebra A) ;
for x being Element of (CAlgebra A) holds
( x * e = x & e * x = x ) by Lm8;
hence 1. (CAlgebra A) = ComplexFuncUnit A by GROUP_1:def 5; :: thesis: verum
end;

theorem Th29: :: CFUNCDOM:29  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being non empty set
for x, y, z being Element of (CAlgebra A)
for a, b being Complex holds
( x + y = y + x & (x + y) + z = x + (y + z) & x + (0. (CAlgebra A)) = x & ex t being Element of (CAlgebra A) st x + t = 0. (CAlgebra A) & 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 end;

definition
let IT be non empty ComplexAlgebraStr ;
attr IT is ComplexAlgebra-like means :Def9: :: CFUNCDOM:def 9
for x, y, z being Element of IT
for a, b being Complex holds
( x * (1. IT) = 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) );
end;

:: deftheorem Def9 defines ComplexAlgebra-like CFUNCDOM:def 9 :
for IT being non empty ComplexAlgebraStr holds
( IT is ComplexAlgebra-like iff for x, y, z being Element of IT
for a, b being Complex holds
( x * (1. IT) = 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) ) );

registration
cluster non empty Abelian add-associative right_zeroed right_complementable associative commutative strict ComplexAlgebra-like 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 ComplexAlgebra-like )
proof end;
end;

definition
mode ComplexAlgebra is non empty Abelian add-associative right_zeroed right_complementable associative commutative ComplexAlgebra-like ComplexAlgebraStr ;
end;

theorem :: CFUNCDOM:30  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being non empty set holds CAlgebra A is ComplexAlgebra
proof end;

theorem :: CFUNCDOM:31  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being non empty set holds 1. (CRing A) = ComplexFuncUnit A by Lm6;

theorem :: CFUNCDOM:32  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being non empty set holds 1. (CAlgebra A) = ComplexFuncUnit A by Lm9;