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 set such that
A1: ( x in the carrier of X & y in the carrier of Y ) and
A2: u = [x,y] by ZFMISC_1:def 2;
reconsider x = x as VECTOR of X by A1;
reconsider y = y as VECTOR of Y by A1;
( x + (0. X) = x & y + (0. Y) = y ) by RLVECT_1:def 7;
hence u + (0. (Prod_of_RLS X,Y)) = u by A2, Def1; :: thesis: verum

end;

hence Prod_of_RLS X,Y is right_zeroed by RLVECT_1:def 7; :: thesis: verum