let f, g be sequence of NAT; :: 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)) ) & g . 0 = m div n & g . 1 = n div (m mod n) & ( for k being Nat holds g . (k + 2) = ((modSeq (m,n)) . k) div ((modSeq (m,n)) . (k + 1)) ) implies f = g )
assume that
A3: ( f . 0 = m div n & f . 1 = n div (m mod n) ) and
A4: for k being Nat holds f . (k + 2) = ((modSeq (m,n)) . k) div ((modSeq (m,n)) . (k + 1)) and
A5: ( g . 0 = m div n & g . 1 = n div (m mod n) ) and
A6: for k being Nat holds g . (k + 2) = ((modSeq (m,n)) . k) div ((modSeq (m,n)) . (k + 1)) ; :: thesis: f = g
reconsider f = f, g = g as sequence of NAT ;
A7: ( g . 0 = m div n & g . 1 = n div (m mod n) ) by A5;
A8: for n being Nat holds g . (n + 2) = H₁(n,g . n,g . (n + 1)) by A6;
A9: for n being Nat holds f . (n + 2) = H₁(n,f . n,f . (n + 1)) by A4;
A10: ( f . 0 = m div n & f . 1 = n div (m mod n) ) by A3;
f = g from RECDEF_2:sch 7(A10, A9, A7, A8);
hence f = g ; :: thesis: verum