defpred S₁[ object , object ] means ex A being Subset of T st
( T = A & S = f .: A );
A1: for x, y1, y2 being object st x in G & S₁[x,y1] & S₁[x,y2] holds
y1 = y2 ;
A2: for x being object st x in G holds
ex y being object st S₁[x,y]

proof

let x be object ; :: thesis: ( x in G implies ex y being object st S₁[x,y] )
assume x in G ; :: thesis: ex y being object st S₁[x,y]
then reconsider A = x as Subset of T ;
take f .: A ; :: thesis: S₁[x,f .: A]
take A ; :: thesis: ( x = A & f .: A = f .: A )
thus ( x = A & f .: A = f .: A ) ; :: thesis: verum

end;

consider g being Function such that
A3: ( dom g = G & ( for x being object st x in G holds
S₁[x,g . x] ) ) from FUNCT_1:sch 2(A1, A2);
for y being object holds
( y in rng g iff y in f .: G )

proof

let y be object ; :: thesis: ( y in rng g iff y in f .: G )

hereby :: thesis: ( y in f .: G implies y in rng g )

assume y in rng g ; :: thesis: y in f .: G
then consider x being object such that
A4: ( x in dom g & g . x = y ) by FUNCT_1:def 3;
ex A being Subset of T st
( x = A & y = f .: A ) by A3, A4;
hence y in f .: G by A3, A4, FUNCT_2:def 10; :: thesis: verum

end;

assume A6: y in f .: G ; :: thesis: y in rng g
then reconsider B = y as Subset of S ;
consider A being Subset of T such that
A7: ( A in G & B = f .: A ) by A6, FUNCT_2:def 10;
ex A0 being Subset of T st
( A = A0 & g . A = f .: A0 ) by A3, A7;
hence y in rng g by A3, A7, FUNCT_1:def 3; :: thesis: verum

end;

then rng g = f .: G by TARSKI:2;
hence f .: G is finite by A3, FINSET_1:8; :: thesis: verum