for u1, u2 being Element of (Prod_of_RLS (X,Y)) holds u1 + u2 = u2 + u1

proof

hence
Prod_of_RLS (X,Y) is Abelian
; :: thesis: verum
let u1, u2 be Element of (Prod_of_RLS (X,Y)); :: thesis: u1 + u2 = u2 + u1

consider x1, y1 being object such that

A1: x1 in the carrier of X and

A2: y1 in the carrier of Y and

A3: u1 = [x1,y1] by ZFMISC_1:def 2;

reconsider y1 = y1 as VECTOR of Y by A2;

reconsider x1 = x1 as VECTOR of X by A1;

consider x2, y2 being object such that

A4: x2 in the carrier of X and

A5: y2 in the carrier of Y and

A6: u2 = [x2,y2] by ZFMISC_1:def 2;

reconsider y2 = y2 as VECTOR of Y by A5;

reconsider x2 = x2 as VECTOR of X by A4;

u1 + u2 = [(x2 + x1),(y2 + y1)] by A3, A6, Th2;

hence u1 + u2 = u2 + u1 by A3, A6, Def1; :: thesis: verum

end;consider x1, y1 being object such that

A1: x1 in the carrier of X and

A2: y1 in the carrier of Y and

A3: u1 = [x1,y1] by ZFMISC_1:def 2;

reconsider y1 = y1 as VECTOR of Y by A2;

reconsider x1 = x1 as VECTOR of X by A1;

consider x2, y2 being object such that

A4: x2 in the carrier of X and

A5: y2 in the carrier of Y and

A6: u2 = [x2,y2] by ZFMISC_1:def 2;

reconsider y2 = y2 as VECTOR of Y by A5;

reconsider x2 = x2 as VECTOR of X by A4;

u1 + u2 = [(x2 + x1),(y2 + y1)] by A3, A6, Th2;

hence u1 + u2 = u2 + u1 by A3, A6, Def1; :: thesis: verum