let N be with_non-empty_elements set ; :: thesis: for S being non empty stored-program IC-Ins-separated definite standard-ins standard regular AMI-Struct of NAT ,N
for F, G being NAT -defined non empty lower FinPartState of S holds dom F c= dom (F ';' G)
let S be non empty stored-program IC-Ins-separated definite standard-ins standard regular AMI-Struct of NAT ,N; :: thesis: for F, G being NAT -defined non empty lower FinPartState of S holds dom F c= dom (F ';' G)
let F, G be NAT -defined non empty lower FinPartState of S; :: thesis: dom F c= dom (F ';' G)
set P = F ';' G;
A1: dom (F ';' G) = (dom (CutLastLoc F)) \/ (dom (Shift (IncAddr G,((card F) -' 1)),((card F) -' 1))) by FUNCT_4:def 1;
A2: dom F = (dom (CutLastLoc F)) \/ {(LastLoc F)} by Th48;
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in dom F or x in dom (F ';' G) )
assume A3: x in dom F ; :: thesis: x in dom (F ';' G)

per cases ( x in dom (CutLastLoc F) or x in {(LastLoc F)} ) by A2, A3, XBOOLE_0:def 3;

suppose x in dom (CutLastLoc F) ; :: thesis: x in dom (F ';' G)

hence x in dom (F ';' G) by A1, XBOOLE_0:def 3; :: thesis: verum

end;

suppose A4: x in {(LastLoc F)} ; :: thesis: x in dom (F ';' G)

then A5: x = LastLoc F by TARSKI:def 1;
reconsider f = x as Instruction-Location of S by A4, TARSKI:def 1;
A6: locnum f = locnum (il. S,((card F) -' 1)) by A5, AMISTD_1:55
.= (card F) -' 1 by AMISTD_1:def 13
.= ((card F) - 1) + 0 by PRE_CIRC:25 ;
A7: card (F ';' G) = ((card F) + (card G)) - 1 by Th52
.= ((card F) - 1) + (card G) ;
locnum f < card (F ';' G) by A6, A7, XREAL_1:8;
then il. S,(locnum f) in dom (F ';' G) by AMISTD_1:50;
hence x in dom (F ';' G) by AMISTD_1:def 13; :: thesis: verum

end;

end;