let l be Instruction-Location of SCM+FSA ; :: thesis: for I being Program of SCM+FSA holds
( l in dom I iff l in dom (Initialized I) )
let I be Program of SCM+FSA ; :: thesis: ( l in dom I iff l in dom (Initialized I) )
A1: l in NAT by AMI_1:def 4;
A2: (Initialized I) | NAT = I by SCMFSA6A:33;
A3: dom ((Initialized I) | NAT ) c= dom (Initialized I) by RELAT_1:89;
A4: dom ((Initialized I) | NAT ) = (dom (Initialized I)) /\ NAT by RELAT_1:90;
thus ( l in dom I implies l in dom (Initialized I) ) by A2, A3; :: thesis: ( l in dom (Initialized I) implies l in dom I )
assume l in dom (Initialized I) ; :: thesis: l in dom I
hence l in dom I by A1, A2, A4, XBOOLE_0:def 4; :: thesis: verum