reconsider n = n as Nat by TARSKI:1;

set D = product the Sorts of A;

deffunc H_{1}( natural Number , Element of product the Sorts of A) -> Element of product the Sorts of A = Following $2;

( ex y being Element of product the Sorts of A ex f being sequence of (product the Sorts of A) st

( y = f . n & f . 0 = s & ( for n being Nat holds f . (n + 1) = H_{1}(n,f . n) ) ) & ( for y1, y2 being Element of product the Sorts of A st ex f being sequence of (product the Sorts of A) st

( y1 = f . n & f . 0 = s & ( for n being Nat holds f . (n + 1) = H_{1}(n,f . n) ) ) & ex f being sequence of (product the Sorts of A) st

( y2 = f . n & f . 0 = s & ( for n being Nat holds f . (n + 1) = H_{1}(n,f . n) ) ) holds

y1 = y2 ) ) from RECDEF_1:sch 14();

hence ( ex b_{1} being State of A ex f being sequence of (product the Sorts of A) st

( b_{1} = f . n & f . 0 = s & ( for n being Nat holds f . (n + 1) = Following (f . n) ) ) & ( for b_{1}, b_{2} being State of A st ex f being sequence of (product the Sorts of A) st

( b_{1} = f . n & f . 0 = s & ( for n being Nat holds f . (n + 1) = Following (f . n) ) ) & ex f being sequence of (product the Sorts of A) st

( b_{2} = f . n & f . 0 = s & ( for n being Nat holds f . (n + 1) = Following (f . n) ) ) holds

b_{1} = b_{2} ) )
; :: thesis: verum

set D = product the Sorts of A;

deffunc H

( ex y being Element of product the Sorts of A ex f being sequence of (product the Sorts of A) st

( y = f . n & f . 0 = s & ( for n being Nat holds f . (n + 1) = H

( y1 = f . n & f . 0 = s & ( for n being Nat holds f . (n + 1) = H

( y2 = f . n & f . 0 = s & ( for n being Nat holds f . (n + 1) = H

y1 = y2 ) ) from RECDEF_1:sch 14();

hence ( ex b

( b

( b

( b

b