let S, T, W be RealNormSpace; for f being PartFunc of T,W
for g being Function of S,T
for x being Point of S st x in dom g & g /. x in dom f & g is_continuous_in x & f is_continuous_in g /. x holds
f * g is_continuous_in x
let f be PartFunc of T,W; for g being Function of S,T
for x being Point of S st x in dom g & g /. x in dom f & g is_continuous_in x & f is_continuous_in g /. x holds
f * g is_continuous_in x
let g be Function of S,T; for x being Point of S st x in dom g & g /. x in dom f & g is_continuous_in x & f is_continuous_in g /. x holds
f * g is_continuous_in x
let x be Point of S; ( x in dom g & g /. x in dom f & g is_continuous_in x & f is_continuous_in g /. x implies f * g is_continuous_in x )
assume that
AS1:
x in dom g
and
AS2:
g /. x in dom f
and
AS3:
g is_continuous_in x
and
AS4:
f is_continuous_in g /. x
; f * g is_continuous_in x
set h = f * g;
P1:
x in dom (f * g)
by AS1, AS2, PARTFUN2:3;
for r being Real st 0 < r holds
ex s being Real st
( 0 < s & ( for x1 being Point of S st x1 in dom (f * g) & ||.(x1 - x).|| < s holds
||.(((f * g) /. x1) - ((f * g) /. x)).|| < r ) )
proof
let r be
Real;
( 0 < r implies ex s being Real st
( 0 < s & ( for x1 being Point of S st x1 in dom (f * g) & ||.(x1 - x).|| < s holds
||.(((f * g) /. x1) - ((f * g) /. x)).|| < r ) ) )
assume
0 < r
;
ex s being Real st
( 0 < s & ( for x1 being Point of S st x1 in dom (f * g) & ||.(x1 - x).|| < s holds
||.(((f * g) /. x1) - ((f * g) /. x)).|| < r ) )
then consider t being
Real such that P2:
(
0 < t & ( for
y1 being
Point of
T st
y1 in dom f &
||.(y1 - (g /. x)).|| < t holds
||.((f /. y1) - (f /. (g /. x))).|| < r ) )
by AS4, NFCONT_1:7;
consider s being
Real such that P3:
(
0 < s & ( for
x1 being
Point of
S st
x1 in dom g &
||.(x1 - x).|| < s holds
||.((g /. x1) - (g /. x)).|| < t ) )
by P2, AS3, NFCONT_1:7;
take
s
;
( 0 < s & ( for x1 being Point of S st x1 in dom (f * g) & ||.(x1 - x).|| < s holds
||.(((f * g) /. x1) - ((f * g) /. x)).|| < r ) )
thus
0 < s
by P3;
for x1 being Point of S st x1 in dom (f * g) & ||.(x1 - x).|| < s holds
||.(((f * g) /. x1) - ((f * g) /. x)).|| < r
let x1 be
Point of
S;
( x1 in dom (f * g) & ||.(x1 - x).|| < s implies ||.(((f * g) /. x1) - ((f * g) /. x)).|| < r )
assume P4:
(
x1 in dom (f * g) &
||.(x1 - x).|| < s )
;
||.(((f * g) /. x1) - ((f * g) /. x)).|| < r
then P7:
(
x1 in dom g &
g /. x1 in dom f )
by PARTFUN2:3;
then P5:
||.((g /. x1) - (g /. x)).|| < t
by P3, P4;
(
(f * g) /. x1 = f /. (g /. x1) &
(f * g) /. x = f /. (g /. x) )
by P4, AS1, AS2, PARTFUN2:3, PARTFUN2:4;
hence
||.(((f * g) /. x1) - ((f * g) /. x)).|| < r
by P2, P5, P7;
verum
end;
hence
f * g is_continuous_in x
by NFCONT_1:7, P1; verum