let x be Element of [:G,F:]; :: according to RLVECT_1:def 4 :: thesis: x + (0. [:G,F:]) = x
consider x1 being Point of G, x2 being Point of F such that
A1: x = [x1,x2] by Lm1;
( x1 + (0. G) = x1 & x2 + (0. F) = x2 ) by RLVECT_1:def 4;
hence x + (0. [:G,F:]) = x by A1, Def1; :: thesis: verum