let I1, I2 be XFinSequence of the Instructions of SCM ; :: thesis: for D being FinSequence of INT
for il, ps, ds being Element of NAT
for s being State-consisting of il,ps,ds,I1 ^ I2,D holds
( s is State-consisting of il,ps,ds,I1,D & s is State-consisting of il,ps + (len I1),ds,I2,D )
let D be FinSequence of INT ; :: thesis: for il, ps, ds being Element of NAT
for s being State-consisting of il,ps,ds,I1 ^ I2,D holds
( s is State-consisting of il,ps,ds,I1,D & s is State-consisting of il,ps + (len I1),ds,I2,D )
let il, ps, ds be Element of NAT ; :: thesis: for s being State-consisting of il,ps,ds,I1 ^ I2,D holds
( s is State-consisting of il,ps,ds,I1,D & s is State-consisting of il,ps + (len I1),ds,I2,D )
let s be State-consisting of il,ps,ds,I1 ^ I2,D; :: thesis: ( s is State-consisting of il,ps,ds,I1,D & s is State-consisting of il,ps + (len I1),ds,I2,D )
A1: IC s = il by SCM_1:def 1;
A2: len (I1 ^ I2) = (len I1) + (len I2) by AFINSQ_1:20;

A3: now

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

end;

A7: now

let k be Element of NAT ; :: thesis: ( k < len I1 implies s . (ps + k) = I1 . k )
assume A8: k < len I1 ; :: thesis: s . (ps + k) = I1 . k
len I1 <= (len I1) + (len I2) by NAT_1:11;
then k < len (I1 ^ I2) by A2, A8, XXREAL_0:2;
then A9: s . (ps + k) = (I1 ^ I2) . k by SCM_1:def 1;
k in dom I1 by A8, NAT_1:45;
hence s . (ps + k) = I1 . k by A9, AFINSQ_1:def 4; :: thesis: verum

end;

for k being Element of NAT st k < len D holds
s . (dl. (ds + k)) = D . (k + 1) by SCM_1:def 1;
hence s is State-consisting of il,ps,ds,I1,D by A1, A7, SCM_1:def 1; :: thesis: s is State-consisting of il,ps + (len I1),ds,I2,D
for k being Element of NAT st k < len D holds
s . (dl. (ds + k)) = D . (k + 1) by SCM_1:def 1;
hence s is State-consisting of il,ps + (len I1),ds,I2,D by A1, A3, SCM_1:def 1; :: thesis: verum