let a, b, m 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 12;
consider a1, m1 being Integer such that
A3: a = l * a1 and
A4: m = l * m1 and
A5: a1,m1 are_coprime by A1, INT_2:23;
consider b1 being Integer such that
A6: b = l * b1 by A2;
consider x1 being Integer such that
A7: ((a1 * x1) - b1) mod m1 = 0 by A5, Th15;
deffunc H₁( Nat) -> set = 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:12;
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;
then consider w being Integer such that
A15: (c1 - c2) * m1 = (l * m1) * w by A4;
(c1 - c2) * m1 = (l * w) * m1 by A15;
then c1 - c2 = l * w by A9, XCMPLX_1:5;
then A16: l divides c1 - c2 ;
A17: c2 in Seg l by A8, A12, FINSEQ_1:def 3;
then A18: c2 >= 1 by FINSEQ_1:1;
A19: c1 in Seg l by A8, A11, FINSEQ_1:def 3;
then c1 <= l by FINSEQ_1:1;
then c1 - c2 <= l - 1 by A18, XREAL_1:13;
then A20: c1 - c2 < l by XREAL_1:147;
A21: c2 <= l by A17, FINSEQ_1:1;
c1 >= 1 by A19, FINSEQ_1:1;
then c1 - c2 >= 1 - l by A21, XREAL_1:13;
then c1 - c2 > - l by XREAL_1:145;
then A22: |.(c1 - c2).| < l by A20, SEQ_2:1;
c1 - c2 <> 0 by A13;
then |.l.| <= |.(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, NAT_D:64;
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, NAT_D:64;
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 NAT_D:61
.= 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