let x be VECTOR of [:G,F:]; :: according to RLVECT_1:def 8 :: thesis: 1 * x = x
consider x1 being Point of G, x2 being Point of F such that
A1: x = [x1,x2] by Lm1;
( 1 * x1 = x1 & 1 * x2 = x2 ) by RLVECT_1:def 8;
hence 1 * x = x by A1, Def2; :: thesis: verum