deffunc H_{1}( 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_{1}(x) ) )
from FUNCT_1:sch 3();

A2: proj1 X c= rng f

hence proj1 X is finite by A2; :: thesis: proj2 X is finite

deffunc H_{2}( 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_{2}(x) ) )
from FUNCT_1:sch 3();

A5: proj2 X c= rng f

hence proj2 X is finite by A5; :: thesis: verum

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

A2: proj1 X c= rng f

proof

rng f is finite
by A1, FINSET_1:8;
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;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

hence proj1 X is finite by A2; :: thesis: proj2 X is finite

deffunc H

consider f being Function such that

A4: ( dom f = X & ( for x being object st x in X holds

f . x = H

A5: proj2 X c= rng f

proof

rng f is finite
by A4, FINSET_1:8;
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;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

hence proj2 X is finite by A5; :: thesis: verum