LastLoc F in dom F by Th31;
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 set such that
A2: a in CutLastLoc F by XBOOLE_0:def 1;
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