now :: thesis:

let x be object ; :: thesis:

per cases ;

suppose A1: x in dom (- f) ; :: thesis:

then reconsider x1 = x as Element of X ;
(- f) . x = - (f . x1) by A1, MESFUNC1:def 7;
hence (- f) . x < +infty by XXREAL_3:5, XXREAL_3:38, MESFUNC5:def 5; :: thesis:

end;

suppose not x in dom (- f) ; :: thesis:

hence (- f) . x < +infty by FUNCT_1:def 2; :: thesis:

end;

end;

end;

hence - f is V184() by MESFUNC5:def 6; :: thesis: