let S be standard-ins homogeneous regular J/A-independent COM-Struct ; :: thesis: for F being non empty initial preProgram of S
for G being non empty NAT -defined the Instructions of S -valued finite Function holds
( card (F ';' G) = ((card F) + (card G)) - 1 & card (F ';' G) = ((card F) + (card G)) -' 1 )
let F be non empty initial preProgram of S; :: thesis: for G being non empty NAT -defined the Instructions of S -valued finite Function holds
( card (F ';' G) = ((card F) + (card G)) - 1 & card (F ';' G) = ((card F) + (card G)) -' 1 )
let G be non empty NAT -defined the Instructions of S -valued finite Function; :: 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 VALUED_1:27;
then A1: IncAddr (G,((card F) -' 1)), Shift ((IncAddr (G,((card F) -' 1))),((card F) -' 1)) are_equipotent by PRE_CIRC:21;
dom (CutLastLoc F) misses dom (Shift ((IncAddr (G,((card F) -' 1))),((card F) -' 1))) by Th100;
hence card (F ';' G) = (card (CutLastLoc F)) + (card (Shift ((IncAddr (G,((card F) -' 1))),((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 Def40
.= (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