consider L being sequence of [:NAT,NAT:] such that
A1: ( L . 0 = [a,b] & ( for n being Nat holds L . (n + 1) = H₂(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