A1:
for a being Real

for u1, u2 being VECTOR of (Prod_of_RLS (X,Y)) holds a * (u1 + u2) = (a * u1) + (a * u2)

for u being VECTOR of (Prod_of_RLS (X,Y)) holds (a * b) * u = a * (b * u)

for u being VECTOR of (Prod_of_RLS (X,Y)) holds (a + b) * u = (a * u) + (b * u)

for u1, u2 being VECTOR of (Prod_of_RLS (X,Y)) holds a * (u1 + u2) = (a * u1) + (a * u2)

proof

A12:
for a, b being Real
let a be Real; :: 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 ;

let u1, u2 be VECTOR of (Prod_of_RLS (X,Y)); :: thesis: a * (u1 + u2) = (a * u1) + (a * u2)

consider x1, y1 being object such that

A2: x1 in the carrier of X and

A3: y1 in the carrier of Y and

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

reconsider x1 = x1 as VECTOR of X by A2;

consider x2, y2 being object such that

A5: x2 in the carrier of X and

A6: y2 in the carrier of Y and

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

reconsider y2 = y2 as VECTOR of Y by A6;

reconsider x2 = x2 as VECTOR of X by A5;

reconsider y1 = y1 as VECTOR of Y by A3;

A8: a * (x1 + x2) = (a * x1) + (a * x2) by RLVECT_1:def 5;

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

then A9: a * (u1 + u2) = [(a * (x1 + x2)),(a * (y1 + y2))] by Def2;

A10: a * (y1 + y2) = (a * y1) + (a * y2) by RLVECT_1:def 5;

A11: a * u2 = [(a * x2),(a * y2)] by A7, Def2;

a * u1 = [(a * x1),(a * y1)] by A4, Def2;

hence a * (u1 + u2) = (a * u1) + (a * u2) by A9, A11, A8, A10, Def1; :: thesis: verum

end;reconsider a = a as Real ;

let u1, u2 be VECTOR of (Prod_of_RLS (X,Y)); :: thesis: a * (u1 + u2) = (a * u1) + (a * u2)

consider x1, y1 being object such that

A2: x1 in the carrier of X and

A3: y1 in the carrier of Y and

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

reconsider x1 = x1 as VECTOR of X by A2;

consider x2, y2 being object such that

A5: x2 in the carrier of X and

A6: y2 in the carrier of Y and

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

reconsider y2 = y2 as VECTOR of Y by A6;

reconsider x2 = x2 as VECTOR of X by A5;

reconsider y1 = y1 as VECTOR of Y by A3;

A8: a * (x1 + x2) = (a * x1) + (a * x2) by RLVECT_1:def 5;

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

then A9: a * (u1 + u2) = [(a * (x1 + x2)),(a * (y1 + y2))] by Def2;

A10: a * (y1 + y2) = (a * y1) + (a * y2) by RLVECT_1:def 5;

A11: a * u2 = [(a * x2),(a * y2)] by A7, Def2;

a * u1 = [(a * x1),(a * y1)] by A4, Def2;

hence a * (u1 + u2) = (a * u1) + (a * u2) by A9, A11, A8, A10, Def1; :: thesis: verum

for u being VECTOR of (Prod_of_RLS (X,Y)) holds (a * b) * u = a * (b * u)

proof

A18:
for a, b being Real
let a, b be Real; :: 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 ;

let u be VECTOR of (Prod_of_RLS (X,Y)); :: thesis: (a * b) * u = a * (b * u)

consider x, y being object such that

A13: x in the carrier of X and

A14: y in the carrier of Y and

A15: u = [x,y] by ZFMISC_1:def 2;

reconsider y = y as VECTOR of Y by A14;

reconsider x = x as VECTOR of X by A13;

b * u = [(b * x),(b * y)] by A15, Def2;

then A16: a * (b * u) = [(a * (b * x)),(a * (b * y))] by Def2;

A17: (a * b) * y = a * (b * y) by RLVECT_1:def 7;

(a * b) * x = a * (b * x) by RLVECT_1:def 7;

hence (a * b) * u = a * (b * u) by A15, A16, A17, Def2; :: thesis: verum

end;reconsider a = a, b = b as Real ;

let u be VECTOR of (Prod_of_RLS (X,Y)); :: thesis: (a * b) * u = a * (b * u)

consider x, y being object such that

A13: x in the carrier of X and

A14: y in the carrier of Y and

A15: u = [x,y] by ZFMISC_1:def 2;

reconsider y = y as VECTOR of Y by A14;

reconsider x = x as VECTOR of X by A13;

b * u = [(b * x),(b * y)] by A15, Def2;

then A16: a * (b * u) = [(a * (b * x)),(a * (b * y))] by Def2;

A17: (a * b) * y = a * (b * y) by RLVECT_1:def 7;

(a * b) * x = a * (b * x) by RLVECT_1:def 7;

hence (a * b) * u = a * (b * u) by A15, A16, A17, Def2; :: thesis: verum

for u being VECTOR of (Prod_of_RLS (X,Y)) holds (a + b) * u = (a * u) + (b * u)

proof

for u being VECTOR of (Prod_of_RLS (X,Y)) holds 1 * u = u
let a, b be Real; :: 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 ;

let u be VECTOR of (Prod_of_RLS (X,Y)); :: thesis: (a + b) * u = (a * u) + (b * u)

consider x, y being object such that

A19: x in the carrier of X and

A20: y in the carrier of Y and

A21: u = [x,y] by ZFMISC_1:def 2;

reconsider y = y as VECTOR of Y by A20;

reconsider x = x as VECTOR of X by A19;

A22: b * u = [(b * x),(b * y)] by A21, Def2;

a * u = [(a * x),(a * y)] by A21, Def2;

then A23: (a * u) + (b * u) = [((a * x) + (b * x)),((a * y) + (b * y))] by A22, Def1;

A24: (a + b) * y = (a * y) + (b * y) by RLVECT_1:def 6;

(a + b) * x = (a * x) + (b * x) by RLVECT_1:def 6;

hence (a + b) * u = (a * u) + (b * u) by A21, A23, A24, Def2; :: thesis: verum

end;reconsider a = a, b = b as Real ;

let u be VECTOR of (Prod_of_RLS (X,Y)); :: thesis: (a + b) * u = (a * u) + (b * u)

consider x, y being object such that

A19: x in the carrier of X and

A20: y in the carrier of Y and

A21: u = [x,y] by ZFMISC_1:def 2;

reconsider y = y as VECTOR of Y by A20;

reconsider x = x as VECTOR of X by A19;

A22: b * u = [(b * x),(b * y)] by A21, Def2;

a * u = [(a * x),(a * y)] by A21, Def2;

then A23: (a * u) + (b * u) = [((a * x) + (b * x)),((a * y) + (b * y))] by A22, Def1;

A24: (a + b) * y = (a * y) + (b * y) by RLVECT_1:def 6;

(a + b) * x = (a * x) + (b * x) by RLVECT_1:def 6;

hence (a + b) * u = (a * u) + (b * u) by A21, A23, A24, Def2; :: thesis: verum

proof

hence
( Prod_of_RLS (X,Y) is vector-distributive & Prod_of_RLS (X,Y) is scalar-distributive & Prod_of_RLS (X,Y) is scalar-associative & Prod_of_RLS (X,Y) is scalar-unital )
by A1, A18, A12; :: thesis: verum
let u be VECTOR of (Prod_of_RLS (X,Y)); :: thesis: 1 * u = u

consider x, y being object such that

A25: x in the carrier of X and

A26: y in the carrier of Y and

A27: u = [x,y] by ZFMISC_1:def 2;

reconsider y = y as VECTOR of Y by A26;

reconsider x = x as VECTOR of X by A25;

A28: 1 * y = y by RLVECT_1:def 8;

1 * x = x by RLVECT_1:def 8;

hence 1 * u = u by A27, A28, Def2; :: thesis: verum

end;consider x, y being object such that

A25: x in the carrier of X and

A26: y in the carrier of Y and

A27: u = [x,y] by ZFMISC_1:def 2;

reconsider y = y as VECTOR of Y by A26;

reconsider x = x as VECTOR of X by A25;

A28: 1 * y = y by RLVECT_1:def 8;

1 * x = x by RLVECT_1:def 8;

hence 1 * u = u by A27, A28, Def2; :: thesis: verum