defpred S_{1}[ 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_{1}[x,y1] & S_{1}[x,y2] holds

y1 = y2 ;

A2: for x being object st x in G holds

ex y being object st S_{1}[x,y]

A3: ( dom g = G & ( for x being object st x in G holds

S_{1}[x,g . x] ) )
from FUNCT_1:sch 2(A1, A2);

for y being object holds

( y in rng g iff y in f .: G )

hence f .: G is finite by A3, FINSET_1:8; :: thesis: verum

( T = A & S = f .: A );

A1: for x, y1, y2 being object st x in G & S

y1 = y2 ;

A2: for x being object st x in G holds

ex y being object st S

proof

consider g being Function such that
let x be object ; :: thesis: ( x in G implies ex y being object st S_{1}[x,y] )

assume x in G ; :: thesis: ex y being object st S_{1}[x,y]

then reconsider A = x as Subset of T ;

take f .: A ; :: thesis: S_{1}[x,f .: A]

take A ; :: thesis: ( x = A & f .: A = f .: A )

thus ( x = A & f .: A = f .: A ) ; :: thesis: verum

end;assume x in G ; :: thesis: ex y being object st S

then reconsider A = x as Subset of T ;

take f .: A ; :: thesis: S

take A ; :: thesis: ( x = A & f .: A = f .: A )

thus ( x = A & f .: A = f .: A ) ; :: thesis: verum

A3: ( dom g = G & ( for x being object st x in G holds

S

for y being object holds

( y in rng g iff y in f .: G )

proof

then
rng g = f .: G
by TARSKI:2;
let y be object ; :: thesis: ( y in rng g iff y in f .: 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;hereby :: thesis: ( y in f .: G implies y in rng g )

assume A6:
y in f .: G
; :: thesis: y in rng gassume
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;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

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

hence f .: G is finite by A3, FINSET_1:8; :: thesis: verum