let W be Normed_AlgebraStr ; :: thesis: for V being Algebra st AlgebraStr(# the carrier of W,the multF of W,the addF of W,the Mult of W,the U3 of W,the U2 of W #) = V holds
W is Algebra
let V be Algebra; :: thesis: ( AlgebraStr(# the carrier of W,the multF of W,the addF of W,the Mult of W,the U3 of W,the U2 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 U3 of W,the U2 of W #) = V ; :: thesis: W is Algebra
reconsider W = W as non empty AlgebraStr by A1;
L1: for x, y being VECTOR of holds x + y = y + x

proof

let x, y be VECTOR of ; :: thesis: x + y = y + x
reconsider x1 = x, y1 = y as VECTOR of by A1;
x + y = x1 + y1 by A1;
then x + y = y1 + x1 ;
hence x + y = y + x by A1; :: thesis: verum

end;

L2: for x, y, z being VECTOR of holds (x + y) + z = x + (y + z)

proof

let x, y, z be VECTOR of ; :: thesis: (x + y) + z = x + (y + z)
reconsider x1 = x, y1 = y, z1 = z as VECTOR of by A1;
(x + y) + z = (x1 + y1) + z1 by A1;
then (x + y) + z = x1 + (y1 + z1) by RLVECT_1:def 6;
hence (x + y) + z = x + (y + z) by A1; :: thesis: verum

end;

L3: for x being VECTOR of holds x + (0. W) = x

proof

let x be VECTOR of ; :: thesis: x + (0. W) = x
reconsider y = x, z = 0. W as VECTOR of by A1;
x + (0. W) = y + (0. V) by A1;
hence x + (0. W) = x by RLVECT_1:10; :: thesis: verum

end;

L4: for x being Element of holds x is right_complementable

proof

let x be Element of ; :: thesis: x is right_complementable
reconsider x1 = x as Element of by A1;
consider v being Element of such that
A2: x1 + v = 0. V by ALGSTR_0:def 11;
reconsider y = v as Element of by A1;
x + y = 0. W by A2, A1;
hence x is right_complementable by ALGSTR_0:def 11; :: thesis: verum

end;

L5: for v, w being Element of holds v * w = w * v

proof

let v, w be Element of ; :: thesis: v * w = w * v
reconsider v1 = v, w1 = w as Element of by A1;
v * w = v1 * w1 by A1;
then v * w = w1 * v1 ;
hence v * w = w * v by A1; :: thesis: verum

end;

L6: for a, b, x being Element of holds (a * b) * x = a * (b * x)

proof

let a, b, x be Element of ; :: thesis: (a * b) * x = a * (b * x)
reconsider y = x, a1 = a, b1 = b as Element of by A1;
(a * b) * x = (a1 * b1) * y by A1;
then (a * b) * x = a1 * (b1 * y) by GROUP_1:def 4;
hence (a * b) * x = a * (b * x) by A1; :: thesis: verum

end;

L7: W is right_unital

proof

let x be Element of ; :: according to VECTSP_1:def 13 :: thesis: x * (1. W) = x
reconsider x1 = x as Element of by A1;
x * (1. W) = x1 * (1. V) by A1;
hence x * (1. W) = x by VECTSP_1:def 13; :: thesis: verum

end;

L8: W is right-distributive

proof

let x, y, z be Element of ; :: according to VECTSP_1:def 11 :: thesis: x * (y + z) = (x * y) + (x * z)
reconsider x1 = x, y1 = y, z1 = z as Element of by A1;
x * (y + z) = x1 * (y1 + z1) by A1;
then x * (y + z) = (x1 * y1) + (x1 * z1) by VECTSP_1:def 11;
hence x * (y + z) = (x * y) + (x * z) by A1; :: thesis: verum

end;

W is Algebra-like

proof

let x, y, z be Element of ; :: according to FUNCSDOM:def 20 :: thesis: for b₁, b₂ being Element of REAL holds
( b₁ * (x * y) = (b₁ * x) * y & b₁ * (x + y) = (b₁ * x) + (b₁ * y) & (b₁ + b₂) * x = (b₁ * x) + (b₂ * x) & (b₁ * b₂) * x = b₁ * (b₂ * x) )
let a, b be Real; :: thesis: ( a * (x * y) = (a * x) * y & a * (x + y) = (a * x) + (a * y) & (a + b) * x = (a * x) + (b * x) & (a * b) * x = a * (b * x) )
reconsider x1 = x, y1 = y, z1 = z as Element of by A1;
a * (x * y) = a * (x1 * y1) by A1;
then a * (x * y) = (a * x1) * y1 by FUNCSDOM:def 20;
hence a * (x * y) = (a * x) * y by A1; :: thesis: ( a * (x + y) = (a * x) + (a * y) & (a + b) * x = (a * x) + (b * x) & (a * b) * x = a * (b * x) )
a * (x + y) = a * (x1 + y1) by A1;
then a * (x + y) = (a * x1) + (a * y1) by FUNCSDOM:def 20;
hence a * (x + y) = (a * x) + (a * y) by A1; :: thesis: ( (a + b) * x = (a * x) + (b * x) & (a * b) * x = a * (b * x) )
(a + b) * x = (a + b) * x1 by A1;
then (a + b) * x = (a * x1) + (b * x1) by FUNCSDOM:def 20;
hence (a + b) * x = (a * x) + (b * x) by A1; :: thesis: (a * b) * x = a * (b * x)
(a * b) * x = (a * b) * x1 by A1;
then (a * b) * x = a * (b * x1) by FUNCSDOM:def 20;
hence (a * b) * x = a * (b * x) by A1; :: thesis: verum

end;

hence W is Algebra by L1, L2, L3, L4, L5, L6, L7, L8, RLVECT_1:def 5, RLVECT_1:def 6, RLVECT_1:def 7, ALGSTR_0:def 16, GROUP_1:def 4, GROUP_1:def 16; :: thesis: verum