theorem :: NUMBER12:11

for n being Nat ex f being non-empty increasing FinSequence of NAT st
( dom f = Seg (n + 1) & ( for i being Nat st i in dom f holds
f . i is tetrahedral ) & f is with_all_coprime_terms )