let Z be RealNormSpace; :: thesis: for r being Real
for X being set
for f being PartFunc of REAL, the carrier of Z st f | X is bounded holds
(r (#) f) | X is bounded
let r be Real; :: thesis: for X being set
for f being PartFunc of REAL, the carrier of Z st f | X is bounded holds
(r (#) f) | X is bounded
let X be set ; :: thesis: for f being PartFunc of REAL, the carrier of Z st f | X is bounded holds
(r (#) f) | X is bounded
let f be PartFunc of REAL, the carrier of Z; :: thesis: ( f | X is bounded implies (r (#) f) | X is bounded )
assume f | X is bounded ; :: thesis: (r (#) f) | X is bounded
then consider s being Real such that
A2: for x being set st x in dom (f | X) holds
||.((f | X) /. x).|| < s ;
reconsider p = (|.r.| * |.s.|) + 1 as Real ;
take p ; :: according to INTEGR19:def 1 :: thesis: for b1 being set holds
( not b1 in dom ((r (#) f) | X) or not p <= ||.(((r (#) f) | X) /. b1).|| )
now :: thesis: for x being set st x in dom ((r (#) f) | X) holds
||.(((r (#) f) | X) /. x).|| < p
let x be set ; :: thesis: ( x in dom ((r (#) f) | X) implies ||.(((r (#) f) | X) /. x).|| < p )
assume A3: x in dom ((r (#) f) | X) ; :: thesis: ||.(((r (#) f) | X) /. x).|| < p
then A4: x in (dom (r (#) f)) /\ X by RELAT_1:61;
A5: ( x in X & x in dom (r (#) f) ) by A3, RELAT_1:57;
then A6: ( x in X & x in dom f ) by VFUNCT_1:def 4;
then A7: x in (dom f) /\ X by XBOOLE_0:def 4;
A8: ||.((f | X) /. x).|| < s by A2, A6, RELAT_1:57;
(r (#) f) /. x = r * (f /. x) by VFUNCT_1:def 4, A5;
then ((r (#) f) | X) /. x = r * (f /. x) by A4, PARTFUN2:16;
then A11: ||.(((r (#) f) | X) /. x).|| = ||.(r * ((f | X) /. x)).|| by A7, PARTFUN2:16
.= |.r.| * ||.((f | X) /. x).|| by NORMSP_1:def 1 ;
0 <= |.r.| by COMPLEX1:46;
then ( |.r.| * s <= |.r.| * |.s.| & |.r.| * ||.((f | X) /. x).|| <= |.r.| * s ) by A8, ABSVALUE:4, XREAL_1:64;
then |.r.| * ||.((f | X) /. x).|| <= |.r.| * |.s.| by XXREAL_0:2;
hence ||.(((r (#) f) | X) /. x).|| < p by A11, XREAL_1:145; :: thesis: verum
end;
hence for b1 being set holds
( not b1 in dom ((r (#) f) | X) or not p <= ||.(((r (#) f) | X) /. b1).|| ) ; :: thesis: verum