let I be Program of SCMPDS ; :: thesis: for l being Nat holds
( l in dom I iff l in dom (Initialized I) )
let l be Nat; :: thesis: ( l in dom I iff l in dom (Initialized I) )
A1: (Initialized I) | NAT = I by SCMPDS_4:16;
A2: dom ((Initialized I) | NAT ) c= dom (Initialized I) by RELAT_1:89;
A3: dom ((Initialized I) | NAT ) = (dom (Initialized I)) /\ NAT by RELAT_1:90;
thus ( l in dom I implies l in dom (Initialized I) ) by A1, A2; :: thesis: ( l in dom (Initialized I) implies l in dom I )
A4: l in NAT by ORDINAL1:def 13;
assume l in dom (Initialized I) ; :: thesis: l in dom I
hence l in dom I by A1, A3, A4, XBOOLE_0:def 4; :: thesis: verum