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

proof

thus ( len pp1 = i & len pp2 = i ) by A7, A10; :: thesis: for k being Nat st k in dom pp1 holds
pp1 . k = pp2 . k

hereby :: thesis: verum

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

end;

end;

hence s1 = s2 by A9, A12, FINSEQ_2:10; :: thesis: verum