theorem :: NUMBER06:22

for n being Nat ex f being integer-valued AP-like XFinSequence st
( dom f >= n & f is with_all_coprime_terms )