let n, m be Nat; :: thesis:
set f = modSeq (m,n);
defpred S₁[ Nat] means ex k being Nat st (modSeq (m,n)) . k = $1;
A1: for a being Nat st a <> 0 & S₁[a] holds
ex w being Nat st
( w < a & S₁[w] )

let a be Nat; :: thesis:
assume A2: a <> 0 ; :: thesis:
given k being Nat such that A3: (modSeq (m,n)) . k = a ; :: thesis:
take w = (modSeq (m,n)) . (k + 1); :: thesis:
k + 0 < k + 1 by XREAL_1:6;
hence w < a by A2, A3, Th15; :: thesis:
thus S₁[w] ; :: thesis:

end;

take (modSeq (m,n)) . 0 ; :: thesis:
take 0 ; :: thesis:
thus (modSeq (m,n)) . 0 = (modSeq (m,n)) . 0 ; :: thesis:

end;