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

hence ex h being Function of T,V st

( h = g * f & h is continuous ) by A3; :: thesis: verum

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

then
f1 is continuous
;
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;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

hence ex h being Function of T,V st

( h = g * f & h is continuous ) by A3; :: thesis: verum