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 :: thesis: ex z being Element of NAT st
for c being object st c in X /\ (dom |.f.|) holds
z <= |.f.| . c

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

end;

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