let X be non empty RLSStruct ; :: thesis: for x being VECTOR of X
for u being VECTOR of (Prod_of_RLS X,RLS_Real )
for p, w being Real st u = [x,w] holds
p * u = [(p * x),(p * w)]
let x be VECTOR of X; :: thesis: for u being VECTOR of (Prod_of_RLS X,RLS_Real )
for p, w being Real st u = [x,w] holds
p * u = [(p * x),(p * w)]
let u be VECTOR of (Prod_of_RLS X,RLS_Real ); :: thesis: for p, w being Real st u = [x,w] holds
p * u = [(p * x),(p * w)]
let p, w be Real; :: thesis: ( u = [x,w] implies p * u = [(p * x),(p * w)] )
reconsider y = w as VECTOR of RLS_Real ;
A1: p * y = p * w by BINOP_2:def 11;
assume u = [x,w] ; :: thesis: p * u = [(p * x),(p * w)]
hence p * u = [(p * x),(p * w)] by A1, Def2; :: thesis: verum