let x, y be Element of [:G,F:]; :: according to RLVECT_1:def 5 :: thesis: x + y = y + x
consider x1 being Point of G, x2 being Point of F such that
P1: x = [x1,x2] by LM01;
consider y1 being Point of G, y2 being Point of F such that
P2: y = [y1,y2] by LM01;
thus x + y = [(x1 + y1),(x2 + y2)] by P1, P2, defADD
.= y + x by P1, P2, defADD ; :: thesis: verum