let x be Vector of [:G,F:]; :: according to VECTSP_1:def 16 :: thesis: (1. K) * x = x
consider x1 being Vector of G, x2 being Vector of F such that
A1: x = [x1,x2] by SUBSET_1:43;
( (1. K) * x1 = x1 & (1. K) * x2 = x2 ) by VECTSP_1:def 17;
hence (1. K) * x = x by A1, YDef2; :: thesis: verum