let n, k be Nat; :: thesis: ( k > 0 & not n + 1 is prime & (n + k) + 1 is prime implies card (primeNumbers ((n + 1),k)) = (card (primeNumbers (n,k))) + 1 )
assume that
A1: k > 0 and
A2: ( not n + 1 is prime & (n + k) + 1 is prime ) ; :: thesis: card (primeNumbers ((n + 1),k)) = (card (primeNumbers (n,k))) + 1
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;
( card (primeNumbers (n,1)) = 0 & card (primeNumbers (((n + 1) + k1),1)) = 1 ) by A2, Th81;
hence card (primeNumbers ((n + 1),k)) = (card (primeNumbers (n,k))) + 1 by Th79, A3; :: thesis: verum