let x be Element of [:G,F:]; ALGSTR_0:def 16 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
; ALGSTR_0:def 11 x + y = 0. [:G,F:]
thus
x + y = 0. [:G,F:]
by A1, A2, A3, Def1; verum