let S be standard-ins homogeneous regular J/A-independent COM-Struct ; :: thesis: for F, G being non empty initial preProgram of S
for f being Nat st f < (card F) - 1 holds
(IncAddr (F,((card F) -' 1))) . f = (IncAddr ((F ';' G),((card F) -' 1))) . f
let F, G be non empty initial preProgram of S; :: thesis: for f being Nat st f < (card F) - 1 holds
(IncAddr (F,((card F) -' 1))) . f = (IncAddr ((F ';' G),((card F) -' 1))) . f
let f be Nat; :: thesis: ( f < (card F) - 1 implies (IncAddr (F,((card F) -' 1))) . f = (IncAddr ((F ';' G),((card F) -' 1))) . f )
set k = (card F) -' 1;
set P = F ';' G;
assume f < (card F) - 1 ; :: thesis: (IncAddr (F,((card F) -' 1))) . f = (IncAddr ((F ';' G),((card F) -' 1))) . f
then f < card (CutLastLoc F) by VALUED_1:38;
then A1: f in dom (CutLastLoc F) by AFINSQ_1:66;
A2: dom (CutLastLoc F) c= dom F by GRFUNC_1:2;
CutLastLoc F c= CutLastLoc (F ';' G) by Th104;
then CutLastLoc F c= F ';' G by XBOOLE_1:1;
then A3: dom (CutLastLoc F) c= dom (F ';' G) by GRFUNC_1:2;
A4: F . f = F /. f by A1, A2, PARTFUN1:def 6;
dom (CutLastLoc F) misses dom (Shift ((IncAddr (G,((card F) -' 1))),((card F) -' 1))) by Th100;
then (dom (CutLastLoc F)) /\ (dom (Shift ((IncAddr (G,((card F) -' 1))),((card F) -' 1)))) = {} by XBOOLE_0:def 7;
then not f in dom (Shift ((IncAddr (G,((card F) -' 1))),((card F) -' 1))) by A1, XBOOLE_0:def 4;
then A5: (F ';' G) . f = (CutLastLoc F) . f by FUNCT_4:11
.= F . f by A1, GRFUNC_1:2 ;
thus (IncAddr (F,((card F) -' 1))) . f = IncAddr ((F /. f),((card F) -' 1)) by A1, A2, Def40
.= IncAddr (((F ';' G) /. f),((card F) -' 1)) by A1, A3, A4, A5, PARTFUN1:def 6
.= (IncAddr ((F ';' G),((card F) -' 1))) . f by A1, A3, Def40 ; :: thesis: verum