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 being Element of (Maps (X,L)) holds x is right_complementable

let x be Element of (Maps (X,L)); :: thesis: x is right_complementable
reconsider f = x as Function of X, the carrier of L by A, FUNCT_2:66;
reconsider y = '-' f as Element of (Maps (X,L)) by A, FUNCT_2:8;
x + y = f '+' ('-' f) by A, dA
.= 0. (Maps (X,L)) by rc, A ;
hence x is right_complementable by ALGSTR_0:def 11; :: thesis: verum

end;

hence Maps (X,L) is right_complementable by ALGSTR_0:def 16; :: thesis: verum