consider r being Real such that

A1: for y being object st y in dom f holds

f . y < r by SEQ_2:def 1;

f | X is bounded_above_{1} being real-valued Function st b_{1} = f | X holds

b_{1} is bounded_above
; :: thesis: verum

A1: for y being object st y in dom f holds

f . y < r by SEQ_2:def 1;

f | X is bounded_above

proof

hence
for b
take
r
; :: according to SEQ_2:def 1 :: thesis: for b_{1} being object holds

( not b_{1} in dom (f | X) or not r <= (f | X) . b_{1} )

let y be object ; :: thesis: ( not y in dom (f | X) or not r <= (f | X) . y )

assume A2: y in dom (f | X) ; :: thesis: not r <= (f | X) . y

then y in dom f by RELAT_1:57;

then f . y < r by A1;

hence not r <= (f | X) . y by A2, FUNCT_1:47; :: thesis: verum

end;( not b

let y be object ; :: thesis: ( not y in dom (f | X) or not r <= (f | X) . y )

assume A2: y in dom (f | X) ; :: thesis: not r <= (f | X) . y

then y in dom f by RELAT_1:57;

then f . y < r by A1;

hence not r <= (f | X) . y by A2, FUNCT_1:47; :: thesis: verum

b