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

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