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;
A4: [#] (S | P1) = P1 by PRE_TOPC:def 5;
A5: [#] (S | P2) = P2 by PRE_TOPC:def 5;
then reconsider f1 = f as Function of T,(S | P3) by A1, A4, FUNCT_2:7;
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 P19 = P1 as non empty Subset of (S | P3) by A1, A5;
A7: [#] (S | P1) = P1 by PRE_TOPC:def 5;
reconsider P4 = F1 /\ P19 as Subset of ((S | P3) | P19) by TOPS_2:29;
A8: S | P1 = (S | P3) | P19 by A1, PRE_TOPC:7;
A9: P4 is closed by A6, Th2;
f1 " P1 = the carrier of T by A7, FUNCT_2:40
.= dom f1 by FUNCT_2:def 1 ;
then f1 " F1 = (f1 " F1) /\ (f1 " P1) by RELAT_1:132, XBOOLE_1:28
.= f " P4 by FUNCT_1:68 ;
hence f1 " F1 is closed by A2, A8, A9; :: thesis: verum

end;

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