for u being Element of (Prod_of_RLS (X,Y)) holds u + (0. (Prod_of_RLS (X,Y))) = u

proof

hence
Prod_of_RLS (X,Y) is right_zeroed
; :: thesis: verum
let u be Element of (Prod_of_RLS (X,Y)); :: thesis: u + (0. (Prod_of_RLS (X,Y))) = u

consider x, y being object such that

A1: x in the carrier of X and

A2: y in the carrier of Y and

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

reconsider y = y as VECTOR of Y by A2;

reconsider x = x as VECTOR of X by A1;

A4: y + (0. Y) = y by RLVECT_1:def 4;

x + (0. X) = x by RLVECT_1:def 4;

hence u + (0. (Prod_of_RLS (X,Y))) = u by A3, A4, Def1; :: thesis: verum

end;consider x, y being object such that

A1: x in the carrier of X and

A2: y in the carrier of Y and

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

reconsider y = y as VECTOR of Y by A2;

reconsider x = x as VECTOR of X by A1;

A4: y + (0. Y) = y by RLVECT_1:def 4;

x + (0. X) = x by RLVECT_1:def 4;

hence u + (0. (Prod_of_RLS (X,Y))) = u by A3, A4, Def1; :: thesis: verum