reconsider ss = s as Element of product (the_Values_of SCM+FSA) by CARD_3:107;

consider f being sequence of (product (the_Values_of SCM+FSA)) such that

A1: f . 0 = ss and

A2: for i being Nat holds f . (i + 1) = H_{2}(i,f . i)
from NAT_1:sch 12();

take f ; :: thesis: ( f . 0 = s & ( for i being Nat holds f . (i + 1) = Comput ((P +* (while>0 (a,I))),(Initialized (f . i)),((LifeSpan (((P +* (while>0 (a,I))) +* I),(Initialized (f . i)))) + 2)) ) )

thus f . 0 = s by A1; :: thesis: for i being Nat holds f . (i + 1) = Comput ((P +* (while>0 (a,I))),(Initialized (f . i)),((LifeSpan (((P +* (while>0 (a,I))) +* I),(Initialized (f . i)))) + 2))

let i be Nat; :: thesis: f . (i + 1) = Comput ((P +* (while>0 (a,I))),(Initialized (f . i)),((LifeSpan (((P +* (while>0 (a,I))) +* I),(Initialized (f . i)))) + 2))

f . (i + 1) = H_{2}(i,f . i)
by A2;

hence f . (i + 1) = Comput ((P +* (while>0 (a,I))),(Initialized (f . i)),((LifeSpan (((P +* (while>0 (a,I))) +* I),(Initialized (f . i)))) + 2)) ; :: thesis: verum

consider f being sequence of (product (the_Values_of SCM+FSA)) such that

A1: f . 0 = ss and

A2: for i being Nat holds f . (i + 1) = H

take f ; :: thesis: ( f . 0 = s & ( for i being Nat holds f . (i + 1) = Comput ((P +* (while>0 (a,I))),(Initialized (f . i)),((LifeSpan (((P +* (while>0 (a,I))) +* I),(Initialized (f . i)))) + 2)) ) )

thus f . 0 = s by A1; :: thesis: for i being Nat holds f . (i + 1) = Comput ((P +* (while>0 (a,I))),(Initialized (f . i)),((LifeSpan (((P +* (while>0 (a,I))) +* I),(Initialized (f . i)))) + 2))

let i be Nat; :: thesis: f . (i + 1) = Comput ((P +* (while>0 (a,I))),(Initialized (f . i)),((LifeSpan (((P +* (while>0 (a,I))) +* I),(Initialized (f . i)))) + 2))

f . (i + 1) = H

hence f . (i + 1) = Comput ((P +* (while>0 (a,I))),(Initialized (f . i)),((LifeSpan (((P +* (while>0 (a,I))) +* I),(Initialized (f . i)))) + 2)) ; :: thesis: verum