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 by XREAL_0:def 1;
assume A1: u = [x,w] ; :: thesis: p * u = [(p * x),(p * w)]
p * y = p * w by BINOP_2:def 11;
hence p * u = [(p * x),(p * w)] by A1, Def2; :: thesis: verum