let T, T1 be non empty TopSpace; :: thesis: for f being continuous Function of T,T1 st T1 is T_1 holds
( { (f " {z}) where z is Element of T1 : z in rng f } is a_partition of the carrier of T & ( for A being Subset of T st A in { (f " {z}) where z is Element of T1 : z in rng f } holds
A is closed ) )
let f be continuous Function of T,T1; :: thesis: ( T1 is T_1 implies ( { (f " {z}) where z is Element of T1 : z in rng f } is a_partition of the carrier of T & ( for A being Subset of T st A in { (f " {z}) where z is Element of T1 : z in rng f } holds
A is closed ) ) )
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: ( { (f " {z}) where z is Element of T1 : z in rng f } is a_partition of the carrier of T & ( for A being Subset of T st A in { (f " {z}) where z is Element of T1 : z in rng f } holds
A is closed ) )
thus { (f " {z}) where z is Element of T1 : z in rng f } is a_partition of the carrier of T :: thesis: for A being Subset of T st A in { (f " {z}) where z is Element of T1 : z in rng f } holds
A is closed

proof

{ (f " {z}) where z is Element of T1 : z in rng f } c= bool the carrier of T

proof

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in { (f " {z}) where z is Element of T1 : z in rng f } or y in bool the carrier of T )
assume y in { (f " {z}) where z is Element of T1 : z in rng f } ; :: thesis: y in bool the carrier of T
then consider z being Element of T1 such that
A3: ( y = f " {z} & z in rng f ) ;
thus y in bool the carrier of T by A3; :: thesis: verum

end;

then reconsider fz = { (f " {z}) where z is Element of T1 : z in rng f } as Subset-Family of T ;
reconsider fz = fz as Subset-Family of T ;
A4: union fz = the carrier of T

proof

thus union fz c= the carrier of T ; :: according to XBOOLE_0:def 10 :: thesis: the carrier of T c= union fz
thus the carrier of T c= union fz :: thesis: verum

proof

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in the carrier of T or y in union fz )
assume A5: y in the carrier of T ; :: thesis: y in union fz
consider z being set such that
A6: z = f . y ;
A7: z in rng f by A1, A5, A6, FUNCT_1:def 5;
then reconsider z = z as Element of T1 ;
A8: f " {z} in fz by A7;
f . y in {(f . y)} by TARSKI:def 1;
then y in f " {z} by A1, A5, A6, FUNCT_1:def 13;
hence y in union fz by A8, TARSKI:def 4; :: thesis: verum

end;

end;

for A being Subset of T st A in fz holds
( A <> {} & ( for B being Subset of T holds
( not B in fz or A = B or A misses B ) ) )

proof

let A be Subset of T; :: thesis: ( A in fz implies ( A <> {} & ( for B being Subset of T holds
( not B in fz or A = B or A misses B ) ) ) )
assume A in fz ; :: thesis: ( A <> {} & ( for B being Subset of T holds
( not B in fz or A = B or A misses B ) ) )
then consider z being Element of T1 such that
A9: ( A = f " {z} & z in rng f ) ;
consider y being set such that
A10: ( y in dom f & z = f . y ) by A9, FUNCT_1:def 5;
f . y in {(f . y)} by TARSKI:def 1;
hence A <> {} by A9, A10, FUNCT_1:def 13; :: thesis: for B being Subset of T holds
( not B in fz or A = B or A misses B )
let B be Subset of T; :: thesis: ( not B in fz or A = B or A misses B )
assume B in fz ; :: thesis: ( A = B or A misses B )
then consider w being Element of T1 such that
A11: ( B = f " {w} & w in rng f ) ;
thus ( A = B or A misses B ) :: thesis: verum

proof

now

assume not A misses B ; :: thesis: A = B
then consider v being set such that
A12: ( v in A & v in B ) by XBOOLE_0:3;
( f . v in {z} & f . v in {w} ) by A9, A11, A12, FUNCT_1:def 13;
then ( f . v = z & f . v = w ) by TARSKI:def 1;
hence A = B by A9, A11; :: thesis: verum

end;

hence ( A = B or A misses B ) ; :: thesis: verum

end;

end;

hence { (f " {z}) where z is Element of T1 : z in rng f } is a_partition of the carrier of T by A4, EQREL_1:def 6; :: thesis: verum

end;

thus for A being Subset of T st A in { (f " {z}) where z is Element of T1 : z in rng f } holds
A is closed :: thesis: verum

proof

let A be Subset of T; :: thesis: ( A in { (f " {z}) where z is Element of T1 : z in rng f } implies A is closed )
assume A in { (f " {z}) where z is Element of T1 : z in rng f } ; :: thesis: A is closed
then consider z being Element of T1 such that
A13: ( A = f " {z} & z in rng f ) ;
{z} is closed by A2, URYSOHN1:27;
hence A is closed by A13, PRE_TOPC:def 12; :: thesis: verum

end;