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
P1: x = [x1,x2] by LM01;
consider y1 being Point of G such that
P2: x1 + y1 = 0. G by ALGSTR_0:def 11;
consider y2 being Point of F such that
P3: 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 P1, P2, P3, defADD; :: thesis: verum