deffunc H1( 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 = H1(x) ) ) from 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 ; :: thesis: verum
end;
rng f is finite by ;
hence proj1 X is finite by A2; :: thesis: proj2 X is finite
deffunc H2( 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 = H2(x) ) ) from 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 ; :: thesis: verum
end;
rng f is finite by ;
hence proj2 X is finite by A5; :: thesis: verum