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 Instructions of SCM+FSA ^omega ;
A1: for k being Nat st k in len p holds
ex d being Element of the Instructions of SCM+FSA ^omega st S₁[k,d]

proof

let k be Nat; :: thesis: ( k in len p implies ex d being Element of the Instructions of SCM+FSA ^omega st S₁[k,d] )
assume k in len p ; :: thesis: ex d being Element of the Instructions of SCM+FSA ^omega st S₁[k,d]
then k < len p by NAT_1:45;
then ( 1 <= k + 1 & k + 1 <= len p ) by NAT_1:12, NAT_1:13;
then k + 1 in dom p by FINSEQ_3:27;
then p . (k + 1) in INT by FINSEQ_2:13;
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 Instructions of SCM+FSA ^omega by AFINSQ_1:def 8;
take d ; :: thesis: S₁[k,d]
thus S₁[k,d] ; :: thesis: verum

end;

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

hereby :: thesis: tt = FlattenSeq pp

let k be Element of NAT ; :: thesis: ( k < len pp implies 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 ) )
assume A4: k < len pp ; :: thesis: 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 )
then ( 1 <= k + 1 & k + 1 <= len p ) by A2, NAT_1:12, NAT_1:13;
then k + 1 in dom p by FINSEQ_3:27;
then p . (k + 1) in INT by FINSEQ_2:13;
then reconsider i = p . (k + 1) as Integer ;
take i = i; :: thesis: ( i = p . (k + 1) & ((aSeq ((intloc 1),(k + 1))) ^ (aSeq ((intloc 2),i))) ^ <%((f,(intloc 1)) := (intloc 2))%> = pp . k )
thus i = p . (k + 1) ; :: thesis: ((aSeq ((intloc 1),(k + 1))) ^ (aSeq ((intloc 2),i))) ^ <%((f,(intloc 1)) := (intloc 2))%> = pp . k
k in len p by A2, A4, NAT_1:45;
then ( k in dom pp & S₁[k,pp . k] ) by A2, A3;
hence ((aSeq ((intloc 1),(k + 1))) ^ (aSeq ((intloc 2),i))) ^ <%((f,(intloc 1)) := (intloc 2))%> = pp . k ; :: thesis: verum

end;

thus tt = FlattenSeq pp ; :: thesis: verum