deffunc H_{1}( set , Element of [:NAT,NAT:]) -> Element of [:NAT,NAT:] = [($2 `2),(($2 `1) + ($2 `2))];

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

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

take (L . n) `1 ; :: thesis: ex L being sequence of [:NAT,NAT:] st

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

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

thus ( (L . n) `1 = (L . n) `1 & 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

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

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

take (L . n) `1 ; :: thesis: ex L being sequence of [:NAT,NAT:] st

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

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

thus ( (L . n) `1 = (L . n) `1 & 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