let T, T1 be non empty TopSpace; :: thesis: for f being continuous Function of T,T1 st T1 is T_1 holds
for w being set
for x being Element of T st w = EqClass (x,) holds
w c= f " {(f . x)}

let f be continuous Function of T,T1; :: thesis: ( T1 is T_1 implies for w being set
for x being Element of T st w = EqClass (x,) holds
w c= f " {(f . x)} )

assume A1: T1 is T_1 ; :: thesis: for w being set
for x being Element of T st w = EqClass (x,) holds
w c= f " {(f . x)}

then reconsider fz = { (f " {z}) where z is Element of T1 : z in rng f } as a_partition of the carrier of T by Th5;
let w be set ; :: thesis: for x being Element of T st w = EqClass (x,) holds
w c= f " {(f . x)}

let x be Element of T; :: thesis: ( w = EqClass (x,) implies w c= f " {(f . x)} )
for A being Subset of T st A in fz holds
A is closed by ;
then fz is closed by TOPS_2:def 2;
then fz in { B where B is a_partition of the carrier of T : B is closed } ;
then A2: EqClass (x,fz) in { (EqClass (x,S)) where S is a_partition of the carrier of T : S in Closed_Partitions T } ;
assume A3: w = EqClass (x,) ; :: thesis: w c= f " {(f . x)}
A4: dom f = the carrier of T by FUNCT_2:def 1;
A5: f " {(f . x)} = EqClass (x,fz)
proof
reconsider fx = f . x as Element of T1 ;
f . x in rng f by ;
then A6: f " {fx} in fz ;
f . x in {(f . x)} by TARSKI:def 1;
then x in f " {(f . x)} by ;
hence f " {(f . x)} = EqClass (x,fz) by ; :: thesis: verum
end;
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in w or y in f " {(f . x)} )
A7: EqClass (x,) = meet { (EqClass (x,S)) where S is a_partition of the carrier of T : S in Closed_Partitions T } by EQREL_1:def 8;
assume y in w ; :: thesis: y in f " {(f . x)}
hence y in f " {(f . x)} by ; :: thesis: verum