let T, T1 be non empty TopSpace; 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; ( 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
; 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 ; 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; ( 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)))
; w c= f " {(f . x)}
A4:
dom f = the carrier of T
by FUNCT_2:def 1;
A5:
f " {(f . x)} = EqClass (x,fz)
let y be object ; TARSKI:def 3 ( not y in w or y in f " {(f . x)} )
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
; y in f " {(f . x)}
hence
y in f " {(f . x)}
by A3, A2, A5, A7, SETFAM_1:def 1; verum