A1:
for a being real number
for u1, u2 being VECTOR of (Prod_of_RLS X,Y) holds a * (u1 + u2) = (a * u1) + (a * u2)
proof
let a be
real number ;
:: thesis: for u1, u2 being VECTOR of (Prod_of_RLS X,Y) holds a * (u1 + u2) = (a * u1) + (a * u2)
reconsider a =
a as
Real by XREAL_0:def 1;
let u1,
u2 be
VECTOR of
(Prod_of_RLS X,Y);
:: thesis: a * (u1 + u2) = (a * u1) + (a * u2)
consider x1,
y1 being
set such that A2:
(
x1 in the
carrier of
X &
y1 in the
carrier of
Y )
and A3:
u1 = [x1,y1]
by ZFMISC_1:def 2;
reconsider x1 =
x1 as
VECTOR of
X by A2;
reconsider y1 =
y1 as
VECTOR of
Y by A2;
consider x2,
y2 being
set such that A4:
(
x2 in the
carrier of
X &
y2 in the
carrier of
Y )
and A5:
u2 = [x2,y2]
by ZFMISC_1:def 2;
reconsider x2 =
x2 as
VECTOR of
X by A4;
reconsider y2 =
y2 as
VECTOR of
Y by A4;
u1 + u2 = [(x1 + x2),(y1 + y2)]
by A3, A5, Def1;
then A6:
a * (u1 + u2) = [(a * (x1 + x2)),(a * (y1 + y2))]
by Def2;
A7:
(
a * u1 = [(a * x1),(a * y1)] &
a * u2 = [(a * x2),(a * y2)] )
by A3, A5, Def2;
(
a * (x1 + x2) = (a * x1) + (a * x2) &
a * (y1 + y2) = (a * y1) + (a * y2) )
by RLVECT_1:def 9;
hence
a * (u1 + u2) = (a * u1) + (a * u2)
by A6, A7, Def1;
:: thesis: verum
end;
A8:
for a, b being real number
for u being VECTOR of (Prod_of_RLS X,Y) holds (a + b) * u = (a * u) + (b * u)
proof
let a,
b be
real number ;
:: thesis: for u being VECTOR of (Prod_of_RLS X,Y) holds (a + b) * u = (a * u) + (b * u)
reconsider a =
a,
b =
b as
Real by XREAL_0:def 1;
let u be
VECTOR of
(Prod_of_RLS X,Y);
:: thesis: (a + b) * u = (a * u) + (b * u)
consider x,
y being
set such that A9:
(
x in the
carrier of
X &
y in the
carrier of
Y )
and A10:
u = [x,y]
by ZFMISC_1:def 2;
reconsider x =
x as
VECTOR of
X by A9;
reconsider y =
y as
VECTOR of
Y by A9;
(
a * u = [(a * x),(a * y)] &
b * u = [(b * x),(b * y)] )
by A10, Def2;
then A11:
(a * u) + (b * u) = [((a * x) + (b * x)),((a * y) + (b * y))]
by Def1;
(
(a + b) * x = (a * x) + (b * x) &
(a + b) * y = (a * y) + (b * y) )
by RLVECT_1:def 9;
hence
(a + b) * u = (a * u) + (b * u)
by A10, A11, Def2;
:: thesis: verum
end;
A12:
for a, b being real number
for u being VECTOR of (Prod_of_RLS X,Y) holds (a * b) * u = a * (b * u)
proof
let a,
b be
real number ;
:: thesis: for u being VECTOR of (Prod_of_RLS X,Y) holds (a * b) * u = a * (b * u)
reconsider a =
a,
b =
b as
Real by XREAL_0:def 1;
let u be
VECTOR of
(Prod_of_RLS X,Y);
:: thesis: (a * b) * u = a * (b * u)
consider x,
y being
set such that A13:
(
x in the
carrier of
X &
y in the
carrier of
Y )
and A14:
u = [x,y]
by ZFMISC_1:def 2;
reconsider x =
x as
VECTOR of
X by A13;
reconsider y =
y as
VECTOR of
Y by A13;
b * u = [(b * x),(b * y)]
by A14, Def2;
then A15:
a * (b * u) = [(a * (b * x)),(a * (b * y))]
by Def2;
(
(a * b) * x = a * (b * x) &
(a * b) * y = a * (b * y) )
by RLVECT_1:def 9;
hence
(a * b) * u = a * (b * u)
by A14, A15, Def2;
:: thesis: verum
end;
for u being VECTOR of (Prod_of_RLS X,Y) holds 1 * u = u
hence
Prod_of_RLS X,Y is RealLinearSpace-like
by A1, A8, A12, RLVECT_1:def 9; :: thesis: verum