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

proof

assume that
A1: IT is countable and
A2: not IT is empty ; :: thesis: ex F being Function of NAT ,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:127;
consider x being Element of D such that
A5: x in IT by A2, SUBSET_1:10;
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

A7: f " IT c= NAT by A3, RELAT_1:167;
A8: dom (f | (f " IT)) = NAT /\ (f " IT) by A3, RELAT_1:90;

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

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))) /\ (dom ((NAT \ (f " IT)) --> x)) = {} ;
then dom (f | (f " IT)) misses dom ((NAT \ (f " IT)) --> x) by XBOOLE_0:def 7;
then (f | (f " IT)) +* ((NAT \ (f " IT)) --> x) = (f | (f " IT)) \/ ((NAT \ (f " IT)) --> x) by FUNCT_4:32;
hence rng ((f | (f " IT)) +* ((NAT \ (f " IT)) --> x)) = (rng (f | (f " IT))) \/ (rng ((NAT \ (f " IT)) --> x)) by RELAT_1:26
.= (rng (f | (f " IT))) \/ {} by A10
.= f .: (f " IT) by RELAT_1:148
.= IT by A4, FUNCT_1:147 ;
:: 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 A8, A9 ; :: thesis: verum

end;

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

A12: now

assume NAT \ (f " IT) is empty ; :: thesis: contradiction
then NAT c= f " IT by XBOOLE_1:37;
hence contradiction by A7, A11, XBOOLE_0:def 10; :: thesis: verum

end;

dom ((NAT \ (f " IT)) --> x) = NAT \ (f " IT) by FUNCOP_1:19;
then (f | (f " IT)) +* ((NAT \ (f " IT)) --> x) = (f | (f " IT)) \/ ((NAT \ (f " IT)) --> x) by A8, FUNCT_4:32, XBOOLE_1:89;
hence rng ((f | (f " IT)) +* ((NAT \ (f " IT)) --> x)) = (rng (f | (f " IT))) \/ (rng ((NAT \ (f " IT)) --> x)) by RELAT_1:26
.= (rng (f | (f " IT))) \/ {x} by A12, FUNCOP_1:14
.= (f .: (f " IT)) \/ {x} by RELAT_1:148
.= IT \/ {x} by A4, FUNCT_1:147
.= IT by A5, ZFMISC_1:46 ;
:: 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:19
.= NAT by XBOOLE_1:51 ; :: thesis: verum

end;

end;

end;

then reconsider F = (f | (f " IT)) +* ((NAT \ (f " IT)) --> x) as Function of NAT ,D by FUNCT_2:def 1, RELSET_1:11;
take F ; :: thesis: IT = rng F
thus IT = rng F by A6; :: thesis: verum

end;

assume A13: ( IT is empty or ex F being Function of NAT ,D st IT = rng F ) ; :: thesis: IT is countable

per cases ( IT is empty or not IT is empty ) ;

suppose IT is empty ; :: thesis: IT is countable

hence IT is countable by CARD_4:43; :: thesis: verum

end;

suppose not IT is empty ; :: thesis: IT is countable

then consider F being Function of NAT ,D such that
A14: IT = rng F by A13;
dom F = NAT by FUNCT_2:def 1;
hence IT is countable by A14, CARD_3:127; :: thesis: verum

end;

end;