let n, k be Nat; :: thesis: ( k > 0 & ( ( n + 1 is prime & (n + k) + 1 is prime ) or ( not n + 1 is prime & not (n + k) + 1 is prime ) ) implies card (primeNumbers ((n + 1),k)) = card (primeNumbers (n,k)) )
assume that
A1: k > 0 and
A2: ( ( n + 1 is prime & (n + k) + 1 is prime ) or ( not n + 1 is prime & not (n + k) + 1 is prime ) ) ; :: thesis: card (primeNumbers ((n + 1),k)) = card (primeNumbers (n,k))
reconsider k1 = k - 1 as Nat by A1;
A3: card (primeNumbers (n,(1 + k1))) = (card (primeNumbers (n,1))) + (card (primeNumbers ((n + 1),k1))) by Th79;

per cases ( ( n + 1 is prime & (n + k) + 1 is prime ) or ( not n + 1 is prime & not (n + k) + 1 is prime ) ) by A2;

suppose ( n + 1 is prime & (n + k) + 1 is prime ) ; :: thesis: card (primeNumbers ((n + 1),k)) = card (primeNumbers (n,k))

then ( card (primeNumbers (n,1)) = 1 & card (primeNumbers (((n + 1) + k1),1)) = 1 ) by Th81;
hence card (primeNumbers ((n + 1),k)) = card (primeNumbers (n,k)) by Th79, A3; :: thesis: verum

end;

suppose ( not n + 1 is prime & not (n + k) + 1 is prime ) ; :: thesis: card (primeNumbers ((n + 1),k)) = card (primeNumbers (n,k))

then ( card (primeNumbers (n,1)) = 0 & card (primeNumbers (((n + 1) + k1),1)) = 0 ) by Th81;
hence card (primeNumbers ((n + 1),k)) = card (primeNumbers (n,k)) by Th79, A3; :: thesis: verum

end;

end;