let C be non empty set ; :: thesis: for X being set
for f being PartFunc of C,REAL holds (max+ f) | X is bounded_below
let X be set ; :: thesis: for f being PartFunc of C,REAL holds (max+ f) | X is bounded_below
let f be PartFunc of C,REAL ; :: thesis: (max+ f) | X is bounded_below
ex r being Real st
for c being set st c in X /\ (dom (max+ f)) holds
(max+ f) . c >= r

proof

for c being set st c in X /\ (dom (max+ f)) holds
(max+ f) . c >= 0 by RFUNCT_3:40;
hence ex r being Real st
for c being set st c in X /\ (dom (max+ f)) holds
(max+ f) . c >= r ; :: thesis: verum

end;

hence (max+ f) | X is bounded_below by RFUNCT_1:88; :: thesis: verum