set k = (card F) -' 1;
A1: dom F = (dom (CutLastLoc F)) \/ {(LastLoc F)} by VALUED_1:37;
dom (Shift ((Stop S),((card F) -' 1))) = dom (((card F) -' 1) .--> (halt S)) by Th16
.= {((card F) -' 1)}
.= {(LastLoc F)} by AFINSQ_1:70 ;
then A2: dom (F ';' (Stop S)) = dom F by A1, FUNCT_4:def 1;
for x being object st x in dom F holds
(F ';' (Stop S)) . x = F . x
proof
let x be object ; :: thesis: ( x in dom F implies (F ';' (Stop S)) . x = F . x )
assume A3: x in dom F ; :: thesis: (F ';' (Stop S)) . x = F . x
dom (CutLastLoc F) misses dom (Reloc ((Stop S),((card F) -' 1))) by Th9;
then A4: {} = (dom (CutLastLoc F)) /\ (dom (Reloc ((Stop S),((card F) -' 1)))) ;
per cases ( x in dom (CutLastLoc F) or x in {(LastLoc F)} ) by A1, A3, XBOOLE_0:def 3;
suppose A5: x in dom (CutLastLoc F) ; :: thesis: (F ';' (Stop S)) . x = F . x
then not x in dom (Reloc ((Stop S),((card F) -' 1))) by A4, XBOOLE_0:def 4;
hence (F ';' (Stop S)) . x = (CutLastLoc F) . x by FUNCT_4:11
.= F . x by A5, GRFUNC_1:2 ;
:: thesis: verum
end;
suppose x in {(LastLoc F)} ; :: thesis: (F ';' (Stop S)) . x = F . x
then A6: x = LastLoc F by TARSKI:def 1;
then A7: x = (card F) -' 1 by AFINSQ_1:70;
A8: 0 in dom (Stop S) by TARSKI:def 1;
dom (Shift ((Stop S),((card F) -' 1))) = { (m + ((card F) -' 1)) where m is Nat : m in dom (Stop S) } by VALUED_1:def 12;
then 0 + ((card F) -' 1) in dom (Shift ((Stop S),((card F) -' 1))) by A8;
hence (F ';' (Stop S)) . x = (Shift ((Stop S),(0 + ((card F) -' 1)))) . x by A7, FUNCT_4:13
.= (Stop S) . 0 by A7, A8, VALUED_1:def 12
.= halt S
.= F . x by A6, Def6 ;
:: thesis: verum
end;
end;
end;
hence F ';' (Stop S) = F by A2, FUNCT_1:2; :: thesis: verum