let i1, i2, i3, i4 be Integer; :: thesis: for s being State of SCM st s . (dl. 0) = i1 & s . (dl. 1) = i2 & s . (dl. 2) = i3 & s . (dl. 3) = i4 holds
s is State-consisting of 0 ,((<*i1*> ^ <*i2*>) ^ <*i3*>) ^ <*i4*>
let s be State of SCM; :: thesis: ( s . (dl. 0) = i1 & s . (dl. 1) = i2 & s . (dl. 2) = i3 & s . (dl. 3) = i4 implies s is State-consisting of 0 ,((<*i1*> ^ <*i2*>) ^ <*i3*>) ^ <*i4*> )
assume A1: ( s . (dl. 0) = i1 & s . (dl. 1) = i2 & s . (dl. 2) = i3 & s . (dl. 3) = i4 ) ; :: thesis: s is State-consisting of 0 ,((<*i1*> ^ <*i2*>) ^ <*i3*>) ^ <*i4*>
set D = ((<*i1*> ^ <*i2*>) ^ <*i3*>) ^ <*i4*>;

now

let k be Element of NAT ; :: thesis: ( k < len (((<*i1*> ^ <*i2*>) ^ <*i3*>) ^ <*i4*>) implies s . (dl. (0 + k)) = (((<*i1*> ^ <*i2*>) ^ <*i3*>) ^ <*i4*>) . (k + 1) )
A2: ( len (((<*i1*> ^ <*i2*>) ^ <*i3*>) ^ <*i4*>) = 4 & 4 = 3 + 1 ) by FINSEQ_1:66;
A3: 3 = 2 + 1 ;
assume k < len (((<*i1*> ^ <*i2*>) ^ <*i3*>) ^ <*i4*>) ; :: thesis: s . (dl. (0 + k)) = (((<*i1*> ^ <*i2*>) ^ <*i3*>) ^ <*i4*>) . (k + 1)
then k <= 3 by A2, NAT_1:13;
then A4: ( k <= 2 or k = 3 ) by A3, NAT_1:8;
A5: 1 = 0 + 1 ;
2 = 1 + 1 ;
then ( k <= 1 or k = 2 or k = 3 ) by A4, NAT_1:8;
then ( k = 0 or k = 1 or k = 2 or k = 3 ) by A5, NAT_1:8;
hence s . (dl. (0 + k)) = (((<*i1*> ^ <*i2*>) ^ <*i3*>) ^ <*i4*>) . (k + 1) by A1, FINSEQ_1:66; :: thesis: verum

end;

hence s is State-consisting of 0 ,((<*i1*> ^ <*i2*>) ^ <*i3*>) ^ <*i4*> by Def1; :: thesis: verum