let M be non empty set ; :: thesis: for V being ComplexNormSpace
for f being PartFunc of M,V
for z being Complex
for Y being set st f is_bounded_on Y holds
z (#) f is_bounded_on Y
let V be ComplexNormSpace; :: thesis: for f being PartFunc of M,V
for z being Complex
for Y being set st f is_bounded_on Y holds
z (#) f is_bounded_on Y
let f be PartFunc of M,V; :: thesis: for z being Complex
for Y being set st f is_bounded_on Y holds
z (#) f is_bounded_on Y
let z be Complex; :: thesis: for Y being set st f is_bounded_on Y holds
z (#) f is_bounded_on Y
let Y be set ; :: thesis: ( f is_bounded_on Y implies z (#) f is_bounded_on Y )
assume f is_bounded_on Y ; :: thesis: z (#) f is_bounded_on Y
then consider r1 being Real such that
A1: for c being Element of M st c in Y /\ (dom f) holds
||.(f /. c).|| <= r1 ;
reconsider p = |.z.| * |.r1.| as Real ;
take p ; :: according to VFUNCT_2:def 3 :: thesis: for x being Element of M st x in Y /\ (dom (z (#) f)) holds
||.((z (#) f) /. x).|| <= p
let c be Element of M; :: thesis: ( c in Y /\ (dom (z (#) f)) implies ||.((z (#) f) /. c).|| <= p )
assume A2: c in Y /\ (dom (z (#) f)) ; :: thesis: ||.((z (#) f) /. c).|| <= p
then A3: c in Y by XBOOLE_0:def 4;
A4: c in dom (z (#) f) by A2, XBOOLE_0:def 4;
then c in dom f by Def2;
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 ( |.z.| >= 0 & ||.(f /. c).|| <= |.r1.| ) by A5, COMPLEX1:46, XXREAL_0:2;
then |.z.| * ||.(f /. c).|| <= |.z.| * |.r1.| by XREAL_1:64;
then ||.(z * (f /. c)).|| <= p by CLVECT_1:def 13;
hence ||.((z (#) f) /. c).|| <= p by A4, Def2; :: thesis: verum