theorem :: NUMBER12:10

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 triangular ) & f is with_all_coprime_terms )