let x, y be Element of [:G,F:]; :: according to RLVECT_1:def 2 :: thesis: x + y = y + x
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, y2 being Point of F such that
A2: y = [y1,y2] by Lm1;
x + y = [(x1 + y1),(x2 + y2)] by A1, A2, Def1;
hence x + y = y + x by A1, A2, Def1; :: thesis: verum