let Y be set ; :: thesis: for f being real-valued Function holds (0 (#) f) | Y is bounded

let f be real-valued Function; :: thesis: (0 (#) f) | Y is bounded

reconsider p1 = 0 as Real ;

set r = 0 ;

let f be real-valued Function; :: thesis: (0 (#) f) | Y is bounded

reconsider p1 = 0 as Real ;

set r = 0 ;

now :: thesis: ex p being Real st

for c being object st c in Y /\ (dom (0 (#) f)) holds

(0 (#) f) . c <= p

hence
(0 (#) f) | Y is bounded_above
by Th70; :: according to SEQ_2:def 8 :: thesis: (0 (#) f) | Y is bounded_below for c being object st c in Y /\ (dom (0 (#) f)) holds

(0 (#) f) . c <= p

take p = p1; :: thesis: for c being object st c in Y /\ (dom (0 (#) f)) holds

(0 (#) f) . c <= p

let c be object ; :: thesis: ( c in Y /\ (dom (0 (#) f)) implies (0 (#) f) . c <= p )

assume c in Y /\ (dom (0 (#) f)) ; :: thesis: (0 (#) f) . c <= p

then A1: c in dom (0 (#) f) by XBOOLE_0:def 4;

0 * (f . c) <= 0 ;

hence (0 (#) f) . c <= p by A1, VALUED_1:def 5; :: thesis: verum

end;(0 (#) f) . c <= p

let c be object ; :: thesis: ( c in Y /\ (dom (0 (#) f)) implies (0 (#) f) . c <= p )

assume c in Y /\ (dom (0 (#) f)) ; :: thesis: (0 (#) f) . c <= p

then A1: c in dom (0 (#) f) by XBOOLE_0:def 4;

0 * (f . c) <= 0 ;

hence (0 (#) f) . c <= p by A1, VALUED_1:def 5; :: thesis: verum

now :: thesis: ex p being Real st

for c being object st c in Y /\ (dom (0 (#) f)) holds

p <= (0 (#) f) . c

hence
(0 (#) f) | Y is bounded_below
by Th71; :: thesis: verumfor c being object st c in Y /\ (dom (0 (#) f)) holds

p <= (0 (#) f) . c

take p = p1; :: thesis: for c being object st c in Y /\ (dom (0 (#) f)) holds

p <= (0 (#) f) . c

let c be object ; :: thesis: ( c in Y /\ (dom (0 (#) f)) implies p <= (0 (#) f) . c )

assume c in Y /\ (dom (0 (#) f)) ; :: thesis: p <= (0 (#) f) . c

then A2: c in dom (0 (#) f) by XBOOLE_0:def 4;

0 <= 0 * (f . c) ;

hence p <= (0 (#) f) . c by A2, VALUED_1:def 5; :: thesis: verum

end;p <= (0 (#) f) . c

let c be object ; :: thesis: ( c in Y /\ (dom (0 (#) f)) implies p <= (0 (#) f) . c )

assume c in Y /\ (dom (0 (#) f)) ; :: thesis: p <= (0 (#) f) . c

then A2: c in dom (0 (#) f) by XBOOLE_0:def 4;

0 <= 0 * (f . c) ;

hence p <= (0 (#) f) . c by A2, VALUED_1:def 5; :: thesis: verum