let l be Instruction-Location of S; :: thesis: ex f being non empty IL-FinSequence of S st
( f /. 1 = l & f /. (len f) = l & ( for n being Element of NAT st 1 <= n & n < len f holds
f /. (n + 1) in SUCC (f /. n) ) )
A1: l in IL by AMI_1:def 4;
take <*l*> ; :: thesis: ( <*l*> /. 1 = l & <*l*> /. (len <*l*>) = l & ( for n being Element of NAT st 1 <= n & n < len <*l*> holds
<*l*> /. (n + 1) in SUCC (<*l*> /. n) ) )
thus <*l*> /. 1 = l by A1, FINSEQ_4:25; :: thesis: ( <*l*> /. (len <*l*>) = l & ( for n being Element of NAT st 1 <= n & n < len <*l*> holds
<*l*> /. (n + 1) in SUCC (<*l*> /. n) ) )
hence ( <*l*> /. (len <*l*>) = l & ( for n being Element of NAT st 1 <= n & n < len <*l*> holds
<*l*> /. (n + 1) in SUCC (<*l*> /. n) ) ) by FINSEQ_1:56; :: thesis: verum