now :: thesis: ex p being Real st

for c being object st c in dom (abs f) holds

p < (abs f) . c

hence
abs f is bounded_below
; :: thesis: verumfor c being object st c in dom (abs f) holds

p < (abs f) . c

reconsider p = - 1 as Real ;

take p = p; :: thesis: for c being object st c in dom (abs f) holds

p < (abs f) . c

let c be object ; :: thesis: ( c in dom (abs f) implies p < (abs f) . c )

assume c in dom (abs f) ; :: thesis: p < (abs f) . c

0 <= |.(f . c).| by COMPLEX1:46;

hence p < (abs f) . c by VALUED_1:18; :: thesis: verum

end;take p = p; :: thesis: for c being object st c in dom (abs f) holds

p < (abs f) . c

let c be object ; :: thesis: ( c in dom (abs f) implies p < (abs f) . c )

assume c in dom (abs f) ; :: thesis: p < (abs f) . c

0 <= |.(f . c).| by COMPLEX1:46;

hence p < (abs f) . c by VALUED_1:18; :: thesis: verum