let N be with_non-empty_elements set ; :: thesis: for S being non empty stored-program IC-Ins-separated definite standard-ins standard regular AMI-Struct of NAT ,N
for F being NAT -defined non empty lower FinPartState of S
for G being NAT -defined non empty FinPartState of S holds
( card (F ';' G) = ((card F) + (card G)) - 1 & card (F ';' G) = ((card F) + (card G)) -' 1 )
let S be non empty stored-program IC-Ins-separated definite standard-ins standard regular AMI-Struct of NAT ,N; :: thesis: for F being NAT -defined non empty lower FinPartState of S
for G being NAT -defined non empty FinPartState of S holds
( card (F ';' G) = ((card F) + (card G)) - 1 & card (F ';' G) = ((card F) + (card G)) -' 1 )
let F be NAT -defined non empty lower FinPartState of S; :: thesis: for G being NAT -defined non empty FinPartState of S holds
( card (F ';' G) = ((card F) + (card G)) - 1 & card (F ';' G) = ((card F) + (card G)) -' 1 )
let G be NAT -defined non empty FinPartState of S; :: thesis: ( card (F ';' G) = ((card F) + (card G)) - 1 & card (F ';' G) = ((card F) + (card G)) -' 1 )
set k = (card F) -' 1;
dom (IncAddr G,((card F) -' 1)), dom (Shift (IncAddr G,((card F) -' 1)),((card F) -' 1)) are_equipotent by Th43;
then A1: IncAddr G,((card F) -' 1), Shift (IncAddr G,((card F) -' 1)),((card F) -' 1) are_equipotent by PRE_CIRC:26;
dom (CutLastLoc F) misses dom (Shift (IncAddr G,((card F) -' 1)),((card F) -' 1)) by Th50;
hence card (F ';' G) = (card (CutLastLoc F)) + (card (Shift (IncAddr G,((card F) -' 1)),((card F) -' 1))) by PRE_CIRC:27
.= (card (CutLastLoc F)) + (card (IncAddr G,((card F) -' 1))) by A1, CARD_1:21
.= (card (CutLastLoc F)) + (card (dom (IncAddr G,((card F) -' 1)))) by CARD_1:104
.= (card (CutLastLoc F)) + (card (dom G)) by Def15
.= (card (CutLastLoc F)) + (card G) by CARD_1:104
.= ((card F) - 1) + (card G) by Th49
.= ((card F) + (card G)) - 1 ;
:: thesis: card (F ';' G) = ((card F) + (card G)) -' 1
hence card (F ';' G) = ((card F) + (card G)) -' 1 by XREAL_0:def 2; :: thesis: verum