let X be non empty set ; :: thesis: for L being non empty right_complementable add-associative right_zeroed addLoopStr
for f being Function of X,L holds f '+' ('-' f) = X --> (0. L)
let L be non empty right_complementable add-associative right_zeroed addLoopStr ; :: thesis: for f being Function of X,L holds f '+' ('-' f) = X --> (0. L)
let f be Function of X,L; :: thesis: f '+' ('-' f) = X --> (0. L)

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

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

end;

hence f '+' ('-' f) = X --> (0. L) by FUNCT_2:12; :: thesis: verum