theorem Th13: :: REAL_3:13

for n, m being Nat holds (modSeq (m,n)) . 1 = n mod ((modSeq (m,n)) . 0)