let k be Element of NAT ; :: thesis: for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite AMI-Struct of N holds k <= k,S
let N be non empty with_non-empty_elements set ; :: thesis: for S being non empty stored-program IC-Ins-separated definite AMI-Struct of N holds k <= k,S
let S be non empty stored-program IC-Ins-separated definite AMI-Struct of N; :: thesis: k <= k,S
reconsider l = k as Element of NAT ;
reconsider f = <*l*> as non empty FinSequence of NAT ;
take f ; :: according to AMI_WSTD:def 8 :: thesis: ( f /. 1 = k & f /. (len f) = k & ( for n being Element of NAT st 1 <= n & n < len f holds
f /. (n + 1) in SUCC ((f /. n),S) ) )
thus f /. 1 = k by FINSEQ_4:25; :: thesis: ( f /. (len f) = k & ( for n being Element of NAT st 1 <= n & n < len f holds
f /. (n + 1) in SUCC ((f /. n),S) ) )
hence ( f /. (len f) = k & ( for n being Element of NAT st 1 <= n & n < len f holds
f /. (n + 1) in SUCC ((f /. n),S) ) ) by FINSEQ_1:56; :: thesis: verum