let T, S, V be non empty TopSpace; :: thesis: for P1 being non empty Subset of S
for P2 being Subset of S
for f being Function of T,(S | P1)
for g being Function of (S | P2),V st P1 c= P2 & f is continuous & g is continuous holds
ex h being Function of T,V st
( h = g * f & h is continuous )
let P1 be non empty Subset of S; :: thesis: for P2 being Subset of S
for f being Function of T,(S | P1)
for g being Function of (S | P2),V st P1 c= P2 & f is continuous & g is continuous holds
ex h being Function of T,V st
( h = g * f & h is continuous )
let P2 be Subset of S; :: thesis: for f being Function of T,(S | P1)
for g being Function of (S | P2),V st P1 c= P2 & f is continuous & g is continuous holds
ex h being Function of T,V st
( h = g * f & h is continuous )
let f be Function of T,(S | P1); :: thesis: for g being Function of (S | P2),V st P1 c= P2 & f is continuous & g is continuous holds
ex h being Function of T,V st
( h = g * f & h is continuous )
let g be Function of (S | P2),V; :: thesis: ( P1 c= P2 & f is continuous & g is continuous implies ex h being Function of T,V st
( h = g * f & h is continuous ) )
assume that
A1: P1 c= P2 and
A2: f is continuous and
A3: g is continuous ; :: thesis: ex h being Function of T,V st
( h = g * f & h is continuous )
reconsider P3 = P2 as non empty Subset of S by A1, XBOOLE_1:3;
reconsider g1 = g as Function of (S | P3),V ;
A4: [#] (S | P1) = P1 by PRE_TOPC:def 10;
A5: [#] (S | P2) = P2 by PRE_TOPC:def 10;
then reconsider f1 = f as Function of T,(S | P3) by A1, A4, FUNCT_2:9;
f1 is continuous

proof

for F1 being Subset of (S | P2) st F1 is closed holds
f1 " F1 is closed

proof

let F1 be Subset of (S | P2); :: thesis: ( F1 is closed implies f1 " F1 is closed )
assume A6: F1 is closed ; :: thesis: f1 " F1 is closed
reconsider P1' = P1 as non empty Subset of (S | P3) by A1, A5;
A7: [#] (S | P1) = P1 by PRE_TOPC:def 10;
reconsider P4 = F1 /\ P1' as Subset of ((S | P3) | P1') by TOPS_2:38;
A8: S | P1 = (S | P3) | P1' by A1, PRE_TOPC:28;
A9: P4 is closed by A6, Th3;
f1 " P1 = the carrier of T by A7, FUNCT_2:48
.= dom f1 by FUNCT_2:def 1 ;
then f1 " F1 = (f1 " F1) /\ (f1 " P1) by RELAT_1:167, XBOOLE_1:28
.= f " P4 by FUNCT_1:137 ;
hence f1 " F1 is closed by A2, A8, A9, PRE_TOPC:def 12; :: thesis: verum

end;

hence f1 is continuous by PRE_TOPC:def 12; :: thesis: verum

end;

then g1 * f1 is continuous by A3;
hence ex h being Function of T,V st
( h = g * f & h is continuous ) ; :: thesis: verum