let n be Nat; :: thesis: for i1, i2, i3 being Integer
for s being n -started State-consisting of <%i1,i2,i3%> holds
( s . (dl. 0) = i1 & s . (dl. 1) = i2 & s . (dl. 2) = i3 )
let i1, i2, i3 be Integer; :: thesis: for s being n -started State-consisting of <%i1,i2,i3%> holds
( s . (dl. 0) = i1 & s . (dl. 1) = i2 & s . (dl. 2) = i3 )
let s be n -started State-consisting of <%i1,i2,i3%>; :: thesis: ( s . (dl. 0) = i1 & s . (dl. 1) = i2 & s . (dl. 2) = i3 )
set D = <%i1,i2,i3%>;
A1: len <%i1,i2,i3%> = 3 by AFINSQ_1:39;
( <%i1,i2,i3%> . 0 = i1 & <%i1,i2,i3%> . 1 = i2 & <%i1,i2,i3%> . 2 = i3 ) ;
hence ( s . (dl. 0) = i1 & s . (dl. 1) = i2 & s . (dl. 2) = i3 ) by A1, SCM_1:def 1; :: thesis: verum