set G = CutLastLoc F;

per cases ( CutLastLoc F is empty or not CutLastLoc F is empty ) ;

suppose CutLastLoc F is empty ; :: thesis: CutLastLoc F is initial

then reconsider H = CutLastLoc F as empty finite Function ;
H is initial ;
hence CutLastLoc F is initial ; :: thesis: verum

end;

suppose not CutLastLoc F is empty ; :: thesis: CutLastLoc F is initial

then reconsider G = CutLastLoc F as non empty finite Function ;
G is initial

proof

let m, l be Nat; :: according to AFINSQ_1:def 13 :: thesis: ( l in dom G & m < l implies m in dom G )
assume that
A1: l in dom G and
A2: m < l ; :: thesis: m in dom G
set M = dom F;
reconsider R = {[(LastLoc F),(F . (LastLoc F))]} as Relation ;
R = (LastLoc F) .--> (F . (LastLoc F)) by FUNCT_4:87;
then A5: dom R = {(LastLoc F)} by FUNCOP_1:19;
then A6: (dom F) \ (dom R) = dom G by VALUED_1:37;
then l in dom F by A1, XBOOLE_0:def 5;
then A7: m in dom F by A2, Def13;
l in dom F by A6, A1, XBOOLE_0:def 5;
then m <> LastLoc F by A2, XXREAL_2:def 8;
then not m in {(LastLoc F)} by TARSKI:def 1;
hence m in dom G by A5, A6, A7, XBOOLE_0:def 5; :: thesis: verum

end;

hence CutLastLoc F is initial ; :: thesis: verum

end;

end;