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

proof

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;

hence Prod_of_RLS (X,Y) is right_zeroed ; :: thesis: verum