let i1, i2 be Integer; :: thesis: for il being Element of NAT

for s being b_{1} -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

for s being b

( 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