let S be COM-Struct ; :: thesis: for F being Program of S
for G being non empty preProgram of S holds
( card (F ';' G) = ((card F) + (card G)) - 1 & card (F ';' G) = ((card F) + (card G)) -' 1 )
let F be Program of S; :: thesis: for G being non empty preProgram of S holds
( card (F ';' G) = ((card F) + (card G)) - 1 & card (F ';' G) = ((card F) + (card G)) -' 1 )
let G be non empty preProgram 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 (Reloc (G,((card F) -' 1))) are_equipotent by VALUED_1:27;
then A1: IncAddr (G,((card F) -' 1)), Reloc (G,((card F) -' 1)) are_equipotent by PRE_CIRC:21;
dom (CutLastLoc F) misses dom (Reloc (G,((card F) -' 1))) by Th9;
hence card (F ';' G) = (card (CutLastLoc F)) + (card (Reloc (G,((card F) -' 1)))) by PRE_CIRC:22
.= (card (CutLastLoc F)) + (card (IncAddr (G,((card F) -' 1)))) by A1, CARD_1:5
.= (card (CutLastLoc F)) + (card (dom (IncAddr (G,((card F) -' 1))))) by CARD_1:62
.= (card (CutLastLoc F)) + (card (dom G)) by Def9
.= (card (CutLastLoc F)) + (card G) by CARD_1:62
.= ((card F) - 1) + (card G) by VALUED_1:38
.= ((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