let X be RealLinearSpace-Sequence; :: thesis: for r being Element of REAL
for v being Element of product (carr X)
for i being Element of dom (carr X) holds
( ([:(multop X):] . (r,v)) . i = the Mult of (X . i) . (r,(v . i)) & ( for vi being VECTOR of (X . i) st vi = v . i holds
([:(multop X):] . (r,v)) . i = r * vi ) )
let r be Element of REAL ; :: thesis: for v being Element of product (carr X)
for i being Element of dom (carr X) holds
( ([:(multop X):] . (r,v)) . i = the Mult of (X . i) . (r,(v . i)) & ( for vi being VECTOR of (X . i) st vi = v . i holds
([:(multop X):] . (r,v)) . i = r * vi ) )
let v be Element of product (carr X); :: thesis: for i being Element of dom (carr X) holds
( ([:(multop X):] . (r,v)) . i = the Mult of (X . i) . (r,(v . i)) & ( for vi being VECTOR of (X . i) st vi = v . i holds
([:(multop X):] . (r,v)) . i = r * vi ) )
let i be Element of dom (carr X); :: thesis: ( ([:(multop X):] . (r,v)) . i = the Mult of (X . i) . (r,(v . i)) & ( for vi being VECTOR of (X . i) st vi = v . i holds
([:(multop X):] . (r,v)) . i = r * vi ) )
([:(multop X):] . (r,v)) . i = ((multop X) . i) . (r,(v . i)) by PRVECT_2:def 2;
hence ( ([:(multop X):] . (r,v)) . i = the Mult of (X . i) . (r,(v . i)) & ( for vi being VECTOR of (X . i) st vi = v . i holds
([:(multop X):] . (r,v)) . i = r * vi ) ) by PRVECT_2:def 8; :: thesis: verum