let Y be set ; :: thesis:
let C be non empty set ; :: thesis:
let f be PartFunc of C,COMPLEX; :: thesis:
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:

assume f | Y is bounded ; :: thesis:
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;

let c be Element of C; :: thesis:
assume A5: c in Y /\ (dom f) ; :: thesis:
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:

end;

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

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:
A8: dom |.f.| = dom f by VALUED_1:def 11;

let c be object ; :: thesis:
assume A9: c in dom (|.f.| | Y) ; :: thesis:
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:

end;

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