let N be with_non-empty_elements set ; :: thesis: for T being non empty stored-program IC-Ins-separated definite standard AMI-Struct of NAT ,N
for F being non empty programmed lower FinPartState of T
for G being non empty programmed FinPartState of T st F c= G & LastLoc F = LastLoc G holds
F = G
let T be non empty stored-program IC-Ins-separated definite standard AMI-Struct of NAT ,N; :: thesis: for F being non empty programmed lower FinPartState of T
for G being non empty programmed FinPartState of T st F c= G & LastLoc F = LastLoc G holds
F = G
let F be non empty programmed lower FinPartState of T; :: thesis: for G being non empty programmed FinPartState of T st F c= G & LastLoc F = LastLoc G holds
F = G
let G be non empty programmed FinPartState of T; :: thesis: ( F c= G & LastLoc F = LastLoc G implies F = G )
assume that
A1: F c= G and
A2: LastLoc F = LastLoc G ; :: thesis: F = G
dom F = dom G

proof

thus dom F c= dom G by A1, GRFUNC_1:8; :: according to XBOOLE_0:def 10 :: thesis: dom G c= dom F
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in dom G or x in dom F )
assume A3: x in dom G ; :: thesis: x in dom F
dom G c= NAT by AMI_1:def 40;
then reconsider x = x as Instruction-Location of T by A3, AMI_1:def 4;
A4: x <= LastLoc F by A2, A3, Th53;
LastLoc F in dom F by Th51;
hence x in dom F by A4, Def20; :: thesis: verum

end;

hence F = G by A1, GRFUNC_1:9; :: thesis: verum