set A = { n where n is Nat : 5 divides (2 |^ n) - 3 } ;
deffunc H₁( Nat) -> Element of NAT = (4 * $1) + 3;
consider f being ManySortedSet of NAT such that
A1: for d being Element of NAT holds f . d = H₁(d) from PBOOLE:sch 5();
A2: dom f = NAT by PARTFUN1:def 2;
A3: rng f c= { n where n is Nat : 5 divides (2 |^ n) - 3 }

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng f or y in { n where n is Nat : 5 divides (2 |^ n) - 3 } )
assume y in rng f ; :: thesis: y in { n where n is Nat : 5 divides (2 |^ n) - 3 }
then consider k being object such that
A4: k in dom f and
A5: f . k = y by FUNCT_1:def 3;
reconsider k = k as Element of NAT by A4, PARTFUN1:def 2;
A6: 2 |^ (4 * k),1 are_congruent_mod 5 by Th7;
A7: (2 |^ (4 * k)) * (2 |^ 3) = 2 |^ ((4 * k) + 3) by NEWTON:8;
8,3 are_congruent_mod 5 ;
then (2 |^ (4 * k)) * (2 |^ 3),1 * 3 are_congruent_mod 5 by A6, Lm3, INT_1:18;
then H₁(k) in { n where n is Nat : 5 divides (2 |^ n) - 3 } by A7;
hence y in { n where n is Nat : 5 divides (2 |^ n) - 3 } by A1, A5; :: thesis: verum

end;

f is one-to-one

proof

let x1, x2 be object ; :: according to FUNCT_1:def 4 :: thesis: ( not x1 in dom f or not x2 in dom f or not f . x1 = f . x2 or x1 = x2 )
assume that
A8: ( x1 in dom f & x2 in dom f ) and
A9: f . x1 = f . x2 ; :: thesis: x1 = x2
reconsider x1 = x1, x2 = x2 as Element of NAT by A8, PARTFUN1:def 2;
( f . x1 = H₁(x1) & f . x2 = H₁(x2) ) by A1;
then (4 * x1) + 3 = (4 * x2) + 3 by A9;
hence x1 = x2 ; :: thesis: verum

end;

hence { n where n is Nat : 5 divides (2 |^ n) - 3 } is infinite by A2, A3, CARD_1:59; :: thesis: verum