deffunc H₁( set , Element of [:NAT,NAT:]) -> Element of [:NAT,NAT:] = [($2 `2),(($2 `1) + ($2 `2))];
let it1, it2 be Element of NAT ; :: thesis: ( ex L being sequence of [:NAT,NAT:] st
( it1 = (L . n) `1 & L . 0 = [2,1] & ( for n being Nat holds L . (n + 1) = [((L . n) `2),(((L . n) `1) + ((L . n) `2))] ) ) & ex L being sequence of [:NAT,NAT:] st
( it2 = (L . n) `1 & L . 0 = [2,1] & ( for n being Nat holds L . (n + 1) = [((L . n) `2),(((L . n) `1) + ((L . n) `2))] ) ) implies it1 = it2 )
given L1 being sequence of [:NAT,NAT:] such that A2: it1 = (L1 . n) `1 and
A3: L1 . 0 = [2,1] and
A4: for n being Nat holds L1 . (n + 1) = H₁(n,L1 . n) ; :: thesis: ( for L being sequence of [:NAT,NAT:] holds
( not it2 = (L . n) `1 or not L . 0 = [2,1] or ex n being Nat st not L . (n + 1) = [((L . n) `2),(((L . n) `1) + ((L . n) `2))] ) or it1 = it2 )
given L2 being sequence of [:NAT,NAT:] such that A5: it2 = (L2 . n) `1 and
A6: L2 . 0 = [2,1] and
A7: for n being Nat holds L2 . (n + 1) = H₁(n,L2 . n) ; :: thesis: it1 = it2
L1 = L2 from NAT_1:sch 16(A3, A4, A6, A7);
hence it1 = it2 by A2, A5; :: thesis: verum