defpred S_{1}[ set , set ] means $2 = u mod (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]

A2: ( 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

p . i = u mod (m . i) ) )

thus len p = len m by A2, FINSEQ_1:def 3; :: thesis: for i being Nat st i in dom p holds

p . i = u mod (m . i)

thus for i being Nat st i in dom p holds

p . i = u mod (m . i) by A2; :: thesis: verum

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]

reconsider j = u mod (m . k) as Element of INT by INT_1:def 2;

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

thus S_{1}[k,j]
; :: thesis: verum

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

reconsider j = u mod (m . k) as Element of INT by INT_1:def 2;

take j ; :: thesis: S

thus S

A2: ( 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

p . i = u mod (m . i) ) )

thus len p = len m by A2, FINSEQ_1:def 3; :: thesis: for i being Nat st i in dom p holds

p . i = u mod (m . i)

thus for i being Nat st i in dom p holds

p . i = u mod (m . i) by A2; :: thesis: verum