let X be non empty RLSStruct ; :: thesis: for x1, x2 being VECTOR of X
for w1, w2 being Real
for u1, u2 being VECTOR of (Prod_of_RLS X,RLS_Real ) st u1 = [x1,w1] & u2 = [x2,w2] holds
u1 + u2 = [(x1 + x2),(w1 + w2)]
let x1, x2 be VECTOR of X; :: thesis: for w1, w2 being Real
for u1, u2 being VECTOR of (Prod_of_RLS X,RLS_Real ) st u1 = [x1,w1] & u2 = [x2,w2] holds
u1 + u2 = [(x1 + x2),(w1 + w2)]
let w1, w2 be Real; :: thesis: for u1, u2 being VECTOR of (Prod_of_RLS X,RLS_Real ) st u1 = [x1,w1] & u2 = [x2,w2] holds
u1 + u2 = [(x1 + x2),(w1 + w2)]
let u1, u2 be VECTOR of (Prod_of_RLS X,RLS_Real ); :: thesis: ( u1 = [x1,w1] & u2 = [x2,w2] implies u1 + u2 = [(x1 + x2),(w1 + w2)] )
reconsider y1 = w1 as VECTOR of RLS_Real ;
reconsider y2 = w2 as VECTOR of RLS_Real ;
A1: y1 + y2 = w1 + w2 by BINOP_2:def 9;
assume ( u1 = [x1,w1] & u2 = [x2,w2] ) ; :: thesis: u1 + u2 = [(x1 + x2),(w1 + w2)]
hence u1 + u2 = [(x1 + x2),(w1 + w2)] by A1, Def1; :: thesis: verum