let F be NAT -defined non empty finite initial Function; :: thesis: LastLoc F = (card F) -' 1
consider k being natural number such that
A1: LastLoc F = k ;
reconsider k = k as Element of NAT by ORDINAL1:def 12;
LastLoc F in dom F by VALUED_1:30;
then k < card F by A1, Th70;
then A2: k <= (card F) -' 1 by NAT_D:49;

per cases ( k < (card F) -' 1 or k = (card F) -' 1 ) by A2, XXREAL_0:1;

suppose k < (card F) -' 1 ; :: thesis: LastLoc F = (card F) -' 1

then k + 1 < ((card F) -' 1) + 1 by XREAL_1:6;
then k + 1 < card F by NAT_1:14, XREAL_1:235;
then k + 1 in dom F by Th70;
then A3: k + 1 <= k by A1, VALUED_1:32;
k <= k + 1 by NAT_1:11;
then k + 0 = k + 1 by A3, XXREAL_0:1;
hence LastLoc F = (card F) -' 1 ; :: thesis: verum

end;

suppose k = (card F) -' 1 ; :: thesis: LastLoc F = (card F) -' 1

hence LastLoc F = (card F) -' 1 by A1; :: thesis: verum

end;

end;