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

proof

A5: f " A c= omega by A1, RELAT_1:132;
A6: dom (f | (f " A)) = omega /\ (f " A) by A1, RELAT_1:61;

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

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

then A8: omega \ (f " A) = {} by XBOOLE_1:37;
then (dom (f | (f " A))) /\ (dom ((omega \ (f " A)) --> x)) = {} ;
then dom (f | (f " A)) misses dom ((omega \ (f " A)) --> x) ;
then (f | (f " A)) +* ((omega \ (f " A)) --> x) = (f | (f " A)) \/ ((omega \ (f " A)) --> x) by FUNCT_4:31;
hence rng ((f | (f " A)) +* ((omega \ (f " A)) --> x)) = (rng (f | (f " A))) \/ (rng ((omega \ (f " A)) --> x)) by RELAT_1:12
.= (rng (f | (f " A))) \/ {} by A8
.= f .: (f " A) by RELAT_1:115
.= A by A2, FUNCT_1:77 ;
:: thesis: dom ((f | (f " A)) +* ((omega \ (f " A)) --> x)) = omega
thus dom ((f | (f " A)) +* ((omega \ (f " A)) --> x)) = (dom (f | (f " A))) \/ (dom ((omega \ (f " A)) --> x)) by FUNCT_4:def 1
.= (dom (f | (f " A))) \/ {} by A8
.= omega by A6, A7 ; :: thesis: verum

end;

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

then A9: not omega \ (f " A) is empty by A5, XBOOLE_1:37;
dom ((omega \ (f " A)) --> x) = omega \ (f " A) ;
then (f | (f " A)) +* ((omega \ (f " A)) --> x) = (f | (f " A)) \/ ((omega \ (f " A)) --> x) by A6, FUNCT_4:31, XBOOLE_1:89;
hence rng ((f | (f " A)) +* ((omega \ (f " A)) --> x)) = (rng (f | (f " A))) \/ (rng ((omega \ (f " A)) --> x)) by RELAT_1:12
.= (rng (f | (f " A))) \/ {x} by A9, FUNCOP_1:8
.= (f .: (f " A)) \/ {x} by RELAT_1:115
.= A \/ {x} by A2, FUNCT_1:77
.= A by A3, ZFMISC_1:40 ;
:: thesis: dom ((f | (f " A)) +* ((omega \ (f " A)) --> x)) = omega
thus dom ((f | (f " A)) +* ((omega \ (f " A)) --> x)) = (dom (f | (f " A))) \/ (dom ((omega \ (f " A)) --> x)) by FUNCT_4:def 1
.= (omega /\ (f " A)) \/ (omega \ (f " A)) by A6
.= omega by XBOOLE_1:51 ; :: thesis: verum

end;

end;

end;

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