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;

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

A3:
product G is right_complementable
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;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

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;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

A4: now :: thesis: for a being Real

for v, w being VECTOR of (product G) holds a * (v + w) = (a * v) + (a * w)

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;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

A5: now :: thesis: for a, b being Real

for v being VECTOR of (product G) holds (a * b) * v = a * (b * v)

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;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

A6: now :: thesis: for a, b being Real

for v being VECTOR of (product G) holds (a + b) * v = (a * v) + (b * v)

A7:
product G is add-associative
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;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

proof

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

proof

product G is right_zeroed
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;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

proof

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
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;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