set C = CAlgebra A;
thus CAlgebra A is strict ; :: thesis:
thus CAlgebra A is Abelian by Th5; :: thesis:
thus CAlgebra A is add-associative by Th6; :: thesis:
thus CAlgebra A is right_zeroed :: thesis:

proof

let x be Element of (CAlgebra A); :: according to RLVECT_1:def 4 :: thesis:
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:

end;

thus CAlgebra A is right_complementable :: thesis:

proof

let x be Element of (CAlgebra A); :: according to ALGSTR_0:def 16 :: thesis:
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:
thus x + t = 0. (CAlgebra A) by Th11; :: thesis:

end;

thus CAlgebra A is commutative by Th7; :: thesis:
thus CAlgebra A is associative by Th8; :: thesis:
thus CAlgebra A is right_unital :: thesis:

proof

let x be Element of (CAlgebra A); :: according to VECTSP_1:def 4 :: thesis:
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:

end;

thus CAlgebra A is right-distributive by Th15; :: thesis:
thus CAlgebra A is vector-distributive by Lm2; :: thesis:
thus CAlgebra A is scalar-distributive by Th14; :: thesis:
thus CAlgebra A is scalar-associative by Th13; :: thesis:
let x, y be Element of (CAlgebra A); :: according to CFUNCDOM:def 9 :: thesis:
let a be Complex; :: thesis:
thus a * (x * y) = (a * x) * y by Th16; :: thesis: