let S be State of SCM ; :: thesis: for s1, s being State of SCM+FSA st s1 = (s +* S) +* (s | NAT ) holds
s1 . (IC SCM+FSA ) = S . (IC SCM )
let s1, s be State of SCM+FSA ; :: thesis: ( s1 = (s +* S) +* (s | NAT ) implies s1 . (IC SCM+FSA ) = S . (IC SCM ) )
A1: dom S = the carrier of SCM by PARTFUN1:def 4
.= SCM-Memory ;
( dom (s | NAT ) = (dom s) /\ NAT & not IC SCM+FSA in NAT ) by FUNCT_7:def 1, RELAT_1:90, SCMFSA_1:5;
then A2: not IC SCM+FSA in dom (s | NAT ) by XBOOLE_0:def 4;
assume s1 = (s +* S) +* (s | NAT ) ; :: thesis: s1 . (IC SCM+FSA ) = S . (IC SCM )
hence s1 . (IC SCM+FSA ) = (s +* S) . (IC SCM+FSA ) by A2, FUNCT_4:12
.= S . (IC SCM ) by A1, Th7, AMI_3:4, FUNCT_4:14 ;
:: thesis: verum