let W be Normed_AlgebraStr ; for V being Algebra st AlgebraStr(# 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 Algebra
let V be Algebra; ( AlgebraStr(# 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 Algebra )
assume A1:
AlgebraStr(# 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 Algebra
reconsider W = W as non empty AlgebraStr by A1;
A2:
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;
A3:
for x, y, z being VECTOR of W holds (x + y) + z = x + (y + z)
A4:
for x being VECTOR of W holds x + (0. W) = x
A5:
for x being Element of W holds x is right_complementable
A7:
for v, w being Element of W holds v * w = w * v
A8:
for a, b, x being Element of W holds (a * b) * x = a * (b * x)
A9:
W is right_unital
A10:
W is right-distributive
( W is vector-distributive & W is scalar-distributive & W is scalar-associative & W is vector-associative )
hence
W is Algebra
by A2, A3, A4, A5, A7, A8, A9, A10, 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