now

reconsider p = - 1 as real number ;
take p = p; :: thesis: for c being set st c in dom (abs f) holds
p < (abs f) . c
let c be set ; :: thesis: ( c in dom (abs f) implies p < (abs f) . c )
assume c in dom (abs f) ; :: thesis: p < (abs f) . c
0 <= abs (f . c) by COMPLEX1:46;
hence p < (abs f) . c by VALUED_1:18; :: thesis: verum

end;

hence abs f is bounded_below by SEQ_2:def 2; :: thesis: verum