let k be Integer; :: thesis: ( k <> 1 implies { n where n is positive Nat : (2 |^ (2 |^ n)) + k is composite } , { ((2 |^ (2 |^ n)) + k) where n is positive Nat : (2 |^ (2 |^ n)) + k is composite } are_equipotent )
set X = { n where n is positive Nat : (2 |^ (2 |^ n)) + k is composite } ;
set Y = { ((2 |^ (2 |^ n)) + k) where n is positive Nat : (2 |^ (2 |^ n)) + k is composite } ;
assume k <> 1 ; :: thesis: { n where n is positive Nat : (2 |^ (2 |^ n)) + k is composite } , { ((2 |^ (2 |^ n)) + k) where n is positive Nat : (2 |^ (2 |^ n)) + k is composite } are_equipotent
then A1: not { ((2 |^ (2 |^ n)) + k) where n is positive Nat : (2 |^ (2 |^ n)) + k is composite } is empty by Lm13;
defpred S₁[ object , object ] means for m being Nat st m = $1 holds
$2 = (2 |^ (2 |^ m)) + k;
A2: for x being object st x in { n where n is positive Nat : (2 |^ (2 |^ n)) + k is composite } holds
ex y being object st
( y in { ((2 |^ (2 |^ n)) + k) where n is positive Nat : (2 |^ (2 |^ n)) + k is composite } & S₁[x,y] )

proof

let x be object ; :: thesis: ( x in { n where n is positive Nat : (2 |^ (2 |^ n)) + k is composite } implies ex y being object st
( y in { ((2 |^ (2 |^ n)) + k) where n is positive Nat : (2 |^ (2 |^ n)) + k is composite } & S₁[x,y] ) )
assume x in { n where n is positive Nat : (2 |^ (2 |^ n)) + k is composite } ; :: thesis: ex y being object st
( y in { ((2 |^ (2 |^ n)) + k) where n is positive Nat : (2 |^ (2 |^ n)) + k is composite } & S₁[x,y] )
then consider n being positive Nat such that
A3: ( x = n & (2 |^ (2 |^ n)) + k is composite ) ;
take (2 |^ (2 |^ n)) + k ; :: thesis: ( (2 |^ (2 |^ n)) + k in { ((2 |^ (2 |^ n)) + k) where n is positive Nat : (2 |^ (2 |^ n)) + k is composite } & S₁[x,(2 |^ (2 |^ n)) + k] )
thus ( (2 |^ (2 |^ n)) + k in { ((2 |^ (2 |^ n)) + k) where n is positive Nat : (2 |^ (2 |^ n)) + k is composite } & S₁[x,(2 |^ (2 |^ n)) + k] ) by A3; :: thesis: verum

end;

consider f being Function of { n where n is positive Nat : (2 |^ (2 |^ n)) + k is composite } , { ((2 |^ (2 |^ n)) + k) where n is positive Nat : (2 |^ (2 |^ n)) + k is composite } such that
A4: for x being object st x in { n where n is positive Nat : (2 |^ (2 |^ n)) + k is composite } holds
S₁[x,f . x] from FUNCT_2:sch 1(A2);
take f ; :: according to WELLORD2:def 4 :: thesis: ( f is one-to-one & proj1 f = { n where n is positive Nat : (2 |^ (2 |^ n)) + k is composite } & proj2 f = { ((2 |^ (2 |^ n)) + k) where n is positive Nat : (2 |^ (2 |^ n)) + k is composite } )
A5: dom f = { n where n is positive Nat : (2 |^ (2 |^ n)) + k is composite } by A1, FUNCT_2:def 1;
thus f is one-to-one :: thesis: ( proj1 f = { n where n is positive Nat : (2 |^ (2 |^ n)) + k is composite } & proj2 f = { ((2 |^ (2 |^ n)) + k) where n is positive Nat : (2 |^ (2 |^ n)) + k is composite } )

proof

let x1, x2 be object ; :: according to FUNCT_1:def 4 :: thesis: ( not x1 in proj1 f or not x2 in proj1 f or not f . x1 = f . x2 or x1 = x2 )
assume A6: x1 in dom f ; :: thesis: ( not x2 in proj1 f or not f . x1 = f . x2 or x1 = x2 )
then consider n1 being positive Nat such that
A7: x1 = n1 and
(2 |^ (2 |^ n1)) + k is composite by A5;
assume A8: x2 in dom f ; :: thesis: ( not f . x1 = f . x2 or x1 = x2 )
then consider n2 being positive Nat such that
A9: x2 = n2 and
(2 |^ (2 |^ n2)) + k is composite by A5;
assume A10: f . x1 = f . x2 ; :: thesis: x1 = x2
A11: f . n1 = (2 |^ (2 |^ n1)) + k by A4, A6, A7;
f . n2 = (2 |^ (2 |^ n2)) + k by A4, A8, A9;
then 2 |^ n1 = 2 |^ n2 by A7, A9, A10, A11, XCMPLX_1:2, PEPIN:30;
hence x1 = x2 by A7, A9, PEPIN:30; :: thesis: verum

end;

thus dom f = { n where n is positive Nat : (2 |^ (2 |^ n)) + k is composite } by A5; :: thesis: proj2 f = { ((2 |^ (2 |^ n)) + k) where n is positive Nat : (2 |^ (2 |^ n)) + k is composite }
thus rng f c= { ((2 |^ (2 |^ n)) + k) where n is positive Nat : (2 |^ (2 |^ n)) + k is composite } ; :: according to XBOOLE_0:def 10 :: thesis: { ((2 |^ (2 |^ n)) + k) where n is positive Nat : (2 |^ (2 |^ n)) + k is composite } c= proj2 f
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in { ((2 |^ (2 |^ n)) + k) where n is positive Nat : (2 |^ (2 |^ n)) + k is composite } or y in proj2 f )
assume y in { ((2 |^ (2 |^ n)) + k) where n is positive Nat : (2 |^ (2 |^ n)) + k is composite } ; :: thesis: y in proj2 f
then consider n being positive Nat such that
A12: y = (2 |^ (2 |^ n)) + k and
A13: (2 |^ (2 |^ n)) + k is composite ;
A14: n in dom f by A5, A13;
then f . n = y by A4, A12;
hence y in proj2 f by A14, FUNCT_1:def 3; :: thesis: verum