thus
( not IT is countable or IT is empty or ex F being sequence of D st IT = rng F )
:: thesis: ( ( IT is empty or ex F being sequence of D st IT = rng F ) implies IT is countable )

proof

assume A12:
( IT is empty or ex F being sequence of D st IT = rng F )
; :: thesis: IT is countable
assume that

A1: IT is countable and

A2: not IT is empty ; :: thesis: ex F being sequence of D st IT = rng F

consider f being Function such that

A3: dom f = NAT and

A4: IT c= rng f by A1, CARD_3:93;

consider x being Element of D such that

A5: x in IT by A2;

set F = (f | (f " IT)) +* ((NAT \ (f " IT)) --> x);

A6: ( rng ((f | (f " IT)) +* ((NAT \ (f " IT)) --> x)) = IT & dom ((f | (f " IT)) +* ((NAT \ (f " IT)) --> x)) = NAT )

take F ; :: thesis: IT = rng F

thus IT = rng F by A6; :: thesis: verum

end;A1: IT is countable and

A2: not IT is empty ; :: thesis: ex F being sequence of D st IT = rng F

consider f being Function such that

A3: dom f = NAT and

A4: IT c= rng f by A1, CARD_3:93;

consider x being Element of D such that

A5: x in IT by A2;

set F = (f | (f " IT)) +* ((NAT \ (f " IT)) --> x);

A6: ( rng ((f | (f " IT)) +* ((NAT \ (f " IT)) --> x)) = IT & dom ((f | (f " IT)) +* ((NAT \ (f " IT)) --> x)) = NAT )

proof

then reconsider F = (f | (f " IT)) +* ((NAT \ (f " IT)) --> x) as sequence of D by FUNCT_2:def 1, RELSET_1:4;
A7:
f " IT c= NAT
by A3, RELAT_1:132;

A8: dom (f | (f " IT)) = NAT /\ (f " IT) by A3, RELAT_1:61;

end;A8: dom (f | (f " IT)) = NAT /\ (f " IT) by A3, RELAT_1:61;

per cases
( NAT = f " IT or NAT <> f " IT )
;

end;

suppose A9:
NAT = f " IT
; :: thesis: ( rng ((f | (f " IT)) +* ((NAT \ (f " IT)) --> x)) = IT & dom ((f | (f " IT)) +* ((NAT \ (f " IT)) --> x)) = NAT )

then A10:
NAT \ (f " IT) = {}
by XBOOLE_1:37;

then dom ((NAT \ (f " IT)) --> x) = {} ;

then dom (f | (f " IT)) misses dom ((NAT \ (f " IT)) --> x) ;

then (f | (f " IT)) +* ((NAT \ (f " IT)) --> x) = (f | (f " IT)) \/ ((NAT \ (f " IT)) --> x) by FUNCT_4:31;

hence rng ((f | (f " IT)) +* ((NAT \ (f " IT)) --> x)) = (rng (f | (f " IT))) \/ (rng ((NAT \ (f " IT)) --> x)) by RELAT_1:12

.= (rng (f | (f " IT))) \/ {} by A10

.= f .: (f " IT) by RELAT_1:115

.= IT by A4, FUNCT_1:77 ;

:: thesis: dom ((f | (f " IT)) +* ((NAT \ (f " IT)) --> x)) = NAT

thus dom ((f | (f " IT)) +* ((NAT \ (f " IT)) --> x)) = (dom (f | (f " IT))) \/ (dom ((NAT \ (f " IT)) --> x)) by FUNCT_4:def 1

.= (dom (f | (f " IT))) \/ {} by A10

.= NAT by A3, A9 ; :: thesis: verum

end;then dom ((NAT \ (f " IT)) --> x) = {} ;

then dom (f | (f " IT)) misses dom ((NAT \ (f " IT)) --> x) ;

then (f | (f " IT)) +* ((NAT \ (f " IT)) --> x) = (f | (f " IT)) \/ ((NAT \ (f " IT)) --> x) by FUNCT_4:31;

hence rng ((f | (f " IT)) +* ((NAT \ (f " IT)) --> x)) = (rng (f | (f " IT))) \/ (rng ((NAT \ (f " IT)) --> x)) by RELAT_1:12

.= (rng (f | (f " IT))) \/ {} by A10

.= f .: (f " IT) by RELAT_1:115

.= IT by A4, FUNCT_1:77 ;

:: thesis: dom ((f | (f " IT)) +* ((NAT \ (f " IT)) --> x)) = NAT

thus dom ((f | (f " IT)) +* ((NAT \ (f " IT)) --> x)) = (dom (f | (f " IT))) \/ (dom ((NAT \ (f " IT)) --> x)) by FUNCT_4:def 1

.= (dom (f | (f " IT))) \/ {} by A10

.= NAT by A3, A9 ; :: thesis: verum

suppose
NAT <> f " IT
; :: thesis: ( rng ((f | (f " IT)) +* ((NAT \ (f " IT)) --> x)) = IT & dom ((f | (f " IT)) +* ((NAT \ (f " IT)) --> x)) = NAT )

then A11:
not NAT \ (f " IT) is empty
by A7, XBOOLE_1:37;

dom ((NAT \ (f " IT)) --> x) = NAT \ (f " IT) by FUNCOP_1:13;

then (f | (f " IT)) +* ((NAT \ (f " IT)) --> x) = (f | (f " IT)) \/ ((NAT \ (f " IT)) --> x) by A8, FUNCT_4:31, XBOOLE_1:89;

hence rng ((f | (f " IT)) +* ((NAT \ (f " IT)) --> x)) = (rng (f | (f " IT))) \/ (rng ((NAT \ (f " IT)) --> x)) by RELAT_1:12

.= (rng (f | (f " IT))) \/ {x} by A11, FUNCOP_1:8

.= (f .: (f " IT)) \/ {x} by RELAT_1:115

.= IT \/ {x} by A4, FUNCT_1:77

.= IT by A5, ZFMISC_1:40 ;

:: thesis: dom ((f | (f " IT)) +* ((NAT \ (f " IT)) --> x)) = NAT

thus dom ((f | (f " IT)) +* ((NAT \ (f " IT)) --> x)) = (dom (f | (f " IT))) \/ (dom ((NAT \ (f " IT)) --> x)) by FUNCT_4:def 1

.= (NAT /\ (f " IT)) \/ (NAT \ (f " IT)) by A8, FUNCOP_1:13

.= NAT by XBOOLE_1:51 ; :: thesis: verum

end;dom ((NAT \ (f " IT)) --> x) = NAT \ (f " IT) by FUNCOP_1:13;

then (f | (f " IT)) +* ((NAT \ (f " IT)) --> x) = (f | (f " IT)) \/ ((NAT \ (f " IT)) --> x) by A8, FUNCT_4:31, XBOOLE_1:89;

hence rng ((f | (f " IT)) +* ((NAT \ (f " IT)) --> x)) = (rng (f | (f " IT))) \/ (rng ((NAT \ (f " IT)) --> x)) by RELAT_1:12

.= (rng (f | (f " IT))) \/ {x} by A11, FUNCOP_1:8

.= (f .: (f " IT)) \/ {x} by RELAT_1:115

.= IT \/ {x} by A4, FUNCT_1:77

.= IT by A5, ZFMISC_1:40 ;

:: thesis: dom ((f | (f " IT)) +* ((NAT \ (f " IT)) --> x)) = NAT

thus dom ((f | (f " IT)) +* ((NAT \ (f " IT)) --> x)) = (dom (f | (f " IT))) \/ (dom ((NAT \ (f " IT)) --> x)) by FUNCT_4:def 1

.= (NAT /\ (f " IT)) \/ (NAT \ (f " IT)) by A8, FUNCOP_1:13

.= NAT by XBOOLE_1:51 ; :: thesis: verum

take F ; :: thesis: IT = rng F

thus IT = rng F by A6; :: thesis: verum