let x be Element of [:G,F:]; :: according to RLVECT_1:def 4 :: thesis: x + (0. [:G,F:]) = x

consider x1 being Vector of G, x2 being Vector of F such that

A1: x = [x1,x2] by SUBSET_1:43;

( x1 + (0. G) = x1 & x2 + (0. F) = x2 ) by RLVECT_1:def 4;

hence x + (0. [:G,F:]) = x by A1, 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;

( x1 + (0. G) = x1 & x2 + (0. F) = x2 ) by RLVECT_1:def 4;

hence x + (0. [:G,F:]) = x by A1, PRVECT_3:def 1; :: thesis: verum