let A be non empty countable set ; :: thesis: ex f being Function of NAT,A st rng f = A
consider f being Function such that
A1: dom f = NAT and
A2: A c= rng f by Th127;
consider x being set such that
A3: x in A by XBOOLE_0:def 1;
set F = (f | (f " A)) +* ((NAT \ (f " A)) --> x);
A4: ( rng ((f | (f " A)) +* ((NAT \ (f " A)) --> x)) = A & dom ((f | (f " A)) +* ((NAT \ (f " A)) --> x)) = NAT )

proof

A5: f " A c= NAT by A1, RELAT_1:167;
A6: dom (f | (f " A)) = NAT /\ (f " A) by A1, RELAT_1:90;

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

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

then A8: NAT \ (f " A) = {} by XBOOLE_1:37;
then (dom (f | (f " A))) /\ (dom ((NAT \ (f " A)) --> x)) = {} ;
then dom (f | (f " A)) misses dom ((NAT \ (f " A)) --> x) by XBOOLE_0:def 7;
then (f | (f " A)) +* ((NAT \ (f " A)) --> x) = (f | (f " A)) \/ ((NAT \ (f " A)) --> x) by FUNCT_4:32;
hence rng ((f | (f " A)) +* ((NAT \ (f " A)) --> x)) = (rng (f | (f " A))) \/ (rng ((NAT \ (f " A)) --> x)) by RELAT_1:26
.= (rng (f | (f " A))) \/ {} by A8
.= f .: (f " A) by RELAT_1:148
.= A by A2, FUNCT_1:147 ;
:: thesis: dom ((f | (f " A)) +* ((NAT \ (f " A)) --> x)) = NAT
thus dom ((f | (f " A)) +* ((NAT \ (f " A)) --> x)) = (dom (f | (f " A))) \/ (dom ((NAT \ (f " A)) --> x)) by FUNCT_4:def 1
.= (dom (f | (f " A))) \/ {} by A8
.= NAT by A6, A7 ; :: thesis: verum

end;

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

A10: now

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

end;

dom ((NAT \ (f " A)) --> x) = NAT \ (f " A) by FUNCOP_1:19;
then (f | (f " A)) +* ((NAT \ (f " A)) --> x) = (f | (f " A)) \/ ((NAT \ (f " A)) --> x) by A6, FUNCT_4:32, XBOOLE_1:89;
hence rng ((f | (f " A)) +* ((NAT \ (f " A)) --> x)) = (rng (f | (f " A))) \/ (rng ((NAT \ (f " A)) --> x)) by RELAT_1:26
.= (rng (f | (f " A))) \/ {x} by A10, FUNCOP_1:14
.= (f .: (f " A)) \/ {x} by RELAT_1:148
.= A \/ {x} by A2, FUNCT_1:147
.= A by A3, ZFMISC_1:46 ;
:: thesis: dom ((f | (f " A)) +* ((NAT \ (f " A)) --> x)) = NAT
thus dom ((f | (f " A)) +* ((NAT \ (f " A)) --> x)) = (dom (f | (f " A))) \/ (dom ((NAT \ (f " A)) --> x)) by FUNCT_4:def 1
.= (NAT /\ (f " A)) \/ (NAT \ (f " A)) by A6, FUNCOP_1:19
.= NAT by XBOOLE_1:51 ; :: thesis: verum

end;

end;

end;

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