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