let n, m be Nat; :: thesis: ex k being Nat st (modSeq (m,n)) . k = 0
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] )

proof

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

end;

A4: ex a being Nat st S₁[a]

proof

take (modSeq (m,n)) . 0 ; :: thesis: S₁[(modSeq (m,n)) . 0]
take 0 ; :: thesis: (modSeq (m,n)) . 0 = (modSeq (m,n)) . 0
thus (modSeq (m,n)) . 0 = (modSeq (m,n)) . 0 ; :: thesis: verum

end;

thus S₁[ 0 ] from NAT_1:sch 7(A4, A1); :: thesis: verum