deffunc H₁( set , Element of [:NAT,NAT:]) -> Element of [:NAT,NAT:] = [($2 `2),(($2 `1) + ($2 `2))];
consider L being Function of NAT,[:NAT,NAT:] such that
A1: ( L . 0 = [a,b] & ( for n being Nat holds L . (n + 1) = H<sub>1</sub>(n,L . n) ) ) from NAT_1:sch 12();
take (L . n) `1 ; :: thesis: ex L being Function of NAT,[: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