theorem :: WSIERP_1:37

for fp being FinSequence of NAT st len fp >= 2 & ( for b, c being Nat st b in dom fp & c in dom fp & b <> c holds
(fp . b) gcd (fp . c) = 1 ) holds
for fr being FinSequence of INT st len fr = len fp holds
ex fr1 being FinSequence of INT st
( len fr1 = len fp & ( for b being Nat st b in dom fp holds
((fp . b) * (fr1 . b)) + (fr . b) = ((fp . 1) * (fr1 . 1)) + (fr . 1) ) )