let m, n be Nat; :: thesis: ex k being Nat st
( (divSeq m,n) . k = 0 & (modSeq m,n) . k = 0 )
set f = modSeq m,n;
consider k being Nat such that
A1: (modSeq m,n) . k = 0 by Lm6;
take k + 1 ; :: thesis: ( (divSeq m,n) . (k + 1) = 0 & (modSeq m,n) . (k + 1) = 0 )
A2: k + 0 < k + 1 by XREAL_1:8;
hence (divSeq m,n) . (k + 1) = 0 by A1, Th18; :: thesis: (modSeq m,n) . (k + 1) = 0
thus (modSeq m,n) . (k + 1) = 0 by A1, A2, Th14; :: thesis: verum