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 )
F: |.f.| | Y = |.(f | Y).| by RFUNCT_1:62;
G: |.(r (#) f).| | Y = |.((r (#) f) | Y).| by RFUNCT_1:62;
assume f | Y is bounded ; :: thesis: (r (#) f) | Y is bounded
then |.f.| | Y is bounded by Def3, F;
then (|.r.| (#) |.f.|) | Y is bounded by RFUNCT_1:97;
then |.(r (#) f).| | Y is bounded by Th39;
hence (r (#) f) | Y is bounded by Def3, G; :: thesis: verum