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