theorem :: VALUED_1:68

for F, G being NAT -defined non empty finite Function st dom F c= dom G holds
LastLoc F <= LastLoc G by XXREAL_2:59;