deffunc H_{1}( 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 = [a,b] & ( 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 = [a,b] & ( 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 = [a,b] and

A4: for n being Nat holds L1 . (n + 1) = H_{1}(n,L1 . n)
; :: thesis: ( for L being sequence of [:NAT,NAT:] holds

( not it2 = (L . n) `1 or not L . 0 = [a,b] 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 = [a,b] and

A7: for n being Nat holds L2 . (n + 1) = H_{1}(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

let it1, it2 be Element of NAT ; :: thesis: ( ex L being sequence of [:NAT,NAT:] st

( it1 = (L . n) `1 & L . 0 = [a,b] & ( 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 = [a,b] & ( 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 = [a,b] and

A4: for n being Nat holds L1 . (n + 1) = H

( not it2 = (L . n) `1 or not L . 0 = [a,b] 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 = [a,b] and

A7: for n being Nat holds L2 . (n + 1) = H

L1 = L2 from NAT_1:sch 16(A3, A4, A6, A7);

hence it1 = it2 by A2, A5; :: thesis: verum