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 b_{1} being set holds

( not b_{1} in dom ((r (#) f) | X) or not p <= ||.(((r (#) f) | X) /. b_{1}).|| )

_{1} being set holds

( not b_{1} in dom ((r (#) f) | X) or not p <= ||.(((r (#) f) | X) /. b_{1}).|| )
; :: thesis: verum

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 b

( not b

now :: thesis: for x being set st x in dom ((r (#) f) | X) holds

||.(((r (#) f) | X) /. x).|| < p

hence
for b||.(((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;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

( not b