let f be Function; :: thesis: 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 ; :: thesis: ( 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 ; :: thesis: ex Y being set st
( Y c= dom f & Y is finite & f .: Y = Z )

per cases ( Z = {} or Z <> {} ) ;

suppose A3: Z = {} ; :: thesis: ex Y being set st
( Y c= dom f & Y is finite & f .: Y = Z )

take Y = {} ; :: thesis: ( Y c= dom f & Y is finite & f .: Y = Z )
thus ( Y c= dom f & Y is finite ) by XBOOLE_1:2; :: thesis: f .: Y = Z
thus f .: Y = Z by A3, RELAT_1:149; :: thesis: verum

end;

suppose A4: Z <> {} ; :: thesis: ex Y being set st
( Y c= dom f & Y is finite & f .: Y = Z )

deffunc H₁( set ) -> set = f " {$1};
consider g being Function such that
A5: dom g = Z and
A6: for x being set st x in Z holds
g . x = H₁(x) from FUNCT_1:sch 3();
reconsider AA = rng g as non empty set by A4, A5, RELAT_1:65;
A7: for X being set st X in AA holds
X <> {}

proof

let X be set ; :: thesis: ( X in AA implies X <> {} )
assume X in AA ; :: thesis: X <> {}
then consider x being set such that
A8: x in dom g and
A9: g . x = X by FUNCT_1:def 5;
g . x = f " {x} by A5, A6, A8;
hence X <> {} by A2, A5, A8, A9, FUNCT_1:142; :: thesis: verum

end;

then A10: not {} in AA ;
consider ff being Choice_Function of AA;
consider z being Element of AA;
A11: z <> {} by A7;
consider y being Element of z;
y in z by A11;
then reconsider AA' = union AA as non empty set by TARSKI:def 4;
reconsider f' = ff as Function of AA,AA' ;
A12: dom f' = AA by FUNCT_2:def 1;
take Y = ff .: AA; :: thesis: ( Y c= dom f & Y is finite & f .: Y = Z )
thus A13: Y c= dom f :: thesis: ( Y is finite & f .: Y = Z )

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in Y or x in dom f )
assume x in Y ; :: thesis: x in dom f
then consider y being set such that
y in dom ff and
A14: y in AA and
A15: ff . y = x by FUNCT_1:def 12;
y in g .: Z by A5, A14, RELAT_1:146;
then consider z being set such that
A16: ( z in dom g & z in Z ) and
A17: g . z = y by FUNCT_1:def 12;
A18: g . z = f " {z} by A6, A16;
x in g . z by A10, A14, A15, A17, Def1;
hence x in dom f by A18, FUNCT_1:def 13; :: thesis: verum

end;

AA = g .: Z by A5, RELAT_1:146;
then AA is finite by A1;
hence Y is finite ; :: thesis: f .: Y = Z
for x being set holds
( x in f .: Y iff x in Z )

proof

let x be set ; :: thesis: ( x in f .: Y iff x in Z )
thus ( x in f .: Y implies x in Z ) :: thesis: ( x in Z implies x in f .: Y )

proof

assume x in f .: Y ; :: thesis: x in Z
then consider y being set such that
y in dom f and
A19: y in Y and
A20: f . y = x by FUNCT_1:def 12;
consider z being set such that
A21: ( z in dom ff & z in AA ) and
A22: ff . z = y by A19, FUNCT_1:def 12;
consider a being set such that
A23: a in dom g and
A24: g . a = z by A21, FUNCT_1:def 5;
g . a = f " {a} by A5, A6, A23;
then y in f " {a} by A10, A21, A22, A24, Def1;
then f . y in {a} by FUNCT_1:def 13;
hence x in Z by A5, A20, A23, TARSKI:def 1; :: thesis: verum

end;

assume A25: x in Z ; :: thesis: x in f .: Y
set y = ff . (g . x);
A26: g . x in AA by A5, A25, FUNCT_1:def 5;
then ff . (g . x) in rng ff by A12, FUNCT_1:def 5;
then A27: ff . (g . x) in Y by A12, RELAT_1:146;
g . x = f " {x} by A6, A25;
then ff . (g . x) in f " {x} by A10, A26, Def1;
then f . (ff . (g . x)) in {x} by FUNCT_1:def 13;
then ( ff . (g . x) in dom f & ff . (g . x) in Y & f . (ff . (g . x)) = x ) by A13, A27, TARSKI:def 1;
hence x in f .: Y by FUNCT_1:def 12; :: thesis: verum

end;

hence f .: Y = Z by TARSKI:2; :: thesis: verum

end;

end;