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 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 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

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 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