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

proof

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

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;

consider x3, y3 being object such that

A4: x3 in the carrier of X and

A5: y3 in the carrier of Y and

A6: u3 = [x3,y3] by ZFMISC_1:def 2;

reconsider y3 = y3 as VECTOR of Y by A5;

reconsider x3 = x3 as VECTOR of X by A4;

reconsider x1 = x1 as VECTOR of X by A1;

consider x2, y2 being object such that

A7: x2 in the carrier of X and

A8: y2 in the carrier of Y and

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

reconsider y2 = y2 as VECTOR of Y by A8;

reconsider x2 = x2 as VECTOR of X by A7;

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

then A10: (u1 + u2) + u3 = [((x1 + x2) + x3),((y1 + y2) + y3)] by A6, Def1;

u2 + u3 = [(x2 + x3),(y2 + y3)] by A9, A6, Def1;

then A11: u1 + (u2 + u3) = [(x1 + (x2 + x3)),(y1 + (y2 + y3))] by A3, Def1;

(x1 + x2) + x3 = x1 + (x2 + x3) by RLVECT_1:def 3;

hence (u1 + u2) + u3 = u1 + (u2 + u3) by A10, A11, RLVECT_1:def 3; :: 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;

consider x3, y3 being object such that

A4: x3 in the carrier of X and

A5: y3 in the carrier of Y and

A6: u3 = [x3,y3] by ZFMISC_1:def 2;

reconsider y3 = y3 as VECTOR of Y by A5;

reconsider x3 = x3 as VECTOR of X by A4;

reconsider x1 = x1 as VECTOR of X by A1;

consider x2, y2 being object such that

A7: x2 in the carrier of X and

A8: y2 in the carrier of Y and

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

reconsider y2 = y2 as VECTOR of Y by A8;

reconsider x2 = x2 as VECTOR of X by A7;

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

then A10: (u1 + u2) + u3 = [((x1 + x2) + x3),((y1 + y2) + y3)] by A6, Def1;

u2 + u3 = [(x2 + x3),(y2 + y3)] by A9, A6, Def1;

then A11: u1 + (u2 + u3) = [(x1 + (x2 + x3)),(y1 + (y2 + y3))] by A3, Def1;

(x1 + x2) + x3 = x1 + (x2 + x3) by RLVECT_1:def 3;

hence (u1 + u2) + u3 = u1 + (u2 + u3) by A10, A11, RLVECT_1:def 3; :: thesis: verum