set V = Maps (X,L);
A: ( the carrier of (Maps (X,L)) = Funcs (X, the carrier of L) & the addF of (Maps (X,L)) = mapAdd (X,L) & the ZeroF of (Maps (X,L)) = X --> (0. L) & the lmult of (Maps (X,L)) = mapMult (X,L) ) by defmap;

now :: thesis: for a being Element of L
for u, v being Element of (Maps (X,L)) holds a * (u + v) = (a * u) + (a * v)

let a be Element of L; :: thesis: for u, v being Element of (Maps (X,L)) holds a * (u + v) = (a * u) + (a * v)
let u, v be Element of (Maps (X,L)); :: thesis: a * (u + v) = (a * u) + (a * v)
reconsider f = u, g = v as Function of X,L by A, FUNCT_2:66;
( a * v = the lmult of (Maps (X,L)) . (a,v) & a * u = the lmult of (Maps (X,L)) . (a,u) ) by VECTSP_1:def 12;
then B: ( a '*' f = a * u & a '*' g = a * v ) by A, dM;
C: f '+' g = u + v by A, dA;
thus a * (u + v) = (mapMult (X,L)) . (a,(f '+' g)) by A, C, VECTSP_1:def 12
.= a '*' (f '+' g) by dM
.= (a '*' f) '+' (a '*' g) by vd
.= (a * u) + (a * v) by B, A, dA ; :: thesis: verum

end;

hence Maps (X,L) is vector-distributive by VECTSP_1:def 14; :: thesis: verum