let a, b be Element of K; VECTSP_1:def 14 for b1 being Element of the carrier of [:G,F:] holds (a + b) * b1 = (a * b1) + (b * b1)
let x be Vector of [:G,F:]; (a + b) * x = (a * x) + (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 * x1) + (b * x1) & (a + b) * x2 = (a * x2) + (b * x2) )
by VECTSP_1:def 15;
thus (a + b) * x =
[((a + b) * x1),((a + b) * x2)]
by A1, YDef2
.=
(prod_ADD (G,F)) . ([(a * x1),(a * x2)],[(b * x1),(b * x2)])
by A2, PRVECT_3:def 1
.=
(prod_ADD (G,F)) . (((prod_MLT (G,F)) . (a,[x1,x2])),[(b * x1),(b * x2)])
by YDef2
.=
(a * x) + (b * x)
by A1, YDef2
; verum