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: product G is Abelian

proof

let v, w be VECTOR of (product G); :: according to RLVECT_1:def 5 :: 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;

A3: product G is add-associative

proof

let v, w, x be VECTOR of (product G); :: according to RLVECT_1:def 6 :: 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 6;
hence (v + w) + x = v + (w + x) by A1; :: thesis: verum

end;

A4: product G is right_zeroed

proof

let v be VECTOR of (product G); :: according to RLVECT_1:def 7 :: 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 by RLVECT_1:def 7; :: thesis: verum

end;

A5: 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:28;
hence v + w = 0. (product G) by A1; :: thesis: verum

end;

product G is RealLinearSpace-like

proof

A6: now

let a be real number ; :: 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 9;
hence a * (v + w) = (a * v) + (a * w) by A1; :: thesis: verum

end;

A7: now

let a, b be real number ; :: 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 9;
hence (a + b) * v = (a * v) + (b * v) by A1; :: thesis: verum

end;

A8: now

let a, b be real number ; :: 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 9;
hence (a * b) * v = a * (b * v) by A1; :: thesis: verum

end;

now

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

end;

hence product G is RealLinearSpace-like by A6, A7, A8, RLVECT_1:def 9; :: thesis: verum

end;

hence ( product G is RealNormSpace-like & product G is RealLinearSpace-like & product G is Abelian & product G is add-associative & product G is right_zeroed & product G is right_complementable ) by A2, A3, A4, A5, Lm7; :: thesis: verum