let A be non empty set ; :: thesis: 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 & 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 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 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) )

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

for a, b being 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 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 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

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) )
reconsider mj = - 1r as Element of COMPLEX by XCMPLX_0:def 2;

set h = (ComplexFuncExtMult A) . [mj,f];

reconsider t = (ComplexFuncExtMult A) . [mj,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;set h = (ComplexFuncExtMult A) . [mj,f];

reconsider t = (ComplexFuncExtMult A) . [mj,f] as Element of (CAlgebra A) ;

take t ; :: thesis: x + t = 0. (CAlgebra A)

thus x + t = 0. (CAlgebra A) by Th11; :: thesis: verum

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