let it1, it2 be Nat; ( ex k being Nat st
( it1 = k & ((StepWhile=0 (a,I,p,s)) . k) . a <> 0 & ( for i being Nat st ((StepWhile=0 (a,I,p,s)) . i) . a <> 0 holds
k <= i ) & DataPart (Comput ((p +* (while=0 (a,I))),(Initialize s),(LifeSpan ((p +* (while=0 (a,I))),(Initialize s))))) = DataPart ((StepWhile=0 (a,I,p,s)) . k) ) & ex k being Nat st
( it2 = k & ((StepWhile=0 (a,I,p,s)) . k) . a <> 0 & ( for i being Nat st ((StepWhile=0 (a,I,p,s)) . i) . a <> 0 holds
k <= i ) & DataPart (Comput ((p +* (while=0 (a,I))),(Initialize s),(LifeSpan ((p +* (while=0 (a,I))),(Initialize s))))) = DataPart ((StepWhile=0 (a,I,p,s)) . k) ) implies it1 = it2 )
given k1 being Nat such that A31:
it1 = k1
and
A32:
( ((StepWhile=0 (a,I,p,s)) . k1) . a <> 0 & ( for i being Nat st ((StepWhile=0 (a,I,p,s)) . i) . a <> 0 holds
k1 <= i ) )
and
DataPart (Comput ((p +* (while=0 (a,I))),(Initialize s),(LifeSpan ((p +* (while=0 (a,I))),(Initialize s))))) = DataPart ((StepWhile=0 (a,I,p,s)) . k1)
; ( for k being Nat holds
( not it2 = k or not ((StepWhile=0 (a,I,p,s)) . k) . a <> 0 or ex i being Nat st
( ((StepWhile=0 (a,I,p,s)) . i) . a <> 0 & not k <= i ) or not DataPart (Comput ((p +* (while=0 (a,I))),(Initialize s),(LifeSpan ((p +* (while=0 (a,I))),(Initialize s))))) = DataPart ((StepWhile=0 (a,I,p,s)) . k) ) or it1 = it2 )
given k2 being Nat such that A33:
it2 = k2
and
A34:
( ((StepWhile=0 (a,I,p,s)) . k2) . a <> 0 & ( for i being Nat st ((StepWhile=0 (a,I,p,s)) . i) . a <> 0 holds
k2 <= i ) )
and
DataPart (Comput ((p +* (while=0 (a,I))),(Initialize s),(LifeSpan ((p +* (while=0 (a,I))),(Initialize s))))) = DataPart ((StepWhile=0 (a,I,p,s)) . k2)
; it1 = it2
( k1 <= k2 & k2 <= k1 )
by A32, A34;
hence
it1 = it2
by A31, A33, XXREAL_0:1; verum