let f be Function; for Z being set st Z is finite & Z c= rng f holds
ex Y being set st
( Y c= dom f & Y is finite & f .: Y = Z )
let Z be set ; ( Z is finite & Z c= rng f implies ex Y being set st
( Y c= dom f & Y is finite & f .: Y = Z ) )
assume that
A1:
Z is finite
and
A2:
Z c= rng f
; ex Y being set st
( Y c= dom f & Y is finite & f .: Y = Z )
per cases
( Z = {} or Z <> {} )
;
suppose A4:
Z <> {}
;
ex Y being set st
( Y c= dom f & Y is finite & f .: Y = Z )deffunc H1(
object )
-> set =
f " {$1};
consider g being
Function such that A5:
dom g = Z
and A6:
for
x being
object st
x in Z holds
g . x = H1(
x)
from FUNCT_1:sch 3();
reconsider AA =
rng g as non
empty set by A4, A5, RELAT_1:42;
set ff = the
Choice_Function of
AA;
take Y = the
Choice_Function of
AA .: AA;
( Y c= dom f & Y is finite & f .: Y = Z )A7:
for
X being
set st
X in AA holds
X <> {}
then A10:
not
{} in AA
;
thus A11:
Y c= dom f
( Y is finite & f .: Y = Z )
AA = g .: Z
by A5, RELAT_1:113;
hence
Y is
finite
by A1;
f .: Y = Zset z = the
Element of
AA;
set y = the
Element of the
Element of
AA;
the
Element of
AA <> {}
by A7;
then
the
Element of the
Element of
AA in the
Element of
AA
;
then reconsider AA9 =
union AA as non
empty set by TARSKI:def 4;
reconsider f9 = the
Choice_Function of
AA as
Function of
AA,
AA9 by A10, Lm3;
A17:
dom f9 = AA
by FUNCT_2:def 1;
for
x being
object holds
(
x in f .: Y iff
x in Z )
proof
let x be
object ;
( x in f .: Y iff x in Z )
thus
(
x in f .: Y implies
x in Z )
( x in Z implies x in f .: Y )proof
assume
x in f .: Y
;
x in Z
then consider y being
object such that
y in dom f
and A18:
y in Y
and A19:
f . y = x
by FUNCT_1:def 6;
consider z being
object such that A20:
z in dom the
Choice_Function of
AA
and
z in AA
and A21:
the
Choice_Function of
AA . z = y
by A18, FUNCT_1:def 6;
consider a being
object such that A22:
a in dom g
and A23:
g . a = z
by A20, FUNCT_1:def 3;
g . a = f " {a}
by A5, A6, A22;
then
y in f " {a}
by A10, A20, A21, A23, Lm2;
then
f . y in {a}
by FUNCT_1:def 7;
hence
x in Z
by A5, A19, A22, TARSKI:def 1;
verum
end;
set y = the
Choice_Function of
AA . (g . x);
assume A24:
x in Z
;
x in f .: Y
then A25:
g . x in AA
by A5, FUNCT_1:def 3;
g . x = f " {x}
by A6, A24;
then
the
Choice_Function of
AA . (g . x) in f " {x}
by A10, A25, Lm2;
then
f . ( the Choice_Function of AA . (g . x)) in {x}
by FUNCT_1:def 7;
then A26:
f . ( the Choice_Function of AA . (g . x)) = x
by TARSKI:def 1;
the
Choice_Function of
AA . (g . x) in rng the
Choice_Function of
AA
by A17, A25, FUNCT_1:def 3;
then
the
Choice_Function of
AA . (g . x) in Y
by A17, RELAT_1:113;
hence
x in f .: Y
by A11, A26, FUNCT_1:def 6;
verum
end; hence
f .: Y = Z
by TARSKI:2;
verum end;