deffunc H1( set , Element of ) -> Element of = [(\$2 `2),((\$2 `1) + (\$2 `2))];
let it1, it2 be Element of NAT ; :: thesis: ( ex L being sequence of 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 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 such that A2: it1 = (L1 . n) `1 and
A3: L1 . 0 = [a,b] and
A4: for n being Nat holds L1 . (n + 1) = H1(n,L1 . n) ; :: thesis: ( for L being sequence of 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 such that A5: it2 = (L2 . n) `1 and
A6: L2 . 0 = [a,b] and
A7: for n being Nat holds L2 . (n + 1) = H1(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