let X be set ; for p being Real
for S, T being RealNormSpace
for f being PartFunc of S,T st f is_uniformly_continuous_on X holds
p (#) f is_uniformly_continuous_on X
let p be Real; for S, T being RealNormSpace
for f being PartFunc of S,T st f is_uniformly_continuous_on X holds
p (#) f is_uniformly_continuous_on X
let S, T be RealNormSpace; for f being PartFunc of S,T st f is_uniformly_continuous_on X holds
p (#) f is_uniformly_continuous_on X
let f be PartFunc of S,T; ( f is_uniformly_continuous_on X implies p (#) f is_uniformly_continuous_on X )
assume A1:
f is_uniformly_continuous_on X
; p (#) f is_uniformly_continuous_on X
then
X c= dom f
;
hence A2:
X c= dom (p (#) f)
by VFUNCT_1:def 4; NFCONT_2:def 1 for r being Real st 0 < r holds
ex s being Real st
( 0 < s & ( for x1, x2 being Point of S st x1 in X & x2 in X & ||.(x1 - x2).|| < s holds
||.(((p (#) f) /. x1) - ((p (#) f) /. x2)).|| < r ) )
now for r being Real st 0 < r holds
ex s being Real st
( 0 < s & ( for x1, x2 being Point of S st x1 in X & x2 in X & ||.(x1 - x2).|| < s holds
||.(((p (#) f) /. x1) - ((p (#) f) /. x2)).|| < r ) )per cases
( p = 0 or p <> 0 )
;
suppose A3:
p = 0
;
for r being Real st 0 < r holds
ex s being Real st
( 0 < s & ( for x1, x2 being Point of S st x1 in X & x2 in X & ||.(x1 - x2).|| < s holds
||.(((p (#) f) /. x1) - ((p (#) f) /. x2)).|| < r ) )let r be
Real;
( 0 < r implies ex s being Real st
( 0 < s & ( for x1, x2 being Point of S st x1 in X & x2 in X & ||.(x1 - x2).|| < s holds
||.(((p (#) f) /. x1) - ((p (#) f) /. x2)).|| < r ) ) )assume A4:
0 < r
;
ex s being Real st
( 0 < s & ( for x1, x2 being Point of S st x1 in X & x2 in X & ||.(x1 - x2).|| < s holds
||.(((p (#) f) /. x1) - ((p (#) f) /. x2)).|| < r ) )then consider s being
Real such that A5:
0 < s
and
for
x1,
x2 being
Point of
S st
x1 in X &
x2 in X &
||.(x1 - x2).|| < s holds
||.((f /. x1) - (f /. x2)).|| < r
by A1;
take s =
s;
( 0 < s & ( for x1, x2 being Point of S st x1 in X & x2 in X & ||.(x1 - x2).|| < s holds
||.(((p (#) f) /. x1) - ((p (#) f) /. x2)).|| < r ) )thus
0 < s
by A5;
for x1, x2 being Point of S st x1 in X & x2 in X & ||.(x1 - x2).|| < s holds
||.(((p (#) f) /. x1) - ((p (#) f) /. x2)).|| < rlet x1,
x2 be
Point of
S;
( x1 in X & x2 in X & ||.(x1 - x2).|| < s implies ||.(((p (#) f) /. x1) - ((p (#) f) /. x2)).|| < r )assume that A6:
x1 in X
and A7:
x2 in X
and
||.(x1 - x2).|| < s
;
||.(((p (#) f) /. x1) - ((p (#) f) /. x2)).|| < r||.(((p (#) f) /. x1) - ((p (#) f) /. x2)).|| =
||.((p * (f /. x1)) - ((p (#) f) /. x2)).||
by A2, A6, VFUNCT_1:def 4
.=
||.((0. T) - ((p (#) f) /. x2)).||
by A3, RLVECT_1:10
.=
||.((0. T) - (p * (f /. x2))).||
by A2, A7, VFUNCT_1:def 4
.=
||.((0. T) - (0. T)).||
by A3, RLVECT_1:10
.=
||.(0. T).||
by RLVECT_1:13
.=
0
by NORMSP_0:def 6
;
hence
||.(((p (#) f) /. x1) - ((p (#) f) /. x2)).|| < r
by A4;
verum end; suppose A8:
p <> 0
;
for r being Real st 0 < r holds
ex s being Real st
( 0 < s & ( for x1, x2 being Point of S st x1 in X & x2 in X & ||.(x1 - x2).|| < s holds
||.(((p (#) f) /. x1) - ((p (#) f) /. x2)).|| < r ) )then A9:
0 <> |.p.|
by COMPLEX1:47;
let r be
Real;
( 0 < r implies ex s being Real st
( 0 < s & ( for x1, x2 being Point of S st x1 in X & x2 in X & ||.(x1 - x2).|| < s holds
||.(((p (#) f) /. x1) - ((p (#) f) /. x2)).|| < r ) ) )A10:
0 < |.p.|
by A8, COMPLEX1:47;
assume
0 < r
;
ex s being Real st
( 0 < s & ( for x1, x2 being Point of S st x1 in X & x2 in X & ||.(x1 - x2).|| < s holds
||.(((p (#) f) /. x1) - ((p (#) f) /. x2)).|| < r ) )then
0 < r / |.p.|
by A10, XREAL_1:139;
then consider s being
Real such that A11:
0 < s
and A12:
for
x1,
x2 being
Point of
S st
x1 in X &
x2 in X &
||.(x1 - x2).|| < s holds
||.((f /. x1) - (f /. x2)).|| < r / |.p.|
by A1;
take s =
s;
( 0 < s & ( for x1, x2 being Point of S st x1 in X & x2 in X & ||.(x1 - x2).|| < s holds
||.(((p (#) f) /. x1) - ((p (#) f) /. x2)).|| < r ) )thus
0 < s
by A11;
for x1, x2 being Point of S st x1 in X & x2 in X & ||.(x1 - x2).|| < s holds
||.(((p (#) f) /. x1) - ((p (#) f) /. x2)).|| < rlet x1,
x2 be
Point of
S;
( x1 in X & x2 in X & ||.(x1 - x2).|| < s implies ||.(((p (#) f) /. x1) - ((p (#) f) /. x2)).|| < r )assume that A13:
x1 in X
and A14:
x2 in X
and A15:
||.(x1 - x2).|| < s
;
||.(((p (#) f) /. x1) - ((p (#) f) /. x2)).|| < rA16:
||.(((p (#) f) /. x1) - ((p (#) f) /. x2)).|| =
||.((p * (f /. x1)) - ((p (#) f) /. x2)).||
by A2, A13, VFUNCT_1:def 4
.=
||.((p * (f /. x1)) - (p * (f /. x2))).||
by A2, A14, VFUNCT_1:def 4
.=
||.(p * ((f /. x1) - (f /. x2))).||
by RLVECT_1:34
.=
|.p.| * ||.((f /. x1) - (f /. x2)).||
by NORMSP_1:def 1
;
|.p.| * ||.((f /. x1) - (f /. x2)).|| < (r / |.p.|) * |.p.|
by A10, A12, A13, A14, A15, XREAL_1:68;
hence
||.(((p (#) f) /. x1) - ((p (#) f) /. x2)).|| < r
by A9, A16, XCMPLX_1:87;
verum end; end; end;
hence
for r being Real st 0 < r holds
ex s being Real st
( 0 < s & ( for x1, x2 being Point of S st x1 in X & x2 in X & ||.(x1 - x2).|| < s holds
||.(((p (#) f) /. x1) - ((p (#) f) /. x2)).|| < r ) )
; verum