let A be Subset of B; :: thesis: A is finite

per cases ( A is empty or not A is empty ) ;

suppose A is empty ; :: thesis: A is finite

hence A is finite ; :: thesis: verum

end;

suppose not A is empty ; :: thesis: A is finite

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: for y being object holds
( ( y in A implies ex x being object st
( x in dom q & y = q . x ) ) & ( ex x being object st
( x in dom q & y = q . x ) implies y in A ) )

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

proof

assume A6: y in A ; :: thesis: ex x being object st
( x in dom q & y = q . x )
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: ( x in dom q & y = q . x )
thus x in dom q by A4, A7; :: thesis: y = q . x
thus y = q . x by A5, A6, A7, A8; :: thesis: verum

end;

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

per cases ( p . x in A or not p . x in A ) ;

suppose p . x in A ; :: thesis: b₁ in A

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

end;

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

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

end;

end;

end;

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

end;

end;