deffunc H₁( object ) -> set = $1 `1 ;
let X be finite set ; :: thesis: ( proj1 X is finite & proj2 X is finite )
consider f being Function such that
A1: ( dom f = X & ( for x being object st x in X holds
f . x = H₁(x) ) ) from FUNCT_1:sch 3();
A2: proj1 X c= rng f

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in proj1 X or x in rng f )
assume x in proj1 X ; :: thesis: x in rng f
then consider y being object such that
A3: [x,y] in X by XTUPLE_0:def 12;
[x,y] `1 = x ;
then f . [x,y] = x by A1, A3;
hence x in rng f by A1, A3, FUNCT_1:def 3; :: thesis: verum

end;

rng f is finite by A1, FINSET_1:8;
hence proj1 X is finite by A2; :: thesis: proj2 X is finite
deffunc H₂( object ) -> set = $1 `2 ;
consider f being Function such that
A4: ( dom f = X & ( for x being object st x in X holds
f . x = H₂(x) ) ) from FUNCT_1:sch 3();
A5: proj2 X c= rng f

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in proj2 X or x in rng f )
assume x in proj2 X ; :: thesis: x in rng f
then consider y being object such that
A6: [y,x] in X by XTUPLE_0:def 13;
[y,x] `2 = x ;
then f . [y,x] = x by A4, A6;
hence x in rng f by A4, A6, FUNCT_1:def 3; :: thesis: verum

end;

rng f is finite by A4, FINSET_1:8;
hence proj2 X is finite by A5; :: thesis: verum