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, b being Element of R
for v being Element of (Maps (X,L)) holds (a * b) * v = a * (b * v)

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

end;

hence Maps (X,L) is scalar-associative by VECTSP_1:def 16; :: thesis: verum