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 Def2;

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

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

then (max+ f) . x = max ((f . x),0.) by A1, Def2;
hence 0. <= (max+ f) . x by XXREAL_0:25; :: thesis: verum

end;

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

hence 0. <= (max+ f) . x by A1, FUNCT_1:def 2; :: thesis: verum

end;

end;