for u1, u2 being Element of (Prod_of_RLS X,Y) holds u1 + u2 = u2 + u1
proof
let u1,
u2 be
Element of
(Prod_of_RLS X,Y);
:: thesis: u1 + u2 = u2 + u1
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;
u1 + u2 = [(x2 + x1),(y2 + y1)]
by A2, A4, Th2;
hence
u1 + u2 = u2 + u1
by A2, A4, Def1;
:: thesis: verum
end;
hence
Prod_of_RLS X,Y is Abelian
by RLVECT_1:def 5; :: thesis: verum