for u1, u2, u3 being Element of (Prod_of_RLS X,Y) holds (u1 + u2) + u3 = u1 + (u2 + u3)
proof
let u1,
u2,
u3 be
Element of
(Prod_of_RLS X,Y);
:: thesis: (u1 + u2) + u3 = u1 + (u2 + u3)
consider x1,
y1 being
set such that A1:
(
x1 in the
carrier of
X &
y1 in the
carrier of
Y )
and A2:
u1 = [x1,y1]
by ZFMISC_1:def 2;
reconsider x1 =
x1 as
VECTOR of
X by A1;
reconsider y1 =
y1 as
VECTOR of
Y by A1;
consider x2,
y2 being
set such that A3:
(
x2 in the
carrier of
X &
y2 in the
carrier of
Y )
and A4:
u2 = [x2,y2]
by ZFMISC_1:def 2;
reconsider x2 =
x2 as
VECTOR of
X by A3;
reconsider y2 =
y2 as
VECTOR of
Y by A3;
consider x3,
y3 being
set such that A5:
(
x3 in the
carrier of
X &
y3 in the
carrier of
Y )
and A6:
u3 = [x3,y3]
by ZFMISC_1:def 2;
reconsider x3 =
x3 as
VECTOR of
X by A5;
reconsider y3 =
y3 as
VECTOR of
Y by A5;
(
u1 + u2 = [(x1 + x2),(y1 + y2)] &
u2 + u3 = [(x2 + x3),(y2 + y3)] )
by A2, A4, A6, Def1;
then A7:
(
(u1 + u2) + u3 = [((x1 + x2) + x3),((y1 + y2) + y3)] &
u1 + (u2 + u3) = [(x1 + (x2 + x3)),(y1 + (y2 + y3))] )
by A2, A6, Def1;
(
(x1 + x2) + x3 = x1 + (x2 + x3) &
(y1 + y2) + y3 = y1 + (y2 + y3) )
by RLVECT_1:def 6;
hence
(u1 + u2) + u3 = u1 + (u2 + u3)
by A7;
:: thesis: verum
end;
hence
Prod_of_RLS X,Y is add-associative
by RLVECT_1:def 6; :: thesis: verum