for F, G being NAT -defined non empty finite Function st dom F = dom G holds
LastLoc F = LastLoc G ;