consider f being sequence of NAT such that
A1: ( f . 0 = m div n & f . 1 = n div (m mod n) ) and
A2: for n being Nat holds f . (n + 2) = H₁(n,f . n,f . (n + 1)) from RECDEF_2:sch 5();
reconsider f = f as sequence of NAT ;
take f ; :: thesis: ( f . 0 = m div n & f . 1 = n div (m mod n) & ( for k being Nat holds f . (k + 2) = ((modSeq (m,n)) . k) div ((modSeq (m,n)) . (k + 1)) ) )
thus ( f . 0 = m div n & f . 1 = n div (m mod n) ) by A1; :: thesis: for k being Nat holds f . (k + 2) = ((modSeq (m,n)) . k) div ((modSeq (m,n)) . (k + 1))
let k be Nat; :: thesis: f . (k + 2) = ((modSeq (m,n)) . k) div ((modSeq (m,n)) . (k + 1))
thus f . (k + 2) = ((modSeq (m,n)) . k) div ((modSeq (m,n)) . (k + 1)) by A2; :: thesis: verum