let x be Element of [:G,F:]; :: according to ALGSTR_0:def 16 :: thesis: x is right_complementable
consider x1 being Point of G, x2 being Point of F such that
A1: x = [x1,x2] by Lm1;
consider y1 being Point of G such that
A2: x1 + y1 = 0. G by ALGSTR_0:def 11;
consider y2 being Point of F such that
A3: x2 + y2 = 0. F by ALGSTR_0:def 11;
reconsider y = [y1,y2] as Element of [:G,F:] ;
take y ; :: according to ALGSTR_0:def 11 :: thesis: x + y = 0. [:G,F:]
thus x + y = 0. [:G,F:] by A1, A2, A3, Def1; :: thesis: verum