theorem :: VALUED_1:34

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