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

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

A2: dom f = the carrier of T by FUNCT_2:def 1;

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

A is closed :: thesis: verum

( { (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 ) ) )

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

A2: dom f = the carrier of T by FUNCT_2:def 1;

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

thus
for A being Subset of T st A in { (f " {z}) where z is Element of T1 : z in rng f } holds
{ (f " {z}) where z is Element of T1 : z in rng f } c= bool the carrier of T

reconsider fz = fz as Subset-Family of T ;

A3: 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 ) ) )

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

end;proof

then reconsider fz = { (f " {z}) where z is Element of T1 : z in rng f } as Subset-Family of T ;
let y be object ; :: 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 ex z being Element of T1 st

( y = f " {z} & z in rng f ) ;

hence y in bool the carrier of T ; :: thesis: verum

end;assume y in { (f " {z}) where z is Element of T1 : z in rng f } ; :: thesis: y in bool the carrier of T

then ex z being Element of T1 st

( y = f " {z} & z in rng f ) ;

hence y in bool the carrier of T ; :: thesis: verum

reconsider fz = fz as Subset-Family of T ;

A3: 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

the carrier of T c= union fz
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

A4: A = f " {z} and

A5: z in rng f ;

consider y being object such that

A6: ( y in dom f & z = f . y ) by A5, FUNCT_1:def 3;

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

hence A <> {} by A4, A6, FUNCT_1:def 7; :: 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

A7: B = f " {w} and

w in rng f ;

end;( 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

A4: A = f " {z} and

A5: z in rng f ;

consider y being object such that

A6: ( y in dom f & z = f . y ) by A5, FUNCT_1:def 3;

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

hence A <> {} by A4, A6, FUNCT_1:def 7; :: 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

A7: B = f " {w} and

w in rng f ;

now :: thesis: ( not A misses B implies A = B )

hence
( A = B or A misses B )
; :: thesis: verumassume
not A misses B
; :: thesis: A = B

then consider v being object such that

A8: v in A and

A9: v in B by XBOOLE_0:3;

f . v in {z} by A4, A8, FUNCT_1:def 7;

then A10: f . v = z by TARSKI:def 1;

f . v in {w} by A7, A9, FUNCT_1:def 7;

hence A = B by A4, A7, A10, TARSKI:def 1; :: thesis: verum

end;then consider v being object such that

A8: v in A and

A9: v in B by XBOOLE_0:3;

f . v in {z} by A4, A8, FUNCT_1:def 7;

then A10: f . v = z by TARSKI:def 1;

f . v in {w} by A7, A9, FUNCT_1:def 7;

hence A = B by A4, A7, A10, TARSKI:def 1; :: thesis: verum

proof

then
union fz = the carrier of T
;
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in the carrier of T or y in union fz )

consider z being set such that

A11: z = f . y ;

assume A12: y in the carrier of T ; :: thesis: y in union fz

then A13: z in rng f by A2, A11, FUNCT_1:def 3;

then reconsider z = z as Element of T1 ;

A14: f " {z} in fz by A13;

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

then y in f " {z} by A2, A12, A11, FUNCT_1:def 7;

hence y in union fz by A14, TARSKI:def 4; :: thesis: verum

end;consider z being set such that

A11: z = f . y ;

assume A12: y in the carrier of T ; :: thesis: y in union fz

then A13: z in rng f by A2, A11, FUNCT_1:def 3;

then reconsider z = z as Element of T1 ;

A14: f " {z} in fz by A13;

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

then y in f " {z} by A2, A12, A11, FUNCT_1:def 7;

hence y in union fz by A14, TARSKI:def 4; :: thesis: verum

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

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

A15: A = f " {z} and

z in rng f ;

{z} is closed by A1, URYSOHN1:19;

hence A is closed by A15, PRE_TOPC:def 6; :: thesis: verum

end;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

A15: A = f " {z} and

z in rng f ;

{z} is closed by A1, URYSOHN1:19;

hence A is closed by A15, PRE_TOPC:def 6; :: thesis: verum