let S be State of SCM; :: thesis: for s1, s being State of SCM+FSA st s1 = s +* S holds
s1 . (IC ) = S . (IC )
let s1, s be State of SCM+FSA; :: thesis: ( s1 = s +* S implies s1 . (IC ) = S . (IC ) )
A1: dom S = SCM-Memory by PARTFUN1:def 2;
assume s1 = s +* S ; :: thesis: s1 . (IC ) = S . (IC )
hence s1 . (IC ) = (s +* S) . (IC )
.= S . (IC ) by A1, Th7, AMI_3:1, FUNCT_4:13 ;
:: thesis: verum