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 ) )

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

( ( 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

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 )
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;

end;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

hence
f | Y is bounded_above
by Th70; :: thesis: verumfor 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;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

proof

assume that
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;

end;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

hence
f | Y is bounded_below
by Th71; :: thesis: verumfor 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;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

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