let N be with_zero set ; :: thesis: for T being non empty with_non-empty_values IC-Ins-separated weakly_standard AMI-Struct over N
for F being NAT -defined the InstructionsF of b₁ -valued non empty finite lower Function
for G being NAT -defined the InstructionsF of b₁ -valued non empty finite Function st F c= G & LastLoc F = LastLoc G holds
F = G
let T be non empty with_non-empty_values IC-Ins-separated weakly_standard AMI-Struct over N; :: thesis: for F being NAT -defined the InstructionsF of T -valued non empty finite lower Function
for G being NAT -defined the InstructionsF of T -valued non empty finite Function st F c= G & LastLoc F = LastLoc G holds
F = G
let F be NAT -defined the InstructionsF of T -valued non empty finite lower Function; :: thesis: for G being NAT -defined the InstructionsF of T -valued non empty finite Function st F c= G & LastLoc F = LastLoc G holds
F = G
let G be NAT -defined the InstructionsF of T -valued non empty finite Function; :: 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:2; :: according to XBOOLE_0:def 10 :: thesis: dom G c= dom F
let x be object ; :: 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
reconsider x = x as Element of NAT by A3;
A4: LastLoc F in dom F by Th28;
x <= LastLoc F,T by A2, A3, Th30;
hence x in dom F by A4, Def10; :: thesis: verum

end;

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