let it1, it2 be Element of NAT ; :: thesis: ( ex k being Element of NAT st
( it1 = k & ((StepWhile>0 (a,I,s)) . k) . a <= 0 & ( for i being Element of NAT st ((StepWhile>0 (a,I,s)) . i) . a <= 0 holds
k <= i ) & DataPart (Comput ((ProgramPart (s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))))),(s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)))),(LifeSpan ((ProgramPart (s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))))),(s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)))))))) = DataPart ((StepWhile>0 (a,I,s)) . k) ) & ex k being Element of NAT st
( it2 = k & ((StepWhile>0 (a,I,s)) . k) . a <= 0 & ( for i being Element of NAT st ((StepWhile>0 (a,I,s)) . i) . a <= 0 holds
k <= i ) & DataPart (Comput ((ProgramPart (s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))))),(s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)))),(LifeSpan ((ProgramPart (s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))))),(s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)))))))) = DataPart ((StepWhile>0 (a,I,s)) . k) ) implies it1 = it2 )
given k1 being Element of NAT such that A30: it1 = k1 and
A31: ( ((StepWhile>0 (a,I,s)) . k1) . a <= 0 & ( for i being Element of NAT st ((StepWhile>0 (a,I,s)) . i) . a <= 0 holds
k1 <= i ) ) and
DataPart (Comput ((ProgramPart (s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))))),(s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)))),(LifeSpan ((ProgramPart (s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))))),(s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)))))))) = DataPart ((StepWhile>0 (a,I,s)) . k1) ; :: thesis: ( for k being Element of NAT holds
( not it2 = k or not ((StepWhile>0 (a,I,s)) . k) . a <= 0 or ex i being Element of NAT st
( ((StepWhile>0 (a,I,s)) . i) . a <= 0 & not k <= i ) or not DataPart (Comput ((ProgramPart (s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))))),(s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)))),(LifeSpan ((ProgramPart (s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))))),(s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)))))))) = DataPart ((StepWhile>0 (a,I,s)) . k) ) or it1 = it2 )
given k2 being Element of NAT such that A32: it2 = k2 and
A33: ( ((StepWhile>0 (a,I,s)) . k2) . a <= 0 & ( for i being Element of NAT st ((StepWhile>0 (a,I,s)) . i) . a <= 0 holds
k2 <= i ) ) and
DataPart (Comput ((ProgramPart (s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))))),(s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)))),(LifeSpan ((ProgramPart (s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))))),(s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)))))))) = DataPart ((StepWhile>0 (a,I,s)) . k2) ; :: thesis: it1 = it2
( k1 <= k2 & k2 <= k1 ) by A31, A33;
hence it1 = it2 by A30, A32, XXREAL_0:1; :: thesis: verum