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 ) ; :: thesis: f .: Y = Z
thus f .: Y = Z by A3; :: thesis: verum
end;
suppose A4: Z <> {} ; :: thesis: 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; :: thesis: ( Y c= dom f & Y is finite & f .: Y = Z )
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 object such that
A8: x in dom g and
A9: g . x = X by FUNCT_1:def 3;
g . x = f " {x} by A5, A6, A8;
hence X <> {} by A2, A5, A8, A9, FUNCT_1:72; :: thesis: verum
end;
then A10: not {} in AA ;
thus A11: Y c= dom f :: thesis: ( Y is finite & f .: Y = Z )
proof
let x be object ; :: 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 object such that
y in dom the Choice_Function of AA and
A12: y in AA and
A13: the Choice_Function of AA . y = x by FUNCT_1:def 6;
y in g .: Z by A5, A12, RELAT_1:113;
then consider z being object such that
z in dom g and
A14: z in Z and
A15: g . z = y by FUNCT_1:def 6;
A16: g . z = f " {z} by A6, A14;
x in g . z by A10, A12, A13, A15, Lm2;
hence x in dom f by A16, FUNCT_1:def 7; :: thesis: verum
end;
AA = g .: Z by A5, RELAT_1:113;
hence Y is finite by A1; :: thesis: f .: Y = Z
set 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 ; :: 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 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; :: thesis: verum
end;
set y = the Choice_Function of AA . (g . x);
assume A24: x in Z ; :: thesis: 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; :: thesis: verum
end;
hence f .: Y = Z by TARSKI:2; :: thesis: verum
end;
end;