let i1, i2 be Integer; :: thesis: for il being Element of NAT
for s being b₁ -started State-consisting of <%i1,i2%> holds
( s . (dl. 0) = i1 & s . (dl. 1) = i2 )
let il be Element of NAT ; :: thesis: for s being il -started State-consisting of <%i1,i2%> holds
( s . (dl. 0) = i1 & s . (dl. 1) = i2 )
let s be il -started State-consisting of <%i1,i2%>; :: thesis: ( s . (dl. 0) = i1 & s . (dl. 1) = i2 )
set data = <%i1,i2%>;
A1: ( len <%i1,i2%> = 2 & <%i1,i2%> . 0 = i1 ) by AFINSQ_1:38;
<%i1,i2%> . 1 = i2 ;
hence ( s . (dl. 0) = i1 & s . (dl. 1) = i2 ) by A1, Def1; :: thesis: verum