let s be State of SCM; :: thesis: for n being Element of NAT holds s is State-consisting of n, <*> INT
let n be Element of NAT ; :: thesis: s is State-consisting of n, <*> INT
let k be Element of NAT ; :: according to SCM_1:def 1 :: thesis: ( k < len (<*> INT) implies s . (dl. (n + k)) = (<*> INT) . (k + 1) )
thus ( k < len (<*> INT) implies s . (dl. (n + k)) = (<*> INT) . (k + 1) ) ; :: thesis: verum