let m, n be Nat; :: thesis: (modSeq (m,n)) . 1 = n mod ((modSeq (m,n)) . 0)
thus (modSeq (m,n)) . 1 = n mod (m mod n) by Def2
.= n mod ((modSeq (m,n)) . 0) by Def2 ; :: thesis: verum