let n, m be Nat; ex k being Nat st (modSeq (m,n)) . k = 0
set f = modSeq (m,n);
defpred S1[ Nat] means ex k being Nat st (modSeq (m,n)) . k = $1;
A1:
for a being Nat st a <> 0 & S1[a] holds
ex w being Nat st
( w < a & S1[w] )
proof
let a be
Nat;
( a <> 0 & S1[a] implies ex w being Nat st
( w < a & S1[w] ) )
assume A2:
a <> 0
;
( not S1[a] or ex w being Nat st
( w < a & S1[w] ) )
given k being
Nat such that A3:
(modSeq (m,n)) . k = a
;
ex w being Nat st
( w < a & S1[w] )
take w =
(modSeq (m,n)) . (k + 1);
( w < a & S1[w] )
k + 0 < k + 1
by XREAL_1:6;
hence
w < a
by A2, A3, Th15;
S1[w]
thus
S1[
w]
;
verum
end;
A4:
ex a being Nat st S1[a]
thus
S1[ 0 ]
from NAT_1:sch 7(A4, A1); verum