let X be non empty set ; :: thesis: for f being PartFunc of X,REAL
for x being Element of X holds 0 <= (max+ f) . x
let f be PartFunc of X,REAL; :: thesis: for x being Element of X holds 0 <= (max+ f) . x
let x be Element of X; :: thesis: 0 <= (max+ f) . x
0. <= (max+ (R_EAL f)) . x by MESFUNC2:12;
hence 0 <= (max+ f) . x by Th30; :: thesis: verum