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₂(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₂(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