let X be set ; :: thesis: for C being non empty set
for f being PartFunc of C,COMPLEX holds |.f.| | X is bounded_below
let C be non empty set ; :: thesis: for f being PartFunc of C,COMPLEX holds |.f.| | X is bounded_below
let f be PartFunc of C,COMPLEX ; :: thesis: |.f.| | X is bounded_below

now

take z = 0 ; :: thesis: for c being set st c in X /\ (dom |.f.|) holds
z <= |.f.| . c
let c be set ; :: thesis: ( c in X /\ (dom |.f.|) implies z <= |.f.| . c )
assume c in X /\ (dom |.f.|) ; :: thesis: z <= |.f.| . c
then A1: c in dom |.f.| by XBOOLE_0:def 4;
dom |.f.| = dom f by VALUED_1:def 11;
then A2: f . c = f /. c by A1, PARTFUN1:def 8;
z <= |.(f /. c).| by COMPLEX1:132;
hence z <= |.f.| . c by A2, VALUED_1:18; :: thesis: verum

end;

hence |.f.| | X is bounded_below by RFUNCT_1:88; :: thesis: verum