let Y be set ; :: thesis: for C being non empty set
for f being PartFunc of C,COMPLEX holds
( f | Y is bounded iff ex p being Real st
for c being Element of C st c in Y /\ (dom f) holds
|.(f /. c).| <= p )
let C be non empty set ; :: thesis: for f being PartFunc of C,COMPLEX holds
( f | Y is bounded iff ex p being Real st
for c being Element of C st c in Y /\ (dom f) holds
|.(f /. c).| <= p )
let f be PartFunc of C,COMPLEX; :: thesis: ( f | Y is bounded iff ex p being Real st
for c being Element of C st c in Y /\ (dom f) holds
|.(f /. c).| <= p )
A1: dom |.f.| = dom f by VALUED_1:def 11;
A2: dom (|.f.| | Y) = Y /\ (dom |.f.|) by RELAT_1:61;
A3: |.f.| | Y = |.(f | Y).| by RFUNCT_1:46;

hereby :: thesis: ( ex p being Real st
for c being Element of C st c in Y /\ (dom f) holds
|.(f /. c).| <= p implies f | Y is bounded )

assume f | Y is bounded ; :: thesis: ex p being Real st
for c being Element of C st c in Y /\ (dom f) holds
|.(f /. c).| <= p
then |.f.| | Y is bounded by A3, Lm3;
then consider p being Real such that
A4: for c being object st c in dom (|.f.| | Y) holds
|.((|.f.| | Y) . c).| <= p by RFUNCT_1:72;

now :: thesis: for c being Element of C st c in Y /\ (dom f) holds
|.(f /. c).| <= p

let c be Element of C; :: thesis: ( c in Y /\ (dom f) implies |.(f /. c).| <= p )
assume A5: c in Y /\ (dom f) ; :: thesis: |.(f /. c).| <= p
c in dom f by A5, XBOOLE_0:def 4;
then A6: f . c = f /. c by PARTFUN1:def 6;
|.((|.f.| | Y) . c).| = |.(|.f.| . c).| by A1, A2, A5, FUNCT_1:47
.= |.|.(f . c).|.| by VALUED_1:18 ;
hence |.(f /. c).| <= p by A1, A2, A4, A5, A6; :: thesis: verum

end;

hence ex p being Real st
for c being Element of C st c in Y /\ (dom f) holds
|.(f /. c).| <= p ; :: thesis: verum

end;

given p being Real such that A7: for c being Element of C st c in Y /\ (dom f) holds
|.(f /. c).| <= p ; :: thesis: f | Y is bounded
A8: dom |.f.| = dom f by VALUED_1:def 11;

now :: thesis: for c being object st c in dom (|.f.| | Y) holds
|.((|.f.| | Y) . c).| <= p

let c be object ; :: thesis: ( c in dom (|.f.| | Y) implies |.((|.f.| | Y) . c).| <= p )
assume A9: c in dom (|.f.| | Y) ; :: thesis: |.((|.f.| | Y) . c).| <= p
A10: c in dom |.f.| by A9, RELAT_1:57;
|.((|.f.| | Y) . c).| = |.(|.f.| . c).| by A9, FUNCT_1:47
.= |.|.(f . c).|.| by VALUED_1:18
.= |.|.(f /. c).|.| by A1, A10, PARTFUN1:def 6 ;
hence |.((|.f.| | Y) . c).| <= p by A2, A7, A8, A9; :: thesis: verum

end;

then |.f.| | Y is bounded by RFUNCT_1:72;
hence f | Y is bounded by A3, Lm3; :: thesis: verum