for a, b, m being Integer st m <> 0 & a gcd m divides b holds
ex fp being FinSequence of INT st
( len fp = a gcd m & ( for c being Element of NAT st c in dom fp holds
((a * (fp . c)) - b) mod m = 0 ) & ( for c1, c2 being Element of NAT st c1 in dom fp & c2 in dom fp & c1 <> c2 holds
not fp . c1,fp . c2 are_congruent_mod m ) )