reconsider ss = s as Element of product the Object-Kind of SCM+FSA by PBOOLE:155;
consider f being Function of NAT ,(product the Object-Kind of SCM+FSA ) such that
W1: f . 0 = ss and
W2: for i being Nat holds f . (i + 1) = H₂(i,f . i) from NAT_1:sch 12();
take f ; :: thesis: ( f . 0 = s & ( for i being Nat holds f . (i + 1) = Comput (ProgramPart ((f . i) +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA )))),((f . i) +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA ))),((LifeSpan (ProgramPart ((f . i) +* (I +* (Start-At 0 ,SCM+FSA )))),((f . i) +* (I +* (Start-At 0 ,SCM+FSA )))) + 3) ) )
thus f . 0 = s by W1; :: thesis: for i being Nat holds f . (i + 1) = Comput (ProgramPart ((f . i) +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA )))),((f . i) +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA ))),((LifeSpan (ProgramPart ((f . i) +* (I +* (Start-At 0 ,SCM+FSA )))),((f . i) +* (I +* (Start-At 0 ,SCM+FSA )))) + 3)
let i be Nat; :: thesis: f . (i + 1) = Comput (ProgramPart ((f . i) +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA )))),((f . i) +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA ))),((LifeSpan (ProgramPart ((f . i) +* (I +* (Start-At 0 ,SCM+FSA )))),((f . i) +* (I +* (Start-At 0 ,SCM+FSA )))) + 3)
f . (i + 1) = H₂(i,f . i) by W2;
hence f . (i + 1) = Comput (ProgramPart ((f . i) +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA )))),((f . i) +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA ))),((LifeSpan (ProgramPart ((f . i) +* (I +* (Start-At 0 ,SCM+FSA )))),((f . i) +* (I +* (Start-At 0 ,SCM+FSA )))) + 3) ; :: thesis: verum