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