let a0, b0 be Real; RLVECT_1:def 7 for b1 being Element of the carrier of [:G,F:] holds (a0 * b0) * b1 = a0 * (b0 * b1)
let x be VECTOR of [:G,F:]; (a0 * b0) * x = a0 * (b0 * x)
reconsider a = a0, b = b0 as Element of REAL by XREAL_0:def 1;
consider x1 being Point of G, x2 being Point of F such that
A1:
x = [x1,x2]
by Lm1;
A2:
( (a * b) * x1 = a0 * (b0 * x1) & (a * b) * x2 = a0 * (b0 * x2) )
by RLVECT_1:def 7;
thus (a0 * b0) * x =
[((a * b) * x1),((a * b) * x2)]
by A1, Def2
.=
(prod_MLT (G,F)) . (a,[(b * x1),(b * x2)])
by A2, Def2
.=
a0 * (b0 * x)
by A1, Def2
; verum