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