let S, T, U be RealNormSpace; :: thesis: for f1 being PartFunc of S,T
for f2 being PartFunc of T,U
for x0 being Point of S st x0 in dom (f2 * f1) & f1 is_continuous_in x0 & f2 is_continuous_in f1 /. x0 holds
f2 * f1 is_continuous_in x0
let f1 be PartFunc of S,T; :: thesis: for f2 being PartFunc of T,U
for x0 being Point of S st x0 in dom (f2 * f1) & f1 is_continuous_in x0 & f2 is_continuous_in f1 /. x0 holds
f2 * f1 is_continuous_in x0
let f2 be PartFunc of T,U; :: thesis: for x0 being Point of S st x0 in dom (f2 * f1) & f1 is_continuous_in x0 & f2 is_continuous_in f1 /. x0 holds
f2 * f1 is_continuous_in x0
let x0 be Point of S; :: thesis: ( x0 in dom (f2 * f1) & f1 is_continuous_in x0 & f2 is_continuous_in f1 /. x0 implies f2 * f1 is_continuous_in x0 )
assume that
A1: x0 in dom (f2 * f1) and
A2: f1 is_continuous_in x0 and
A3: f2 is_continuous_in f1 /. x0 ; :: thesis: f2 * f1 is_continuous_in x0
set f = f2 * f1;
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 (f2 * f1) & ||.(x1 - x0).|| < s holds
||.(((f2 * f1) /. x1) - ((f2 * f1) /. x0)).|| < 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 (f2 * f1) & ||.(x1 - x0).|| < s holds
||.(((f2 * f1) /. x1) - ((f2 * f1) /. x0)).|| < r ) ) )
assume 0 < r ; :: thesis: ex s being Real st
( 0 < s & ( for x1 being Point of S st x1 in dom (f2 * f1) & ||.(x1 - x0).|| < s holds
||.(((f2 * f1) /. x1) - ((f2 * f1) /. x0)).|| < r ) )
then consider t being Real such that
A5: ( 0 < t & ( for y1 being Point of T st y1 in dom f2 & ||.(y1 - (f1 /. x0)).|| < t holds
||.((f2 /. y1) - (f2 /. (f1 /. x0))).|| < r ) ) by A3, NFCONT_1:7;
consider s being Real such that
A6: ( 0 < s & ( for x1 being Point of S st x1 in dom f1 & ||.(x1 - x0).|| < s holds
||.((f1 /. x1) - (f1 /. x0)).|| < t ) ) by A2, A5, NFCONT_1:7;
take s ; :: thesis: ( 0 < s & ( for x1 being Point of S st x1 in dom (f2 * f1) & ||.(x1 - x0).|| < s holds
||.(((f2 * f1) /. x1) - ((f2 * f1) /. x0)).|| < r ) )
thus 0 < s by A6; :: thesis: for x1 being Point of S st x1 in dom (f2 * f1) & ||.(x1 - x0).|| < s holds
||.(((f2 * f1) /. x1) - ((f2 * f1) /. x0)).|| < r
let x1 be Point of S; :: thesis: ( x1 in dom (f2 * f1) & ||.(x1 - x0).|| < s implies ||.(((f2 * f1) /. x1) - ((f2 * f1) /. x0)).|| < r )
assume that
A7: x1 in dom (f2 * f1) and
A8: ||.(x1 - x0).|| < s ; :: thesis: ||.(((f2 * f1) /. x1) - ((f2 * f1) /. x0)).|| < r
A9: ( x1 in dom f1 & f1 . x1 in dom f2 ) by A7, FUNCT_1:11;
A10: ||.((f1 /. x1) - (f1 /. x0)).|| < t by A6, A7, A8, FUNCT_1:11;
f1 /. x1 in dom f2 by A9, PARTFUN1:def 6;
then A11: ||.((f2 /. (f1 /. x1)) - (f2 /. (f1 /. x0))).|| < r by A5, A10;
f2 /. (f1 /. x1) = (f2 * f1) /. x1 by A7, PARTFUN2:3;
hence ||.(((f2 * f1) /. x1) - ((f2 * f1) /. x0)).|| < r by A1, A11, PARTFUN2:3; :: thesis: verum

end;

hence f2 * f1 is_continuous_in x0 by A1, NFCONT_1:7; :: thesis: verum