consider fib being sequence of [:NAT,NAT:] such that
A1: ( fib . 0 = [0,1] & ( for n being Nat holds fib . (n + 1) = H₁(n,fib . n) ) ) from NAT_1:sch 12();
take fib ; :: thesis: ( fib . 0 = [0,1] & ( for n being Nat holds fib . (n + 1) = [((fib . n) `2),(((fib . n) `1) + ((fib . n) `2))] ) )
thus fib . 0 = [0,1] by A1; :: thesis: for n being Nat holds fib . (n + 1) = [((fib . n) `2),(((fib . n) `1) + ((fib . n) `2))]
let n be Nat; :: thesis: fib . (n + 1) = [((fib . n) `2),(((fib . n) `1) + ((fib . n) `2))]
fib . (n + 1) = H<sub>1</sub>(n,fib . n) by A1;
hence fib . (n + 1) = [((fib . n) `2),(((fib . n) `1) + ((fib . n) `2))] ; :: thesis: verum