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 x, y, z being Element of (Maps (X,L)) holds (x + y) + z = x + (y + z)

let x, y, z be Element of (Maps (X,L)); :: thesis: (x + y) + z = x + (y + z)
reconsider f = x, g = y, h = z as Function of X, the carrier of L by A, FUNCT_2:66;
B: ( x + y = f '+' g & y + z = g '+' h ) by A, dA;
hence (x + y) + z = (f '+' g) '+' h by A, dA
.= f '+' (g '+' h) by ass
.= x + (y + z) by B, A, dA ;
:: thesis: verum

end;

hence Maps (X,L) is add-associative by RLVECT_1:def 3; :: thesis: verum