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 number 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 number 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 number 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:90;
A3: |.f.| | Y = |.(f | Y).| by RFUNCT_1:62;

hereby :: thesis: ( ex p being real number 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 number 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 number such that
A4: for c being set st c in dom (|.f.| | Y) holds
abs ((|.f.| | Y) . c) <= p by RFUNCT_1:89;

now

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 8;
abs ((|.f.| | Y) . c) = abs (|.f.| . c) by A1, A2, A5, FUNCT_1:70
.= abs |.(f . c).| by VALUED_1:18 ;
hence |.(f /. c).| <= p by A1, A2, A4, A5, A6; :: thesis: verum

end;

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

end;

given p being real number 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

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

end;

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