let u be Element of (Prod_of_RLS X,Y); :: according to ALGSTR_0:def 16 :: thesis: u is right_complementable
consider x, y being set 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 x = x as VECTOR of X by A1;
consider x1 being VECTOR of X such that
A4: x + x1 = 0. X by ALGSTR_0:def 11;
reconsider y = y as VECTOR of Y by A2;
consider y1 being VECTOR of Y such that
A5: y + y1 = 0. Y by ALGSTR_0:def 11;
set u1 = [x1,y1];
reconsider u1 = [x1,y1] as Element of (Prod_of_RLS X,Y) ;
take u1 ; :: according to ALGSTR_0:def 11 :: thesis: u + u1 = 0. (Prod_of_RLS X,Y)
thus u + u1 = 0. (Prod_of_RLS X,Y) by A3, A4, A5, Def1; :: thesis: verum