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 6 :: thesis: ( not P is closed or (g * f) " P is closed )
assume P is closed ; :: thesis: (g * f) " P is closed
then ( (g * f) " P = f " (g " P) & g " P is closed ) by A2, RELAT_1:146;
hence (g * f) " P is closed by A1; :: thesis: verum