defpred S₁[ Integer, set ] means ex i being Integer st
( i = p . $1 & $2 = ((aSeq (intloc 1),$1) ^ (aSeq (intloc 2),i)) ^ <*(f,(intloc 1) := (intloc 2))*> );
set D = the Instructions of SCM+FSA * ;
A1: for k being Nat st k in Seg (len p) holds
ex d being Element of the Instructions of SCM+FSA * st S₁[k,d]

proof

let k be Nat; :: thesis: ( k in Seg (len p) implies ex d being Element of the Instructions of SCM+FSA * st S₁[k,d] )
assume k in Seg (len p) ; :: thesis: ex d being Element of the Instructions of SCM+FSA * st S₁[k,d]
then k in dom p by FINSEQ_1:def 3;
then p . k in INT by FINSEQ_2:13;
then reconsider i = p . k as Integer ;
reconsider d = ((aSeq (intloc 1),k) ^ (aSeq (intloc 2),i)) ^ <*(f,(intloc 1) := (intloc 2))*> as Element of the Instructions of SCM+FSA * by FINSEQ_1:def 11;
take d ; :: thesis: S₁[k,d]
thus S₁[k,d] ; :: thesis: verum

end;

consider pp being FinSequence of the Instructions of SCM+FSA * such that
A2: len pp = len p and
A3: for k being Nat st k in Seg (len p) holds
S₁[k,pp /. k] from FINSEQ_4:sch 1(A1);
take FlattenSeq pp ; :: 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))*> ) ) & FlattenSeq pp = FlattenSeq pp )
take pp ; :: thesis: ( 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))*> ) ) & FlattenSeq pp = FlattenSeq pp )
thus len pp = len p by A2; :: thesis: ( ( 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))*> ) ) & FlattenSeq pp = FlattenSeq pp )

hereby :: thesis: FlattenSeq pp = FlattenSeq pp

let k be Element of NAT ; :: thesis: ( 1 <= k & k <= len p implies ex i being Integer st
( i = p . k & ((aSeq (intloc 1),k) ^ (aSeq (intloc 2),i)) ^ <*(f,(intloc 1) := (intloc 2))*> = pp . k ) )
assume A4: ( 1 <= k & k <= len p ) ; :: thesis: ex i being Integer st
( i = p . k & ((aSeq (intloc 1),k) ^ (aSeq (intloc 2),i)) ^ <*(f,(intloc 1) := (intloc 2))*> = pp . k )
then k in dom p by FINSEQ_3:27;
then p . k in INT by FINSEQ_2:13;
then reconsider i = p . k as Integer ;
take i = i; :: thesis: ( i = p . k & ((aSeq (intloc 1),k) ^ (aSeq (intloc 2),i)) ^ <*(f,(intloc 1) := (intloc 2))*> = pp . k )
thus i = p . k ; :: thesis: ((aSeq (intloc 1),k) ^ (aSeq (intloc 2),i)) ^ <*(f,(intloc 1) := (intloc 2))*> = pp . k
k in Seg (len p) by A4;
then ( k in dom pp & S₁[k,pp /. k] ) by A2, A3, FINSEQ_1:def 3;
hence ((aSeq (intloc 1),k) ^ (aSeq (intloc 2),i)) ^ <*(f,(intloc 1) := (intloc 2))*> = pp . k by PARTFUN1:def 8; :: thesis: verum

end;

thus FlattenSeq pp = FlattenSeq pp ; :: thesis: verum