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,(Intersection (Closed_Partitions T)) 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,(Intersection (Closed_Partitions T)) holds
w c= f " {(f . x)} )
A1: ( dom f = the carrier of T & rng f c= the carrier of T1 ) by FUNCT_2:def 1;
assume A2: T1 is T_1 ; :: thesis: for w being set
for x being Element of T st w = EqClass x,(Intersection (Closed_Partitions T)) holds
w c= f " {(f . x)}
let w be set ; :: thesis: for x being Element of T st w = EqClass x,(Intersection (Closed_Partitions T)) holds
w c= f " {(f . x)}
let x be Element of T; :: thesis: ( w = EqClass x,(Intersection (Closed_Partitions T)) implies w c= f " {(f . x)} )
assume A3: w = EqClass x,(Intersection (Closed_Partitions T)) ; :: thesis: w c= f " {(f . x)}
let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in w or y in f " {(f . x)} )
assume A4: y in w ; :: thesis: y in f " {(f . x)}
reconsider fz = { (f " {z}) where z is Element of T1 : z in rng f } as a_partition of the carrier of T by A2, Th13;
for A being Subset of T st A in fz holds
A is closed by A2, Th13;
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 A5: EqClass x,fz in { (EqClass x,S) where S is a_partition of the carrier of T : S in Closed_Partitions T } ;
A6: f " {(f . x)} = EqClass x,fz

proof

f . x in {(f . x)} by TARSKI:def 1;
then A7: x in f " {(f . x)} by A1, FUNCT_1:def 13;
A8: f . x in rng f by A1, FUNCT_1:def 5;
reconsider fx = f . x as Element of T1 ;
f " {fx} in fz by A8;
hence f " {(f . x)} = EqClass x,fz by A7, EQREL_1:def 8; :: thesis: verum

end;

EqClass x,(Intersection (Closed_Partitions T)) = meet { (EqClass x,S) where S is a_partition of the carrier of T : S in Closed_Partitions T } by EQREL_1:def 11;
hence y in f " {(f . x)} by A3, A4, A5, A6, SETFAM_1:def 1; :: thesis: verum