let E, F, G be RealNormSpace; :: thesis: for Z being Subset of E
for T being Subset of F
for u being PartFunc of E,F
for v being PartFunc of F,G st u .: Z c= T & u is_continuous_on Z & v is_continuous_on T holds
v * u is_continuous_on Z
let Z be Subset of E; :: thesis: for T being Subset of F
for u being PartFunc of E,F
for v being PartFunc of F,G st u .: Z c= T & u is_continuous_on Z & v is_continuous_on T holds
v * u is_continuous_on Z
let T be Subset of F; :: thesis: for u being PartFunc of E,F
for v being PartFunc of F,G st u .: Z c= T & u is_continuous_on Z & v is_continuous_on T holds
v * u is_continuous_on Z
let u be PartFunc of E,F; :: thesis: for v being PartFunc of F,G st u .: Z c= T & u is_continuous_on Z & v is_continuous_on T holds
v * u is_continuous_on Z
let v be PartFunc of F,G; :: thesis: ( u .: Z c= T & u is_continuous_on Z & v is_continuous_on T implies v * u is_continuous_on Z )
assume that
A1: u .: Z c= T and
A2: u is_continuous_on Z and
A3: v is_continuous_on T ; :: thesis: v * u is_continuous_on Z
set f = v * u;
A4: Z c= dom u by A2, NFCONT_1:19;
A5: T c= dom v by A3, NFCONT_1:19;

A6: now :: thesis: for x being object st x in Z holds
x in dom (v * u)

let x be object ; :: thesis: ( x in Z implies x in dom (v * u) )
assume A7: x in Z ; :: thesis: x in dom (v * u)
then u . x in u .: Z by A4, FUNCT_1:def 6;
then u . x in T by A1;
hence x in dom (v * u) by A4, A5, A7, FUNCT_1:11; :: thesis: verum

end;

for x0 being Point of E
for r being Real st x0 in Z & 0 < r holds
ex s being Real st
( 0 < s & ( for x1 being Point of E st x1 in Z & ||.(x1 - x0).|| < s holds
||.(((v * u) /. x1) - ((v * u) /. x0)).|| < r ) )

proof

let x0 be Point of E; :: thesis: for r being Real st x0 in Z & 0 < r holds
ex s being Real st
( 0 < s & ( for x1 being Point of E st x1 in Z & ||.(x1 - x0).|| < s holds
||.(((v * u) /. x1) - ((v * u) /. x0)).|| < r ) )
let r be Real; :: thesis: ( x0 in Z & 0 < r implies ex s being Real st
( 0 < s & ( for x1 being Point of E st x1 in Z & ||.(x1 - x0).|| < s holds
||.(((v * u) /. x1) - ((v * u) /. x0)).|| < r ) ) )
assume A8: ( x0 in Z & 0 < r ) ; :: thesis: ex s being Real st
( 0 < s & ( for x1 being Point of E st x1 in Z & ||.(x1 - x0).|| < s holds
||.(((v * u) /. x1) - ((v * u) /. x0)).|| < r ) )
then u . x0 in u .: Z by A4, FUNCT_1:def 6;
then u . x0 in T by A1;
then u /. x0 in T by A4, A8, PARTFUN1:def 6;
then consider t being Real such that
A9: ( 0 < t & ( for y1 being Point of F st y1 in T & ||.(y1 - (u /. x0)).|| < t holds
||.((v /. y1) - (v /. (u /. x0))).|| < r ) ) by A3, A8, NFCONT_1:19;
consider s being Real such that
A10: ( 0 < s & ( for x1 being Point of E st x1 in Z & ||.(x1 - x0).|| < s holds
||.((u /. x1) - (u /. x0)).|| < t ) ) by A2, A8, A9, NFCONT_1:19;
take s ; :: thesis: ( 0 < s & ( for x1 being Point of E st x1 in Z & ||.(x1 - x0).|| < s holds
||.(((v * u) /. x1) - ((v * u) /. x0)).|| < r ) )
thus 0 < s by A10; :: thesis: for x1 being Point of E st x1 in Z & ||.(x1 - x0).|| < s holds
||.(((v * u) /. x1) - ((v * u) /. x0)).|| < r
let x1 be Point of E; :: thesis: ( x1 in Z & ||.(x1 - x0).|| < s implies ||.(((v * u) /. x1) - ((v * u) /. x0)).|| < r )
assume that
A11: x1 in Z and
A12: ||.(x1 - x0).|| < s ; :: thesis: ||.(((v * u) /. x1) - ((v * u) /. x0)).|| < r
A13: ||.((u /. x1) - (u /. x0)).|| < t by A10, A11, A12;
u . x1 in u .: Z by A4, A11, FUNCT_1:def 6;
then u . x1 in T by A1;
then u /. x1 in T by A4, A11, PARTFUN1:def 6;
then A14: ||.((v /. (u /. x1)) - (v /. (u /. x0))).|| < r by A9, A13;
x1 in dom (v * u) by A6, A11;
then A15: v /. (u /. x1) = (v * u) /. x1 by PARTFUN2:3;
x0 in dom (v * u) by A6, A8;
hence ||.(((v * u) /. x1) - ((v * u) /. x0)).|| < r by A14, A15, PARTFUN2:3; :: thesis: verum

end;

hence v * u is_continuous_on Z by A6, NFCONT_1:19, TARSKI:def 3; :: thesis: verum