let m, a, b be Integer; :: thesis: ( m <> 0 & a gcd m divides b implies 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 ) ) )
assume that
A1: m <> 0 and
A2: a gcd m divides b ; :: thesis: 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 ) )
set l = a gcd m;
reconsider l = a gcd m as Element of NAT by ORDINAL1:def 13;
consider a1, m1 being Integer such that
A3: a = l * a1 and
A4: m = l * m1 and
A5: a1,m1 are_relative_prime by A1, INT_2:38;
consider b1 being Integer such that
A6: b = l * b1 by A2, INT_1:def 9;
consider x1 being Integer such that
A7: ((a1 * x1) - b1) mod m1 = 0 by A5, Th15;
deffunc H₁( Nat) -> Element of REAL = x1 + (($1 - 1) * m1);
consider fp being FinSequence such that
A8: ( len fp = l & ( for c being Nat st c in dom fp holds
fp . c = H₁(c) ) ) from FINSEQ_1:sch 2();
for c being Nat st c in dom fp holds
fp . c in INT

proof

let c be Nat; :: thesis: ( c in dom fp implies fp . c in INT )
assume c in dom fp ; :: thesis: fp . c in INT
then fp . c = x1 + ((c - 1) * m1) by A8;
hence fp . c in INT by INT_1:def 2; :: thesis: verum

end;

then reconsider fp = fp as FinSequence of INT by FINSEQ_2:14;
A9: m1 <> 0 by A1, A4;
A10: 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

proof

let c1, c2 be Element of NAT ; :: thesis: ( c1 in dom fp & c2 in dom fp & c1 <> c2 implies not fp . c1,fp . c2 are_congruent_mod m )
assume that
A11: c1 in dom fp and
A12: c2 in dom fp and
A13: c1 <> c2 ; :: thesis: not fp . c1,fp . c2 are_congruent_mod m
assume A14: fp . c1,fp . c2 are_congruent_mod m ; :: thesis: contradiction
( fp . c1 = x1 + ((c1 - 1) * m1) & fp . c2 = x1 + ((c2 - 1) * m1) ) by A8, A11, A12;
then m divides (((c1 - 1) * m1) + x1) - (((c2 - 1) * m1) + x1) by A14, INT_2:19;
then consider w being Integer such that
A15: (c1 - c2) * m1 = (l * m1) * w by A4, INT_1:def 9;
(c1 - c2) * m1 = (l * w) * m1 by A15;
then c1 - c2 = l * w by A9, XCMPLX_1:5;
then A16: l divides c1 - c2 by INT_1:def 9;
A17: c2 in Seg l by A8, A12, FINSEQ_1:def 3;
then A18: c2 >= 1 by FINSEQ_1:3;
A19: c1 in Seg l by A8, A11, FINSEQ_1:def 3;
then c1 <= l by FINSEQ_1:3;
then c1 - c2 <= l - 1 by A18, XREAL_1:15;
then A20: c1 - c2 < l by XREAL_1:149;
A21: c2 <= l by A17, FINSEQ_1:3;
c1 >= 1 by A19, FINSEQ_1:3;
then c1 - c2 >= 1 - l by A21, XREAL_1:15;
then c1 - c2 > - l by XREAL_1:147;
then A22: abs (c1 - c2) < l by A20, SEQ_2:9;
c1 - c2 <> 0 by A13;
then abs l <= abs (c1 - c2) by A16, Th6;
hence contradiction by A22, ABSVALUE:def 1; :: thesis: verum

end;

take fp ; :: thesis: ( 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 ) )
((a1 * x1) - b1) mod m1 = 0 mod m1 by A7, Th12;
then (a1 * x1) - b1, 0 are_congruent_mod m1 by A9, INT_3:12;
then ((a1 * x1) - b1) * l,0 * l are_congruent_mod m1 * l by Th10;
then A23: ((a * x1) - b) mod m = 0 mod m by A3, A4, A6, INT_3:12;
for c being Element of NAT st c in dom fp holds
((a * (fp . c)) - b) mod m = 0

proof

let c be Element of NAT ; :: thesis: ( c in dom fp implies ((a * (fp . c)) - b) mod m = 0 )
assume c in dom fp ; :: thesis: ((a * (fp . c)) - b) mod m = 0
hence ((a * (fp . c)) - b) mod m = ((a * (x1 + ((c - 1) * m1))) - b) mod m by A8
.= (((a * x1) - b) + ((a1 * (c - 1)) * m)) mod m by A3, A4
.= ((a * x1) - b) mod m by INT_3:8
.= 0 by A23, Th12 ;
:: thesis: verum

end;

hence ( 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 ) ) by A8, A10; :: thesis: verum