let F be NAT -defined non empty finite Function; :: thesis: card (CutLastLoc F) = (card F) - 1
(LastLoc F) .--> (F . (LastLoc F)) c= F

proof

let a, b be set ; :: according to RELAT_1:def 3 :: thesis: ( not [a,b] in (LastLoc F) .--> (F . (LastLoc F)) or [a,b] in F )
assume [a,b] in (LastLoc F) .--> (F . (LastLoc F)) ; :: thesis: [a,b] in F
then [a,b] in {[(LastLoc F),(F . (LastLoc F))]} by FUNCT_4:82;
then A1: [a,b] = [(LastLoc F),(F . (LastLoc F))] by TARSKI:def 1;
LastLoc F in dom F by Th31;
hence [a,b] in F by A1, FUNCT_1:def 2; :: thesis: verum

end;

hence card (CutLastLoc F) = (card F) - (card ((LastLoc F) .--> (F . (LastLoc F)))) by CARD_2:44
.= (card F) - (card {[(LastLoc F),(F . (LastLoc F))]}) by FUNCT_4:82
.= (card F) - 1 by CARD_1:30 ;
:: thesis: verum