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