let X, Y be set ; :: thesis: for C being non empty set
for f being PartFunc of C,COMPLEX st Y c= X & f | X is bounded holds
f | Y is bounded
let C be non empty set ; :: thesis: for f being PartFunc of C,COMPLEX st Y c= X & f | X is bounded holds
f | Y is bounded
let f be PartFunc of C,COMPLEX; :: thesis: ( Y c= X & f | X is bounded implies f | Y is bounded )
assume that
A1: Y c= X and
A2: f | X is bounded ; :: thesis: f | Y is bounded
|.f.| | X = |.(f | X).| by RFUNCT_1:46;
then |.f.| | X is bounded by A2, Lm3;
then ( |.f.| | Y = |.(f | Y).| & |.f.| | Y is bounded ) by A1, RFUNCT_1:46, RFUNCT_1:74;
hence f | Y is bounded by Lm3; :: thesis: verum