let F be NAT -defined non empty finite Function; card (CutLastLoc F) = (card F) - 1
(LastLoc F) .--> (F . (LastLoc F)) c= F
proof
let a,
b be
object ;
RELAT_1:def 3 ( not [a,b] in (LastLoc F) .--> (F . (LastLoc F)) or [a,b] in F )
assume
[a,b] in (LastLoc F) .--> (F . (LastLoc F))
;
[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 XXREAL_2:def 8;
hence
[a,b] in F
by A1, FUNCT_1:def 2;
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
;
verum