LastLoc F in dom F by XXREAL_2:def 8;
then A1: [(LastLoc F),(F . (LastLoc F))] in F by FUNCT_1:def 2;
assume not CutLastLoc F is empty ; :: thesis: contradiction
then consider a being object such that
A2: a in CutLastLoc F ;
A3: a = [(LastLoc F),(F . (LastLoc F))] by A1, A2, ZFMISC_1:def 10;
not a in (LastLoc F) .--> (F . (LastLoc F)) by A2, XBOOLE_0:def 5;
then not a in {[(LastLoc F),(F . (LastLoc F))]} by FUNCT_4:82;
hence contradiction by A3, TARSKI:def 1; :: thesis: verum