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 <%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 <%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 <%i1,i2,i3,i4%>

set D = <%i1,i2,i3,i4%>;

s is State-consisting of <%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 <%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 <%i1,i2,i3,i4%>

set D = <%i1,i2,i3,i4%>;

now :: thesis: for k being Element of NAT st k < len <%i1,i2,i3,i4%> holds

s . (dl. k) = <%i1,i2,i3,i4%> . k

hence
s is State-consisting of <%i1,i2,i3,i4%>
by Def1; :: thesis: verums . (dl. k) = <%i1,i2,i3,i4%> . k

let k be Element of NAT ; :: thesis: ( k < len <%i1,i2,i3,i4%> implies s . (dl. k) = <%i1,i2,i3,i4%> . k )

A2: ( len <%i1,i2,i3,i4%> = 4 & 4 = 3 + 1 ) by AFINSQ_1:84;

assume k < len <%i1,i2,i3,i4%> ; :: thesis: s . (dl. k) = <%i1,i2,i3,i4%> . k

then k <= 3 by A2, NAT_1:13;

then not not k = 0 & ... & not k = 3 ;

hence s . (dl. k) = <%i1,i2,i3,i4%> . k by A1; :: thesis: verum

end;A2: ( len <%i1,i2,i3,i4%> = 4 & 4 = 3 + 1 ) by AFINSQ_1:84;

assume k < len <%i1,i2,i3,i4%> ; :: thesis: s . (dl. k) = <%i1,i2,i3,i4%> . k

then k <= 3 by A2, NAT_1:13;

then not not k = 0 & ... & not k = 3 ;

hence s . (dl. k) = <%i1,i2,i3,i4%> . k by A1; :: thesis: verum