let l be Element of NAT ; :: 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) )
A2: (Initialized I) | NAT = I by SCMFSA6A:33;
dom ((Initialized I) | NAT ) c= dom (Initialized I) by RELAT_1:89;
hence ( l in dom I implies l in dom (Initialized I) ) by A2; :: thesis: ( l in dom (Initialized I) implies l in dom I )
A3: dom ((Initialized I) | NAT ) = (dom (Initialized I)) /\ NAT by RELAT_1:90;
assume l in dom (Initialized I) ; :: thesis: l in dom I
hence l in dom I by A2, A3, XBOOLE_0:def 4; :: thesis: verum