set V = Maps (X,L);
set g = X --> (0. 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 being Element of (Maps (X,L)) holds x + (0. (Maps (X,L))) = x

let x be Element of (Maps (X,L)); :: thesis: x + (0. (Maps (X,L))) = x
reconsider f = x as Function of X, the carrier of L by A, FUNCT_2:66;

B: now :: thesis: for o being object st o in X holds
(f '+' (X --> (0. L))) . o = f . o

let o be object ; :: thesis: ( o in X implies (f '+' (X --> (0. L))) . o = f . o )
assume o in X ; :: thesis: (f '+' (X --> (0. L))) . o = f . o
then reconsider x = o as Element of X ;
thus (f '+' (X --> (0. L))) . o = (f . x) + ((X --> (0. L)) . x) by defp
.= f . o by RLVECT_1:def 4 ; :: thesis: verum

end;

thus x + (0. (Maps (X,L))) = f '+' (X --> (0. L)) by A, dA
.= x by B, FUNCT_2:12 ; :: thesis: verum

end;

hence Maps (X,L) is right_zeroed by RLVECT_1:def 4; :: thesis: verum