let m, n 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:8;
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