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;
A3: FirstLoc G = min (dom G) ;
set M = dom F;
dom F c= dom G by A1, RELAT_1:25;
then min (dom G) <= min (dom F) by XXREAL_2:60;
hence FirstLoc G <= FirstLoc F by A3; :: thesis: verum