let a, b be Element of K; :: according to VECTSP_1:def 15 :: thesis: for b₁ being Element of the carrier of [:G,F:] holds (a * b) * b₁ = a * (b * b₁)
let x be Vector of [:G,F:]; :: thesis: (a * b) * x = a * (b * x)
consider x1 being Vector of G, x2 being Vector of F such that
A1: x = [x1,x2] by SUBSET_1:43;
A2: ( (a * b) * x1 = a * (b * x1) & (a * b) * x2 = a * (b * x2) ) by VECTSP_1:def 16;
thus (a * b) * x = [((a * b) * x1),((a * b) * x2)] by A1, YDef2
.= (prod_MLT (G,F)) . (a,[(b * x1),(b * x2)]) by A2, YDef2
.= a * (b * x) by A1, YDef2 ; :: thesis: verum