let S, T, W be RealNormSpace; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: ( 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 ; :: thesis: 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; :: thesis: ( 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 ; :: thesis: 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 ; :: thesis: ( 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; :: thesis: 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; :: thesis: ( 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 ) ; :: thesis: ||.(((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; :: thesis: verum

end;

hence f * g is_continuous_in x by NFCONT_1:7, P1; :: thesis: verum