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