let n, m, k be Nat; :: thesis: (primeNumbers (n,m)) \/ (primeNumbers ((n + m),k)) = primeNumbers (n,(m + k))
( primeNumbers (n,m) = (seq (n,m)) /\ SetPrimes & primeNumbers ((n + m),k) = (seq ((n + m),k)) /\ SetPrimes ) by NUMBER14:def 17;
hence (primeNumbers (n,m)) \/ (primeNumbers ((n + m),k)) = ((seq (n,m)) \/ (seq ((n + m),k))) /\ SetPrimes by XBOOLE_1:23
.= (seq (n,(m + k))) /\ SetPrimes by Th77
.= primeNumbers (n,(m + k)) by NUMBER14:def 17 ;
:: thesis: verum