let S be standard-ins homogeneous regular J/A-independent COM-Struct ; :: thesis: for F being pre-Macro of S holds (Stop S) ';' F = F
let F be pre-Macro of S; :: thesis: (Stop S) ';' F = F
set k = (card (Stop S)) -' 1;
A1: (card (Stop S)) -' 1 = 0 by Lm13;
hence (Stop S) ';' F = (CutLastLoc (Stop S)) +* (Shift (F,((card (Stop S)) -' 1))) by Th98
.= (CutLastLoc (Stop S)) +* F by A1, VALUED_1:28
.= F by FUNCT_4:20 ;
:: thesis: verum