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