let k be Nat; :: thesis: for N being with_zero set
for S being non empty with_non-empty_values IC-Ins-separated AMI-Struct over N ex f being non empty FinSequence of NAT st
( f /. 1 = k & f /. (len f) = k & ( for n being Nat st 1 <= n & n < len f holds
f /. (n + 1) in SUCC ((f /. n),S) ) )
let N be with_zero set ; :: thesis: for S being non empty with_non-empty_values IC-Ins-separated AMI-Struct over N ex f being non empty FinSequence of NAT st
( f /. 1 = k & f /. (len f) = k & ( for n being Nat st 1 <= n & n < len f holds
f /. (n + 1) in SUCC ((f /. n),S) ) )
let S be non empty with_non-empty_values IC-Ins-separated AMI-Struct over N; :: thesis: ex f being non empty FinSequence of NAT st
( f /. 1 = k & f /. (len f) = k & ( for n being Nat st 1 <= n & n < len f holds
f /. (n + 1) in SUCC ((f /. n),S) ) )
reconsider l = k as Element of NAT by ORDINAL1:def 12;
reconsider f = <*l*> as non empty FinSequence of NAT ;
take f ; :: thesis: ( f /. 1 = k & f /. (len f) = k & ( for n being 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 Nat st 1 <= n & n < len f holds
f /. (n + 1) in SUCC ((f /. n),S) ) )
hence ( f /. (len f) = k & ( for n being Nat st 1 <= n & n < len f holds
f /. (n + 1) in SUCC ((f /. n),S) ) ) by FINSEQ_1:39; :: thesis: verum