let W be Normed_Complex_AlgebraStr ; for V being ComplexAlgebra st ComplexAlgebraStr(# the carrier of W, the multF of W, the addF of W, the Mult of W, the OneF of W, the ZeroF of W #) = V holds
W is ComplexAlgebra
let V be ComplexAlgebra; ( ComplexAlgebraStr(# the carrier of W, the multF of W, the addF of W, the Mult of W, the OneF of W, the ZeroF of W #) = V implies W is ComplexAlgebra )
assume A1:
ComplexAlgebraStr(# the carrier of W, the multF of W, the addF of W, the Mult of W, the OneF of W, the ZeroF of W #) = V
; W is ComplexAlgebra
reconsider W = W as non empty ComplexAlgebraStr by A1;
A2:
W is right_unital
A3:
W is right-distributive
A4:
for x being Element of W holds x is right_complementable
A6:
for a, b, x being Element of W holds (a * b) * x = a * (b * x)
A7:
for v, w being Element of W holds v * w = w * v
A8:
for x, y, z being VECTOR of W holds (x + y) + z = x + (y + z)
A9:
for x, y being VECTOR of W holds x + y = y + x
proof
let x,
y be
VECTOR of
W;
x + y = y + x
reconsider x1 =
x,
y1 =
y as
VECTOR of
V by A1;
x + y = x1 + y1
by A1;
then
x + y = y1 + x1
;
hence
x + y = y + x
by A1;
verum
end;
A10:
W is vector-distributive
A11:
W is scalar-distributive
A12:
W is scalar-associative
A13:
W is vector-associative
for x being VECTOR of W holds x + (0. W) = x
hence
W is ComplexAlgebra
by A9, A8, A4, A7, A6, A2, A3, A10, A11, A12, A13, ALGSTR_0:def 16, GROUP_1:def 3, GROUP_1:def 12, RLVECT_1:def 2, RLVECT_1:def 3, RLVECT_1:def 4; verum