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 by XREAL_0:def 1;
reconsider y2 = w2 as VECTOR of RLS_Real by XREAL_0:def 1;
assume that
A1: u1 = [x1,w1] and
A2: u2 = [x2,w2] ; :: thesis: u1 + u2 = [(x1 + x2),(w1 + w2)]
y1 + y2 = w1 + w2 by BINOP_2:def 9;
hence u1 + u2 = [(x1 + x2),(w1 + w2)] by A1, A2, Def1; :: thesis: verum