let k be Element of NAT ; :: thesis: for N being with_zero set
for S being non empty with_non-empty_values IC-Ins-separated AMI-Struct over N holds k <= k,S
let N be with_zero set ; :: thesis: for S being non empty with_non-empty_values IC-Ins-separated AMI-Struct over N holds k <= k,S
let S be non empty with_non-empty_values IC-Ins-separated AMI-Struct over 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 1 :: 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