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