defpred S1[ set , set ] means ex s, mm being Integer st
( mm = () / (m . \$1) & s * mm,1 are_congruent_mod m . \$1 & \$2 = s * (() / (m . \$1)) );
A1: for k being Nat st k in Seg (len m) holds
ex x being Element of INT st S1[k,x]
proof
let k be Nat; :: thesis: ( k in Seg (len m) implies ex x being Element of INT st S1[k,x] )
assume k in Seg (len m) ; :: thesis: ex x being Element of INT st S1[k,x]
then A2: k in dom m by FINSEQ_1:def 3;
then reconsider mm = () / (m . k) as Integer by Th9;
consider s being Integer such that
A3: s * mm,1 are_congruent_mod m . k by ;
set x = s * mm;
reconsider x = s * mm as Element of INT by INT_1:def 2;
take x ; :: thesis: S1[k,x]
take s ; :: thesis: ex mm being Integer st
( mm = () / (m . k) & s * mm,1 are_congruent_mod m . k & x = s * (() / (m . k)) )

take mm ; :: thesis: ( mm = () / (m . k) & s * mm,1 are_congruent_mod m . k & x = s * (() / (m . k)) )
thus ( mm = () / (m . k) & s * mm,1 are_congruent_mod m . k & x = s * (() / (m . k)) ) by A3; :: thesis: verum
end;
consider p being FinSequence of INT such that
A4: ( dom p = Seg (len m) & ( for k being Nat st k in Seg (len m) holds
S1[k,p . k] ) ) from take p ; :: thesis: ( len p = len m & ( for i being Nat st i in dom p holds
ex s, mm being Integer st
( mm = () / (m . i) & s * mm,1 are_congruent_mod m . i & p . i = s * (() / (m . i)) ) ) )

thus ( len p = len m & ( for i being Nat st i in dom p holds
ex s, mm being Integer st
( mm = () / (m . i) & s * mm,1 are_congruent_mod m . i & p . i = s * (() / (m . i)) ) ) ) by ; :: thesis: verum