reconsider i = len p as Element of NAT ;
let s1, s2 be XFinSequence of the Instructions of SCM+FSA; :: thesis: ( ex pp being XFinSequence of the Instructions of SCM+FSA ^omega st
( len pp = len p & ( for k being Element of NAT st k < len pp holds
ex i being Integer st
( i = p . (k + 1) & pp . k = ((aSeq ((intloc 1),(k + 1))) ^ (aSeq ((intloc 2),i))) ^ <%((f,(intloc 1)) := (intloc 2))%> ) ) & s1 = FlattenSeq pp ) & ex pp being XFinSequence of the Instructions of SCM+FSA ^omega st
( len pp = len p & ( for k being Element of NAT st k < len pp holds
ex i being Integer st
( i = p . (k + 1) & pp . k = ((aSeq ((intloc 1),(k + 1))) ^ (aSeq ((intloc 2),i))) ^ <%((f,(intloc 1)) := (intloc 2))%> ) ) & s2 = FlattenSeq pp ) implies s1 = s2 )
assume that
A5: ex pp being XFinSequence of the Instructions of SCM+FSA ^omega st
( len pp = len p & ( for k being Element of NAT st k < len pp holds
ex i being Integer st
( i = p . (k + 1) & pp . k = ((aSeq ((intloc 1),(k + 1))) ^ (aSeq ((intloc 2),i))) ^ <%((f,(intloc 1)) := (intloc 2))%> ) ) & s1 = FlattenSeq pp ) and
A6: ex pp being XFinSequence of the Instructions of SCM+FSA ^omega st
( len pp = len p & ( for k being Element of NAT st k < len pp holds
ex i being Integer st
( i = p . (k + 1) & pp . k = ((aSeq ((intloc 1),(k + 1))) ^ (aSeq ((intloc 2),i))) ^ <%((f,(intloc 1)) := (intloc 2))%> ) ) & s2 = FlattenSeq pp ) ; :: thesis: s1 = s2
consider pp1 being XFinSequence of the Instructions of SCM+FSA ^omega such that
A7: len pp1 = len p and
A8: for k being Element of NAT st k < len pp1 holds
ex i being Integer st
( i = p . (k + 1) & pp1 . k = ((aSeq ((intloc 1),(k + 1))) ^ (aSeq ((intloc 2),i))) ^ <%((f,(intloc 1)) := (intloc 2))%> ) and
A9: s1 = FlattenSeq pp1 by A5;
consider pp2 being XFinSequence of the Instructions of SCM+FSA ^omega such that
A10: len pp2 = len p and
A11: for k being Element of NAT st k < len pp2 holds
ex i being Integer st
( i = p . (k + 1) & pp2 . k = ((aSeq ((intloc 1),(k + 1))) ^ (aSeq ((intloc 2),i))) ^ <%((f,(intloc 1)) := (intloc 2))%> ) and
A12: s2 = FlattenSeq pp2 by A6;
for k being Nat st k < len pp1 holds
pp1 . k = pp2 . k

proof

let k be Nat; :: thesis: ( k < len pp1 implies pp1 . k = pp2 . k )
assume A13: k < len pp1 ; :: thesis: pp1 . k = pp2 . k
k in NAT by ORDINAL1:def 12;
then ( ex i1 being Integer st
( i1 = p . (k + 1) & pp1 . k = ((aSeq ((intloc 1),(k + 1))) ^ (aSeq ((intloc 2),i1))) ^ <%((f,(intloc 1)) := (intloc 2))%> ) & ex i2 being Integer st
( i2 = p . (k + 1) & pp2 . k = ((aSeq ((intloc 1),(k + 1))) ^ (aSeq ((intloc 2),i2))) ^ <%((f,(intloc 1)) := (intloc 2))%> ) ) by A8, A11, A13, A7, A10;
hence pp1 . k = pp2 . k ; :: thesis: verum

end;

hence s1 = s2 by A9, A12, A7, A10, AFINSQ_1:9; :: thesis: verum