let Y be set ; :: thesis: for C being non empty set
for V being RealNormSpace
for f being PartFunc of C,V
for r being Real st f is_bounded_on Y holds
r (#) f is_bounded_on Y
let C be non empty set ; :: thesis: for V being RealNormSpace
for f being PartFunc of C,V
for r being Real st f is_bounded_on Y holds
r (#) f is_bounded_on Y
let V be RealNormSpace; :: thesis: for f being PartFunc of C,V
for r being Real st f is_bounded_on Y holds
r (#) f is_bounded_on Y
let f be PartFunc of C,V; :: thesis: for r being Real st f is_bounded_on Y holds
r (#) f is_bounded_on Y
let r be Real; :: thesis: ( f is_bounded_on Y implies r (#) f is_bounded_on Y )
assume f is_bounded_on Y ; :: thesis: r (#) f is_bounded_on Y
then consider r1 being Real such that
A1: for c being Element of C st c in Y /\ (dom f) holds
||.(f /. c).|| <= r1 ;
take p = |.r.| * |.r1.|; :: according to VFUNCT_1:def 6 :: thesis: for c being Element of C st c in Y /\ (dom (r (#) f)) holds
||.((r (#) f) /. c).|| <= p
let c be Element of C; :: thesis: ( c in Y /\ (dom (r (#) f)) implies ||.((r (#) f) /. c).|| <= p )
assume A2: c in Y /\ (dom (r (#) f)) ; :: thesis: ||.((r (#) f) /. c).|| <= p
then A3: c in Y by XBOOLE_0:def 4;
A4: c in dom (r (#) f) by A2, XBOOLE_0:def 4;
then c in dom f by Def4;
then c in Y /\ (dom f) by A3, XBOOLE_0:def 4;
then A5: ||.(f /. c).|| <= r1 by A1;
r1 <= |.r1.| by ABSVALUE:4;
then ( |.r.| >= 0 & ||.(f /. c).|| <= |.r1.| ) by A5, COMPLEX1:46, XXREAL_0:2;
then |.r.| * ||.(f /. c).|| <= |.r.| * |.r1.| by XREAL_1:64;
then ||.(r * (f /. c)).|| <= p by NORMSP_1:def 1;
hence ||.((r (#) f) /. c).|| <= p by A4, Def4; :: thesis: verum