reconsider G1 = G as RealLinearSpace-Sequence ;
A1: RLSStruct(# the carrier of (product G), the ZeroF of (product G), the addF of (product G), the Mult of (product G) #) = product G by Def13;

A2: now :: thesis: for v being VECTOR of (product G) holds 1 * v = v

let v be VECTOR of (product G); :: thesis: 1 * v = v
reconsider v1 = v as VECTOR of (product G1) by A1;
1 * v = 1 * v1 by A1;
hence 1 * v = v by RLVECT_1:def 8; :: thesis: verum

end;

A3: product G is right_complementable

proof

let v be VECTOR of (product G); :: according to ALGSTR_0:def 16 :: thesis: v is right_complementable
reconsider v1 = v as VECTOR of (product G1) by A1;
reconsider w = - v1 as VECTOR of (product G) by A1;
take w ; :: according to ALGSTR_0:def 11 :: thesis: v + w = 0. (product G)
v + w = v1 - v1 by A1;
then v + w = 0. (product G1) by RLVECT_1:15;
hence v + w = 0. (product G) by A1; :: thesis: verum

end;

A4: now :: thesis: for a being Real
for v, w being VECTOR of (product G) holds a * (v + w) = (a * v) + (a * w)

let a be Real; :: thesis: for v, w being VECTOR of (product G) holds a * (v + w) = (a * v) + (a * w)
let v, w be VECTOR of (product G); :: thesis: a * (v + w) = (a * v) + (a * w)
reconsider v1 = v, w1 = w as VECTOR of (product G1) by A1;
a * (v + w) = a * (v1 + w1) by A1;
then a * (v + w) = (a * v1) + (a * w1) by RLVECT_1:def 5;
hence a * (v + w) = (a * v) + (a * w) by A1; :: thesis: verum

end;

A5: now :: thesis: for a, b being Real
for v being VECTOR of (product G) holds (a * b) * v = a * (b * v)

let a, b be Real; :: thesis: for v being VECTOR of (product G) holds (a * b) * v = a * (b * v)
let v be VECTOR of (product G); :: thesis: (a * b) * v = a * (b * v)
reconsider v1 = v as VECTOR of (product G1) by A1;
(a * b) * v = (a * b) * v1 by A1;
then (a * b) * v = a * (b * v1) by RLVECT_1:def 7;
hence (a * b) * v = a * (b * v) by A1; :: thesis: verum

end;

A6: now :: thesis: for a, b being Real
for v being VECTOR of (product G) holds (a + b) * v = (a * v) + (b * v)

let a, b be Real; :: thesis: for v being VECTOR of (product G) holds (a + b) * v = (a * v) + (b * v)
let v be VECTOR of (product G); :: thesis: (a + b) * v = (a * v) + (b * v)
reconsider v1 = v as VECTOR of (product G1) by A1;
(a + b) * v = (a + b) * v1 by A1;
then (a + b) * v = (a * v1) + (b * v1) by RLVECT_1:def 6;
hence (a + b) * v = (a * v) + (b * v) by A1; :: thesis: verum

end;

A7: product G is add-associative

proof

let v, w, x be VECTOR of (product G); :: according to RLVECT_1:def 3 :: thesis: (v + w) + x = v + (w + x)
reconsider v1 = v, w1 = w, x1 = x as VECTOR of (product G1) by A1;
(v + w) + x = (v1 + w1) + x1 by A1;
then (v + w) + x = v1 + (w1 + x1) by RLVECT_1:def 3;
hence (v + w) + x = v + (w + x) by A1; :: thesis: verum

end;

A8: product G is Abelian

proof

let v, w be VECTOR of (product G); :: according to RLVECT_1:def 2 :: thesis: v + w = w + v
reconsider v1 = v, w1 = w as VECTOR of (product G1) by A1;
v + w = v1 + w1 by A1;
then v + w = w1 + v1 ;
hence v + w = w + v by A1; :: thesis: verum

end;

product G is right_zeroed

proof

let v be VECTOR of (product G); :: according to RLVECT_1:def 4 :: thesis: v + (0. (product G)) = v
reconsider v1 = v as VECTOR of (product G1) by A1;
v + (0. (product G)) = v1 + (0. (product G1)) by A1;
hence v + (0. (product G)) = v ; :: thesis: verum

end;

hence ( product G is reflexive & product G is discerning & product G is RealNormSpace-like & product G is vector-distributive & product G is scalar-distributive & product G is scalar-associative & product G is scalar-unital & product G is Abelian & product G is add-associative & product G is right_zeroed & product G is right_complementable ) by A8, A7, A3, A4, A6, A5, A2, Lm6; :: thesis: verum