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 by Th5; :: 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 )

thus CAlgebra A is add-associative by Th6; :: 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 )

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 )

thus CAlgebra A is associative by Th8; :: 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 )

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 )

thus CAlgebra A is vector-distributive by Lm2; :: thesis: ( CAlgebra A is scalar-distributive & CAlgebra A is scalar-associative & CAlgebra A is vector-associative )

thus CAlgebra A is scalar-distributive by Th14; :: thesis: ( CAlgebra A is scalar-associative & CAlgebra A is vector-associative )

thus CAlgebra A is scalar-associative by Th13; :: thesis: CAlgebra A is vector-associative

let x, y be Element of (CAlgebra A); :: according to CFUNCDOM:def 9 :: thesis: for a being Complex holds a * (x * y) = (a * x) * y

let a be Complex; :: thesis: a * (x * y) = (a * x) * y

thus a * (x * y) = (a * x) * y by Th16; :: thesis: verum

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 by Th5; :: 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 )

thus CAlgebra A is add-associative by Th6; :: 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 )

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

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 )
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;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

proof

thus
CAlgebra A is commutative
by Th7; :: 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 )
let x be Element of (CAlgebra A); :: according to ALGSTR_0:def 16 :: thesis: x is right_complementable

reconsider mj = - 1r as Element of COMPLEX by XCMPLX_0:def 2;

reconsider f = x as Element of Funcs (A,COMPLEX) ;

reconsider t = (ComplexFuncExtMult A) . [mj,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;reconsider mj = - 1r as Element of COMPLEX by XCMPLX_0:def 2;

reconsider f = x as Element of Funcs (A,COMPLEX) ;

reconsider t = (ComplexFuncExtMult A) . [mj,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

thus CAlgebra A is associative by Th8; :: 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 )

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

thus
CAlgebra A is right-distributive
by Th15; :: thesis: ( CAlgebra A is vector-distributive & CAlgebra A is scalar-distributive & CAlgebra A is scalar-associative & CAlgebra A is vector-associative )
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;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

thus CAlgebra A is vector-distributive by Lm2; :: thesis: ( CAlgebra A is scalar-distributive & CAlgebra A is scalar-associative & CAlgebra A is vector-associative )

thus CAlgebra A is scalar-distributive by Th14; :: thesis: ( CAlgebra A is scalar-associative & CAlgebra A is vector-associative )

thus CAlgebra A is scalar-associative by Th13; :: thesis: CAlgebra A is vector-associative

let x, y be Element of (CAlgebra A); :: according to CFUNCDOM:def 9 :: thesis: for a being Complex holds a * (x * y) = (a * x) * y

let a be Complex; :: thesis: a * (x * y) = (a * x) * y

thus a * (x * y) = (a * x) * y by Th16; :: thesis: verum