let K be Ring; :: thesis: for G being VectorSpace-Sequence of K

for r being Element of K

for v being Element of product (carr G)

for i being Element of dom (carr G) holds

( ([:(multop G):] . (r,v)) . i = the lmult 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 G be VectorSpace-Sequence of K; :: thesis: for r being Element of K

for v being Element of product (carr G)

for i being Element of dom (carr G) holds

( ([:(multop G):] . (r,v)) . i = the lmult 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 Element of K; :: thesis: for v being Element of product (carr G)

for i being Element of dom (carr G) holds

( ([:(multop G):] . (r,v)) . i = the lmult 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 lmult 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 lmult 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 PRVECT_2:def 2;

hence ( ([:(multop G):] . (r,v)) . i = the lmult 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

for r being Element of K

for v being Element of product (carr G)

for i being Element of dom (carr G) holds

( ([:(multop G):] . (r,v)) . i = the lmult 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 G be VectorSpace-Sequence of K; :: thesis: for r being Element of K

for v being Element of product (carr G)

for i being Element of dom (carr G) holds

( ([:(multop G):] . (r,v)) . i = the lmult 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 Element of K; :: thesis: for v being Element of product (carr G)

for i being Element of dom (carr G) holds

( ([:(multop G):] . (r,v)) . i = the lmult 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 lmult 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 lmult 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 PRVECT_2:def 2;

hence ( ([:(multop G):] . (r,v)) . i = the lmult 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