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)
proof
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;
let y be object ; :: according to TARSKI:def 3 :: thesis: ( 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 ; :: thesis: y in f " {(f . x)}
hence y in f " {(f . x)} by A3, A2, A5, A7, SETFAM_1:def 1; :: thesis: verum