let G be RealLinearSpace-Sequence; :: thesis: for r being Element of REAL
for v being Element of product (carr G)
for i being Element of dom (carr G) holds
( ([:():] . (r,v)) . i = the Mult of (G . i) . (r,(v . i)) & ( for vi being VECTOR of (G . i) st vi = v . i holds
([:():] . (r,v)) . i = r * vi ) )

let r be Element of REAL ; :: thesis: for v being Element of product (carr G)
for i being Element of dom (carr G) holds
( ([:():] . (r,v)) . i = the Mult of (G . i) . (r,(v . i)) & ( for vi being VECTOR of (G . i) st vi = v . i holds
([:():] . (r,v)) . i = r * vi ) )

let v be Element of product (carr G); :: thesis: for i being Element of dom (carr G) holds
( ([:():] . (r,v)) . i = the Mult of (G . i) . (r,(v . i)) & ( for vi being VECTOR of (G . i) st vi = v . i holds
([:():] . (r,v)) . i = r * vi ) )

let i be Element of dom (carr G); :: thesis: ( ([:():] . (r,v)) . i = the Mult of (G . i) . (r,(v . i)) & ( for vi being VECTOR of (G . i) st vi = v . i holds
([:():] . (r,v)) . i = r * vi ) )

([:():] . (r,v)) . i = (() . i) . (r,(v . i)) by Def2;
hence ( ([:():] . (r,v)) . i = the Mult of (G . i) . (r,(v . i)) & ( for vi being VECTOR of (G . i) st vi = v . i holds
([:():] . (r,v)) . i = r * vi ) ) by Def8; :: thesis: verum