let I1, I2 be XFinSequence of the Instructions of SCM ; :: thesis: for il, ps, ds, k, il1 being Element of NAT
for s being State-consisting of il,ps,ds,I1 ^ I2, <*> INT
for u being State of SCM st u = Comput (ProgramPart s),s,k & il1 = IC u holds
u is State-consisting of il1,ps + (len I1),ds,I2, <*> INT
let il, ps, ds, k1, il1 be Element of NAT ; :: thesis: for s being State-consisting of il,ps,ds,I1 ^ I2, <*> INT
for u being State of SCM st u = Comput (ProgramPart s),s,k1 & il1 = IC u holds
u is State-consisting of il1,ps + (len I1),ds,I2, <*> INT
let s be State-consisting of il,ps,ds,I1 ^ I2, <*> INT ; :: thesis: for u being State of SCM st u = Comput (ProgramPart s),s,k1 & il1 = IC u holds
u is State-consisting of il1,ps + (len I1),ds,I2, <*> INT
let u be State of SCM ; :: thesis: ( u = Comput (ProgramPart s),s,k1 & il1 = IC u implies u is State-consisting of il1,ps + (len I1),ds,I2, <*> INT )
assume that
A1: u = Comput (ProgramPart s),s,k1 and
A2: il1 = IC u ; :: thesis: u is State-consisting of il1,ps + (len I1),ds,I2, <*> INT
A3: len (I1 ^ I2) = (len I1) + (len I2) by AFINSQ_1:20;

A4: now

let k be Element of NAT ; :: thesis: ( k < len I2 implies u . ((ps + (len I1)) + k) = I2 . k )
assume k < len I2 ; :: thesis: u . ((ps + (len I1)) + k) = I2 . k
then A6: (len I1) + k < len (I1 ^ I2) by A3, XREAL_1:8;
A7: s . ((ps + (len I1)) + k) = s . (ps + ((len I1) + k))
.= (I1 ^ I2) . ((len I1) + k) by A6, SCM_1:def 1 ;
(I1 ^ I2) . ((len I1) + k) = I2 . (((len I1) + k) - (len I1)) by A3, A6, AFINSQ_1:21, NAT_1:11
.= I2 . k ;
hence u . ((ps + (len I1)) + k) = I2 . k by A1, A7, AMI_1:54; :: thesis: verum

end;

for k being Element of NAT st k < len (<*> INT ) holds
u . (dl. (ds + k)) = (<*> INT ) . (k + 1) by CARD_1:47;
hence u is State-consisting of il1,ps + (len I1),ds,I2, <*> INT by A2, A4, SCM_1:def 1; :: thesis: verum