let X, Y, Z be non empty TopSpace; :: thesis: for f being Function of X,Y
for g being Function of Y,Z st f is open & g is open holds
g * f is open
let f be Function of X,Y; :: thesis: for g being Function of Y,Z st f is open & g is open holds
g * f is open
let g be Function of Y,Z; :: thesis: ( f is open & g is open implies g * f is open )
assume that
A1: f is open and
A2: g is open ; :: thesis: g * f is open
let A be Subset of X; :: according to T_0TOPSP:def 2 :: thesis: ( not A is open or (g * f) .: A is open )
assume A is open ; :: thesis: (g * f) .: A is open
then A3: f .: A is open by A1, T_0TOPSP:def 2;
(g * f) .: A = g .: (f .: A) by RELAT_1:126;
hence (g * f) .: A is open by A2, A3, T_0TOPSP:def 2; :: thesis: verum