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

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