:: deftheorem Def1 defines modSeq REAL_3:def 1 :
for m, n being Nat
for b₃ being sequence of NAT holds
( b₃ = modSeq (m,n) iff ( b₃ . 0 = m mod n & b₃ . 1 = n mod (m mod n) & ( for k being Nat holds b₃ . (k + 2) = (b₃ . k) mod (b₃ . (k + 1)) ) ) );