let i1, i2 be Integer; :: thesis: for il being Element of NAT
for s being b₁ -started State-consisting of 0 ,<*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 0 ,<*i1*> ^ <*i2*> holds
( s . (dl. 0) = i1 & s . (dl. 1) = i2 )
let s be il -started State-consisting of 0 ,<*i1*> ^ <*i2*>; :: thesis: ( s . (dl. 0) = i1 & s . (dl. 1) = i2 )
set data = <*i1*> ^ <*i2*>;
A1: 0 + 0 = 0 ;
A2: <*i1*> ^ <*i2*> = <*i1,i2*> by FINSEQ_1:def 9;
then A3: ( len (<*i1*> ^ <*i2*>) = 2 & (<*i1*> ^ <*i2*>) . (0 + 1) = i1 ) by FINSEQ_1:44;
(<*i1*> ^ <*i2*>) . (1 + 1) = i2 by A2, FINSEQ_1:44;
hence ( s . (dl. 0) = i1 & s . (dl. 1) = i2 ) by A3, A1, Def1; :: thesis: verum