let x, y be Element of [:G,F:]; :: according to RLVECT_1:def 2 :: thesis: x + y = y + x
consider x1 being Vector of G, x2 being Vector of F such that
A1: x = [x1,x2] by SUBSET_1:43;
consider y1 being Vector of G, y2 being Vector of F such that
A2: y = [y1,y2] by SUBSET_1:43;
x + y = [(x1 + y1),(x2 + y2)] by A1, A2, PRVECT_3:def 1;
hence x + y = y + x by A1, A2, PRVECT_3:def 1; :: thesis: verum