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

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