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)} )

assume A1: 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)}

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,(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)} )

for A being Subset of T st A in fz holds

A is closed by A1, Th5;

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,(Intersection (Closed_Partitions T))) ; :: 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)

A7: 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 8;

assume y in w ; :: thesis: y in f " {(f . x)}

hence y in f " {(f . x)} by A3, A2, A5, A7, SETFAM_1:def 1; :: thesis: verum

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)} )

assume A1: 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)}

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,(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)} )

for A being Subset of T st A in fz holds

A is closed by A1, Th5;

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,(Intersection (Closed_Partitions T))) ; :: 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

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in w or y in f " {(f . x)} )
reconsider fx = f . x as Element of T1 ;

f . x in rng f by A4, FUNCT_1:def 3;

then A6: f " {fx} in fz ;

f . x in {(f . x)} by TARSKI:def 1;

then x in f " {(f . x)} by A4, FUNCT_1:def 7;

hence f " {(f . x)} = EqClass (x,fz) by A6, EQREL_1:def 6; :: thesis: verum

end;f . x in rng f by A4, FUNCT_1:def 3;

then A6: f " {fx} in fz ;

f . x in {(f . x)} by TARSKI:def 1;

then x in f " {(f . x)} by A4, FUNCT_1:def 7;

hence f " {(f . x)} = EqClass (x,fz) by A6, EQREL_1:def 6; :: thesis: verum

A7: 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 8;

assume y in w ; :: thesis: y in f " {(f . x)}

hence y in f " {(f . x)} by A3, A2, A5, A7, SETFAM_1:def 1; :: thesis: verum