theorem :: VALUED_1:31

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