let C be non empty set ; :: thesis: for f being PartFunc of C,ExtREAL
for x being Element of C holds 0. <= (max- f) . x
let f be PartFunc of C,ExtREAL ; :: thesis: for x being Element of C holds 0. <= (max- f) . x
let x be Element of C; :: thesis: 0. <= (max- f) . x
A1: dom (max- f) = dom f by Def3;

per cases ( x in dom f or not x in dom f ) ;

suppose A2: x in dom f ; :: thesis: 0. <= (max- f) . x

A3: (max- f) . x = max (- (f . x)),0. by A1, A2, Def3;
thus 0. <= (max- f) . x by A3, XXREAL_0:25; :: thesis: verum

end;

suppose A4: not x in dom f ; :: thesis: 0. <= (max- f) . x

thus 0. <= (max- f) . x by A1, A4, FUNCT_1:def 4; :: thesis: verum

end;

end;