let F, G be NAT -defined non empty finite Function; :: thesis: ( F c= G implies FirstLoc G <= FirstLoc F )
assume A1: F c= G ; :: thesis: FirstLoc G <= FirstLoc F
set N = dom G;
set M = dom F;
dom F c= dom G by A1, RELAT_1:11;
then min (dom G) <= min (dom F) by XXREAL_2:60;
hence FirstLoc G <= FirstLoc F ; :: thesis: verum