defpred S1[ 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 & S1[x,y1] & S1[x,y2] holds
y1 = y2 ;
A2: for x being object st x in G holds
ex y being object st S1[x,y]
proof
let x be object ; :: thesis: ( x in G implies ex y being object st S1[x,y] )
assume x in G ; :: thesis: ex y being object st S1[x,y]
then reconsider A = x as Subset of T ;
take f .: A ; :: thesis: S1[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
S1[x,g . x] ) ) from 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 ; :: 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 ;
ex A0 being Subset of T st
( A = A0 & g . A = f .: A0 ) by A3, A7;
hence y in rng g by ; :: thesis: verum
end;
then rng g = f .: G by TARSKI:2;
hence f .: G is finite by ; :: thesis: verum