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 ;
now :: thesis: ex p being Real st
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;
hence (0 (#) f) | Y is bounded_above by Th70; :: according to SEQ_2:def 8 :: thesis: (0 (#) f) | Y is bounded_below
now :: thesis: ex p being Real st
for 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;
hence (0 (#) f) | Y is bounded_below by Th71; :: thesis: verum