let n, m 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 Lm4;
take k + 1 ; :: thesis: ( (divSeq (m,n)) . (k + 1) = 0 & (modSeq (m,n)) . (k + 1) = 0 )
A2: k + 0 < k + 1 by XREAL_1:6;
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