let N be non empty with_non-empty_elements set ; :: thesis: for T being non empty IC-Ins-separated weakly_standard AMI-Struct of N
for F being NAT -defined the Instructions of b₁ -valued non empty finite lower Function
for G being NAT -defined the Instructions of b₁ -valued non empty finite Function st F c= G & LastLoc F = LastLoc G holds
F = G
let T be non empty IC-Ins-separated weakly_standard AMI-Struct of N; :: thesis: for F being NAT -defined the Instructions of T -valued non empty finite lower Function
for G being NAT -defined the Instructions of T -valued non empty finite Function st F c= G & LastLoc F = LastLoc G holds
F = G
let F be NAT -defined the Instructions of T -valued non empty finite lower Function; :: thesis: for G being NAT -defined the Instructions of T -valued non empty finite Function st F c= G & LastLoc F = LastLoc G holds
F = G
let G be NAT -defined the Instructions 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 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 RELAT_1:def 18;
then reconsider x = x as Element of NAT by A3;
A4: LastLoc F in dom F by Th51;
x <= LastLoc F,T by A2, A3, Th53;
hence x in dom F by A4, Def20; :: thesis: verum

end;

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