let T, V be TopStruct ; :: thesis: for S being non empty TopStruct
for f being Function of T,S
for g being Function of S,V st f is continuous & g is continuous holds
g * f is continuous
let S be non empty TopStruct ; :: thesis: for f being Function of T,S
for g being Function of S,V st f is continuous & g is continuous holds
g * f is continuous
let f be Function of T,S; :: thesis: for g being Function of S,V st f is continuous & g is continuous holds
g * f is continuous
let g be Function of S,V; :: thesis: ( f is continuous & g is continuous implies g * f is continuous )
assume that
A1: f is continuous and
A2: g is continuous ; :: thesis: g * f is continuous
let P be Subset of V; :: according to PRE_TOPC:def 12 :: thesis: ( not P is closed or (g * f) " P is closed )
A3: (g * f) " P = f " (g " P) by RELAT_1:181;
assume P is closed ; :: thesis: (g * f) " P is closed
then g " P is closed by A2, PRE_TOPC:def 12;
hence (g * f) " P is closed by A1, A3, PRE_TOPC:def 12; :: thesis: verum