consider L being sequence of [:NAT,NAT:] such that

A1: ( L . 0 = [a,b] & ( for n being Nat holds L . (n + 1) = H_{2}(n,L . n) ) )
from NAT_1:sch 12();

take L ; :: thesis: ( L . 0 = [a,b] & ( for n being Nat holds L . (n + 1) = [((L . n) `2),(((L . n) `1) + ((L . n) `2))] ) )

thus ( L . 0 = [a,b] & ( for n being Nat holds L . (n + 1) = [((L . n) `2),(((L . n) `1) + ((L . n) `2))] ) ) by A1; :: thesis: verum

A1: ( L . 0 = [a,b] & ( for n being Nat holds L . (n + 1) = H

take L ; :: thesis: ( L . 0 = [a,b] & ( for n being Nat holds L . (n + 1) = [((L . n) `2),(((L . n) `1) + ((L . n) `2))] ) )

thus ( L . 0 = [a,b] & ( for n being Nat holds L . (n + 1) = [((L . n) `2),(((L . n) `1) + ((L . n) `2))] ) ) by A1; :: thesis: verum