let k be Element of NAT ; :: thesis: for N being non empty with_non-empty_elements set
for S being non empty IC-Ins-separated AMI-Struct of N ex f being non empty FinSequence of NAT st
( 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) ) )
let N be non empty with_non-empty_elements set ; :: thesis: for S being non empty IC-Ins-separated AMI-Struct of N ex f being non empty FinSequence of NAT st
( 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) ) )
let S be non empty IC-Ins-separated AMI-Struct of N; :: thesis: ex f being non empty FinSequence of NAT st
( 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) ) )
reconsider l = k as Element of NAT ;
reconsider f = <*l*> as non empty FinSequence of NAT ;
take f ; :: 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:16; :: 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:39; :: thesis: verum