let X, Y be set ; :: thesis: for f being real-valued Function holds
( ( Y c= X & f | X is bounded_above implies f | Y is bounded_above ) & ( Y c= X & f | X is bounded_below implies f | Y is bounded_below ) & ( Y c= X & f | X is bounded implies f | Y is bounded ) )
let f be real-valued Function; :: thesis: ( ( Y c= X & f | X is bounded_above implies f | Y is bounded_above ) & ( Y c= X & f | X is bounded_below implies f | Y is bounded_below ) & ( Y c= X & f | X is bounded implies f | Y is bounded ) )
thus A1: ( Y c= X & f | X is bounded_above implies f | Y is bounded_above ) :: thesis: ( ( Y c= X & f | X is bounded_below implies f | Y is bounded_below ) & ( Y c= X & f | X is bounded implies f | Y is bounded ) )

proof

assume that
A2: Y c= X and
A3: f | X is bounded_above ; :: thesis: f | Y is bounded_above
consider r being Real such that
A4: for c being object st c in X /\ (dom f) holds
f . c <= r by A3, Th70;

now :: thesis: ex r being Real st
for c being object st c in Y /\ (dom f) holds
f . c <= r

take r = r; :: thesis: for c being object st c in Y /\ (dom f) holds
f . c <= r
let c be object ; :: thesis: ( c in Y /\ (dom f) implies f . c <= r )
assume A5: c in Y /\ (dom f) ; :: thesis: f . c <= r
then A6: c in dom f by XBOOLE_0:def 4;
c in Y by A5, XBOOLE_0:def 4;
then c in X /\ (dom f) by A2, A6, XBOOLE_0:def 4;
hence f . c <= r by A4; :: thesis: verum

end;

hence f | Y is bounded_above by Th70; :: thesis: verum

end;

thus A7: ( Y c= X & f | X is bounded_below implies f | Y is bounded_below ) :: thesis: ( Y c= X & f | X is bounded implies f | Y is bounded )

proof

assume that
A8: Y c= X and
A9: f | X is bounded_below ; :: thesis: f | Y is bounded_below
consider r being Real such that
A10: for c being object st c in X /\ (dom f) holds
r <= f . c by A9, Th71;

now :: thesis: ex r being Real st
for c being object st c in Y /\ (dom f) holds
r <= f . c

take r = r; :: thesis: for c being object st c in Y /\ (dom f) holds
r <= f . c
let c be object ; :: thesis: ( c in Y /\ (dom f) implies r <= f . c )
assume A11: c in Y /\ (dom f) ; :: thesis: r <= f . c
then A12: c in dom f by XBOOLE_0:def 4;
c in Y by A11, XBOOLE_0:def 4;
then c in X /\ (dom f) by A8, A12, XBOOLE_0:def 4;
hence r <= f . c by A10; :: thesis: verum

end;

hence f | Y is bounded_below by Th71; :: thesis: verum

end;

assume that
A13: Y c= X and
A14: f | X is bounded ; :: thesis: f | Y is bounded
thus f | Y is bounded by A1, A7, A13, A14; :: thesis: verum