defpred S_{1}[ set , set ] means ex s, mm being Integer st

( mm = (Product m) / (m . $1) & s * mm,1 are_congruent_mod m . $1 & $2 = s * ((Product m) / (m . $1)) );

A1: for k being Nat st k in Seg (len m) holds

ex x being Element of INT st S_{1}[k,x]

A4: ( dom p = Seg (len m) & ( for k being Nat st k in Seg (len m) holds

S_{1}[k,p . k] ) )
from FINSEQ_1:sch 5(A1);

take p ; :: thesis: ( len p = len m & ( for i being Nat st i in dom p holds

ex s, mm being Integer st

( mm = (Product m) / (m . i) & s * mm,1 are_congruent_mod m . i & p . i = s * ((Product m) / (m . i)) ) ) )

thus ( len p = len m & ( for i being Nat st i in dom p holds

ex s, mm being Integer st

( mm = (Product m) / (m . i) & s * mm,1 are_congruent_mod m . i & p . i = s * ((Product m) / (m . i)) ) ) ) by A4, FINSEQ_1:def 3; :: thesis: verum

( mm = (Product m) / (m . $1) & s * mm,1 are_congruent_mod m . $1 & $2 = s * ((Product m) / (m . $1)) );

A1: for k being Nat st k in Seg (len m) holds

ex x being Element of INT st S

proof

consider p being FinSequence of INT such that
let k be Nat; :: thesis: ( k in Seg (len m) implies ex x being Element of INT st S_{1}[k,x] )

assume k in Seg (len m) ; :: thesis: ex x being Element of INT st S_{1}[k,x]

then A2: k in dom m by FINSEQ_1:def 3;

then reconsider mm = (Product m) / (m . k) as Integer by Th9;

consider s being Integer such that

A3: s * mm,1 are_congruent_mod m . k by A2, Th22, Th25;

set x = s * mm;

reconsider x = s * mm as Element of INT by INT_1:def 2;

take x ; :: thesis: S_{1}[k,x]

take s ; :: thesis: ex mm being Integer st

( mm = (Product m) / (m . k) & s * mm,1 are_congruent_mod m . k & x = s * ((Product m) / (m . k)) )

take mm ; :: thesis: ( mm = (Product m) / (m . k) & s * mm,1 are_congruent_mod m . k & x = s * ((Product m) / (m . k)) )

thus ( mm = (Product m) / (m . k) & s * mm,1 are_congruent_mod m . k & x = s * ((Product m) / (m . k)) ) by A3; :: thesis: verum

end;assume k in Seg (len m) ; :: thesis: ex x being Element of INT st S

then A2: k in dom m by FINSEQ_1:def 3;

then reconsider mm = (Product m) / (m . k) as Integer by Th9;

consider s being Integer such that

A3: s * mm,1 are_congruent_mod m . k by A2, Th22, Th25;

set x = s * mm;

reconsider x = s * mm as Element of INT by INT_1:def 2;

take x ; :: thesis: S

take s ; :: thesis: ex mm being Integer st

( mm = (Product m) / (m . k) & s * mm,1 are_congruent_mod m . k & x = s * ((Product m) / (m . k)) )

take mm ; :: thesis: ( mm = (Product m) / (m . k) & s * mm,1 are_congruent_mod m . k & x = s * ((Product m) / (m . k)) )

thus ( mm = (Product m) / (m . k) & s * mm,1 are_congruent_mod m . k & x = s * ((Product m) / (m . k)) ) by A3; :: thesis: verum

A4: ( dom p = Seg (len m) & ( for k being Nat st k in Seg (len m) holds

S

take p ; :: thesis: ( len p = len m & ( for i being Nat st i in dom p holds

ex s, mm being Integer st

( mm = (Product m) / (m . i) & s * mm,1 are_congruent_mod m . i & p . i = s * ((Product m) / (m . i)) ) ) )

thus ( len p = len m & ( for i being Nat st i in dom p holds

ex s, mm being Integer st

( mm = (Product m) / (m . i) & s * mm,1 are_congruent_mod m . i & p . i = s * ((Product m) / (m . i)) ) ) ) by A4, FINSEQ_1:def 3; :: thesis: verum