let S, T, W be RealNormSpace; :: thesis:
let f be PartFunc of T,W; :: thesis:
let g be Function of S,T; :: thesis:
let x be Point of S; :: thesis:
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:
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 ) )

let r be Real; :: thesis:
assume 0 < r ; :: thesis:
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:
thus 0 < s by P3; :: thesis:
let x1 be Point of S; :: thesis:
assume P4: ( x1 in dom (f * g) & ||.(x1 - x).|| < s ) ; :: thesis:
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:

end;