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;

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;