let Y, X 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 )
F: |.f.| | Y = |.(f | Y).| by RFUNCT_1:62;
G: |.f.| | X = |.(f | X).| by RFUNCT_1:62;
assume ( Y c= X & f | X is bounded ) ; :: thesis: f | Y is bounded
then ( Y c= X & |.f.| | X is bounded ) by Def3, G;
then |.f.| | Y is bounded by RFUNCT_1:91;
hence f | Y is bounded by Def3, F; :: thesis: verum