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
proof
{ (f " {z}) where z is Element of T1 : z in rng f } c= bool the carrier of T
proof
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;
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 ;
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
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 ;
now :: thesis: ( not A misses B implies A = B )
assume 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;
hence ( A = B or A misses B ) ; :: thesis: verum
end;
the carrier of T c= union fz
proof
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;
then union fz = the carrier of T ;
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;
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
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;