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