let A be Subset of B; :: thesis:

per cases ;

suppose A is empty ; :: thesis:

hence A is finite ; :: thesis:

end;

suppose not A is empty ; :: thesis:

then consider x1 being object such that
A1: x1 in A ;
consider p being Function such that
A2: rng p = B and
A3: dom p in omega by Def1;
deffunc H₁( object ) -> set = p . B;
deffunc H₂( object ) -> object = x1;
defpred S₁[ object ] means p . B in A;
consider q being Function such that
A4: dom q = dom p and
A5: for x being object st x in dom p holds
( ( S₁[x] implies q . x = H₁(x) ) & ( not S₁[x] implies q . x = H₂(x) ) ) from PARTFUN1:sch 1();

now :: thesis:

let y be object ; :: thesis:
thus ( y in A implies ex x being object st
( x in dom q & y = q . x ) ) :: thesis:

proof

assume A6: y in A ; :: thesis:
then consider x being object such that
A7: x in dom p and
A8: p . x = y by A2, FUNCT_1:def 3;
take x ; :: thesis:
thus x in dom q by A4, A7; :: thesis:
thus y = q . x by A5, A6, A7, A8; :: thesis:

end;

given x being object such that A9: x in dom q and
A10: y = q . x ; :: thesis:

per cases ;

suppose p . x in A ; :: thesis:

hence y in A by A4, A5, A9, A10; :: thesis:

end;

suppose not p . x in A ; :: thesis:

hence y in A by A1, A4, A5, A9, A10; :: thesis:

end;

end;

end;

then rng q = A by FUNCT_1:def 3;
hence A is finite by A3, A4; :: thesis:

end;

end;