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

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