let X be TopStruct ; :: thesis: for S, V being non empty TopStruct
for B being non empty Subset of S
for f being Function of X,(S | B)
for g being Function of S,V
for h being Function of X,V st h = g * f & f is continuous & g is continuous holds
h is continuous
let S, V be non empty TopStruct ; :: thesis: for B being non empty Subset of S
for f being Function of X,(S | B)
for g being Function of S,V
for h being Function of X,V st h = g * f & f is continuous & g is continuous holds
h is continuous
let B be non empty Subset of S; :: thesis: for f being Function of X,(S | B)
for g being Function of S,V
for h being Function of X,V st h = g * f & f is continuous & g is continuous holds
h is continuous
let f be Function of X,(S | B); :: thesis: for g being Function of S,V
for h being Function of X,V st h = g * f & f is continuous & g is continuous holds
h is continuous
let g be Function of S,V; :: thesis: for h being Function of X,V st h = g * f & f is continuous & g is continuous holds
h is continuous
let h be Function of X,V; :: thesis: ( h = g * f & f is continuous & g is continuous implies h is continuous )
assume that
A1: h = g * f and
A2: f is continuous and
A3: g is continuous ; :: thesis: h is continuous

now :: thesis: for P being Subset of V st P is closed holds
h " P is closed

let P be Subset of V; :: thesis: ( P is closed implies h " P is closed )
A4: (g * f) " P = f " (g " P) by RELAT_1:146;

now :: thesis: ( P is closed implies h " P is closed )

assume P is closed ; :: thesis: h " P is closed
then A5: g " P is closed by A3, PRE_TOPC:def 6;
A6: the carrier of (S | B) = B by PRE_TOPC:8;
then reconsider F = B /\ (g " P) as Subset of (S | B) by XBOOLE_1:17;
A7: (rng f) /\ the carrier of (S | B) = rng f by XBOOLE_1:28;
[#] (S | B) = B by PRE_TOPC:def 5;
then A8: F is closed by A5, PRE_TOPC:13;
h " P = f " ((rng f) /\ (g " P)) by A1, A4, RELAT_1:133
.= f " ((rng f) /\ ( the carrier of (S | B) /\ (g " P))) by A7, XBOOLE_1:16
.= f " F by A6, RELAT_1:133 ;
hence h " P is closed by A2, A8, PRE_TOPC:def 6; :: thesis: verum

end;

hence ( P is closed implies h " P is closed ) ; :: thesis: verum

end;

hence h is continuous by PRE_TOPC:def 6; :: thesis: verum