let S be State of SCM; :: thesis: for s, s1 being State of SCM+FSA st s1 = s +* S holds
s1 . (IC ) = S . (IC )
let s, s1 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 . (IC ) by A1, Th1, AMI_3:1, FUNCT_4:13; :: thesis: verum