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 ) )
assume A1: s1 = (s +* S) +* (s | NAT ) ; :: thesis: s1 . (IC SCM+FSA ) = S . (IC SCM )
A2: dom (s | NAT ) = (dom s) /\ NAT by RELAT_1:90;
not IC SCM+FSA in NAT by Th7;
then A3: not IC SCM+FSA in dom (s | NAT ) by A2, XBOOLE_0:def 4;
A4: dom S = dom SCM-OK by CARD_3:18
.= SCM-Memory by FUNCT_2:def 1 ;
thus s1 . (IC SCM+FSA ) = (s +* S) . (IC SCM+FSA ) by A1, A3, FUNCT_4:12
.= S . (IC SCM ) by A4, Th7, AMI_3:4, FUNCT_4:14 ; :: thesis: verum