set D = product the Sorts of A;
deffunc H₁( Nat, 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 Function of NAT,(product the Sorts of A) st
( y = f . n & f . 0 = s & ( for n being Nat holds f . (n + 1) = H₁(n,f . n) ) ) & ( for y1, y2 being Element of product the Sorts of A st ex f being Function of NAT,(product the Sorts of A) st
( y1 = f . n & f . 0 = s & ( for n being Nat holds f . (n + 1) = H₁(n,f . n) ) ) & ex f being Function of NAT,(product the Sorts of A) st
( y2 = f . n & f . 0 = s & ( for n being Nat holds f . (n + 1) = H₁(n,f . n) ) ) holds
y1 = y2 ) ) from RECDEF_1:sch 14();
hence ( ex b₁ being State of A ex f being Function of NAT,(product the Sorts of A) st
( b₁ = f . n & f . 0 = s & ( for n being Nat holds f . (n + 1) = Following (f . n) ) ) & ( for b₁, b₂ being State of A st ex f being Function of NAT,(product the Sorts of A) st
( b₁ = f . n & f . 0 = s & ( for n being Nat holds f . (n + 1) = Following (f . n) ) ) & ex f being Function of NAT,(product the Sorts of A) st
( b₂ = f . n & f . 0 = s & ( for n being Nat holds f . (n + 1) = Following (f . n) ) ) holds
b₁ = b₂ ) ) ; :: thesis: verum