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 5 :: thesis: x + y = y + x
thus x + y = y + x by Th7; :: 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 6 :: thesis: (x + y) + z = x + (y + z)
thus (x + y) + z = x + (y + z) by Th8; :: 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 7 :: 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 Th7
.= x by Th12 ; :: 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 Th13; :: 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 16 :: thesis: x * y = y * x
thus x * y = y * x by Th9; :: 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 4 :: thesis: (x * y) * z = x * (y * z)
thus (x * y) * z = x * (y * z) by Th10; :: 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 13 :: 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 Th9
.= x by Th11 ; :: 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 11 :: thesis: x * (y + z) = (x * y) + (x * z)
thus x * (y + z) = (x * y) + (x * z) by Th17; :: 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 b₁, b₂ being Element of the carrier of (CAlgebra A) holds a * (b₁ + b₂) = (a * b₁) + (a * b₂)
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 be Complex; :: according to CLVECT_1:def 3 :: thesis: for b₁ being Element of COMPLEX
for b₂ being Element of the carrier of (CAlgebra A) holds (a + b₁) * b₂ = (a * b₂) + (b₁ * b₂)
let b be Complex; :: thesis: for b₁ being Element of the carrier of (CAlgebra A) holds (a + b) * b₁ = (a * b₁) + (b * b₁)
let x be Element of (CAlgebra A); :: thesis: (a + b) * x = (a * x) + (b * x)
thus (a + b) * x = (a * x) + (b * x) by Th16; :: thesis: verum

end;

thus CAlgebra A is scalar-associative :: thesis: CAlgebra A is vector-associative

proof

let a be Complex; :: according to CLVECT_1:def 4 :: thesis: for b₁ being Element of COMPLEX
for b₂ being Element of the carrier of (CAlgebra A) holds (a * b₁) * b₂ = a * (b₁ * b₂)
let b be Complex; :: thesis: for b₁ being Element of the carrier of (CAlgebra A) holds (a * b) * b₁ = a * (b * b₁)
let x be Element of (CAlgebra A); :: thesis: (a * b) * x = a * (b * x)
thus a * (b * x) = (a * b) * x by Th15; :: thesis: verum

end;

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 Th18; :: thesis: verum