reconsider G1 = G as RealLinearSpace-Sequence ;
A1: RLSStruct(# the carrier of (), the ZeroF of (), the addF of (), the Mult of () #) = product G by Def13;
A2: now :: thesis: for v being VECTOR of () holds 1 * v = v
let v be VECTOR of (); :: 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 (); :: according to ALGSTR_0:def 16 :: thesis:
reconsider v1 = v as VECTOR of (product G1) by A1;
reconsider w = - v1 as VECTOR of () by A1;
take w ; :: according to ALGSTR_0:def 11 :: thesis: v + w = 0. ()
v + w = v1 - v1 by A1;
then v + w = 0. (product G1) by RLVECT_1:15;
hence v + w = 0. () by A1; :: thesis: verum
end;
A4: now :: thesis: for a being Real
for v, w being VECTOR of () holds a * (v + w) = (a * v) + (a * w)
let a be Real; :: thesis: for v, w being VECTOR of () holds a * (v + w) = (a * v) + (a * w)
let v, w be VECTOR of (); :: 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 () holds (a * b) * v = a * (b * v)
let a, b be Real; :: thesis: for v being VECTOR of () holds (a * b) * v = a * (b * v)
let v be VECTOR of (); :: 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 () holds (a + b) * v = (a * v) + (b * v)
let a, b be Real; :: thesis: for v being VECTOR of () holds (a + b) * v = (a * v) + (b * v)
let v be VECTOR of (); :: 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;
proof
let v, w, x be VECTOR of (); :: 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 (); :: 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 (); :: according to RLVECT_1:def 4 :: thesis: v + (0. ()) = v
reconsider v1 = v as VECTOR of (product G1) by A1;
v + (0. ()) = v1 + (0. (product G1)) by A1;
hence v + (0. ()) = 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