let n, m, k be Nat; :: thesis: card (primeNumbers (n,(m + k))) = (card (primeNumbers (n,m))) + (card (primeNumbers ((n + m),k)))
card ((primeNumbers (n,m)) \/ (primeNumbers ((n + m),k))) = (card (primeNumbers (n,m))) + (card (primeNumbers ((n + m),k))) by CARD_2:40, Th76;
hence card (primeNumbers (n,(m + k))) = (card (primeNumbers (n,m))) + (card (primeNumbers ((n + m),k))) by Th78; :: thesis: verum