for Y being set
for C being non empty set
for f being PartFunc of C,COMPLEX holds
( f | Y is bounded iff ex p being Real st
for c being Element of C st c in Y /\ (dom f) holds
|.(f /. c).| <= p )