let Y be set ; :: thesis: for C being non empty set
for f being PartFunc of C,COMPLEX
for r being Element of COMPLEX st f | Y is bounded holds
(r (#) f) | Y is bounded
let C be non empty set ; :: thesis: for f being PartFunc of C,COMPLEX
for r being Element of COMPLEX st f | Y is bounded holds
(r (#) f) | Y is bounded
let f be PartFunc of C,COMPLEX ; :: thesis: for r being Element of COMPLEX st f | Y is bounded holds
(r (#) f) | Y is bounded
let r be Element of COMPLEX ; :: thesis: ( f | Y is bounded implies (r (#) f) | Y is bounded )
assume A1: f | Y is bounded ; :: thesis: (r (#) f) | Y is bounded
|.f.| | Y = |.(f | Y).| by RFUNCT_1:62;
then |.f.| | Y is bounded by A1, Lm3;
then (|.r.| (#) |.f.|) | Y is bounded by RFUNCT_1:97;
then ( |.(r (#) f).| | Y = |.((r (#) f) | Y).| & |.(r (#) f).| | Y is bounded ) by Th39, RFUNCT_1:62;
hence (r (#) f) | Y is bounded by Lm3; :: thesis: verum