let N be with_non-empty_elements set ; :: thesis: for S being non empty stored-program IC-Ins-separated definite standard AMI-Struct of NAT ,N
for F being non empty programmed FinPartState of S holds card (CutLastLoc F) = (card F) - 1
let S be non empty stored-program IC-Ins-separated definite standard AMI-Struct of NAT ,N; :: thesis: for F being non empty programmed FinPartState of S holds card (CutLastLoc F) = (card F) - 1
let F be non empty programmed FinPartState of S; :: 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:87;
then A1: [a,b] = [(LastLoc F),(F . (LastLoc F))] by TARSKI:def 1;
LastLoc F in dom F by AMISTD_1:51;
hence [a,b] in F by A1, FUNCT_1:def 4; :: thesis: verum

end;

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