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

proof

let k be Nat; :: thesis: ( k in Segm (len p) implies ex d being Element of the InstructionsF of SCM+FSA ^omega st S₁[k,d] )
assume k in Segm (len p) ; :: thesis: ex d being Element of the InstructionsF of SCM+FSA ^omega st S₁[k,d]
then k < len p by NAT_1:44;
then ( 1 <= k + 1 & k + 1 <= len p ) by NAT_1:12, NAT_1:13;
then k + 1 in dom p by FINSEQ_3:25;
then p . (k + 1) in INT by FINSEQ_2:11;
then reconsider i = p . (k + 1) as Integer ;
reconsider d = ((aSeq ((intloc 1),(k + 1))) ^ (aSeq ((intloc 2),i))) ^ <%((f,(intloc 1)) := (intloc 2))%> as Element of the InstructionsF of SCM+FSA ^omega by AFINSQ_1:def 7;
take d ; :: thesis: S₁[k,d]
thus S₁[k,d] ; :: thesis: verum

end;

consider pp being XFinSequence of the InstructionsF of SCM+FSA ^omega such that
A2: dom pp = Segm (len p) and
A3: for k being Nat st k in Segm (len p) holds
S₁[k,pp . k] from STIRL2_1:sch 5(A1);
reconsider tt = FlattenSeq pp as XFinSequence of the InstructionsF of SCM+FSA by AFINSQ_1:def 7;
take tt ; :: thesis: ex pp being XFinSequence of the InstructionsF of SCM+FSA ^omega st
( len pp = len p & ( for k being 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))%> ) ) & tt = FlattenSeq pp )
take pp ; :: thesis: ( len pp = len p & ( for k being 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))%> ) ) & tt = FlattenSeq pp )
thus len pp = len p by A2; :: thesis: ( ( for k being 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))%> ) ) & tt = FlattenSeq pp )
thus for k being Nat st k < len pp holds
ex i being Integer st
( i = p . (k + 1) & ((aSeq ((intloc 1),(k + 1))) ^ (aSeq ((intloc 2),i))) ^ <%((f,(intloc 1)) := (intloc 2))%> = pp . k ) by A2, A3, NAT_1:44; :: thesis: tt = FlattenSeq pp
thus tt = FlattenSeq pp ; :: thesis: verum