let F be NAT -defined non empty finite initial Function; :: thesis: for G being NAT -defined non empty finite Function st F c= G & LastLoc F = LastLoc G holds
F = G
let G be NAT -defined non empty finite Function; :: thesis: ( F c= G & LastLoc F = LastLoc G implies F = G )
assume that
A1: F c= G and
A2: LastLoc F = LastLoc G ; :: thesis: F = G
dom F = dom G

proof

thus dom F c= dom G by A1, GRFUNC_1:2; :: according to XBOOLE_0:def 10 :: thesis: dom G c= dom F
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in dom G or x in dom F )
assume A3: x in dom G ; :: thesis: x in dom F
dom G c= NAT by RELAT_1:def 18;
then reconsider x = x as Element of NAT by A3;
A4: LastLoc F in dom F by VALUED_1:30;
x <= LastLoc F by A2, A3, VALUED_1:32;
then ( x < LastLoc F or x = LastLoc F ) by XXREAL_0:1;
hence x in dom F by A4, Def12; :: thesis: verum

end;

hence F = G by A1, GRFUNC_1:3; :: thesis: verum