theorem Th25: :: REAL_3:25

for n, m being Nat ex k being Nat st
( (divSeq (m,n)) . k = 0 & (modSeq (m,n)) . k = 0 )