let Y be set ; :: thesis: for C being non empty set
for f being PartFunc of C,COMPLEX
for r being 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 Complex st f | Y is bounded holds
(r (#) f) | Y is bounded
let f be PartFunc of C,COMPLEX; :: thesis: for r being Complex st f | Y is bounded holds
(r (#) f) | Y is bounded
let r be 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:46;
then |.f.| | Y is bounded by A1, Lm3;
then (|.r.| (#) |.f.|) | Y is bounded by RFUNCT_1:80;
then ( |.(r (#) f).| | Y = |.((r (#) f) | Y).| & |.(r (#) f).| | Y is bounded ) by Th30, RFUNCT_1:46;
hence (r (#) f) | Y is bounded by Lm3; :: thesis: verum