let S be COM-Struct ; :: thesis: for F, G being Program of S
for f being Nat st f < (card F) - 1 holds
F . f = (F ';' G) . f
let F, G be Program of S; :: thesis: for f being Nat st f < (card F) - 1 holds
F . f = (F ';' G) . f
let f be Nat; :: thesis: ( f < (card F) - 1 implies F . f = (F ';' G) . f )
set k = (card F) -' 1;
set P = F ';' G;
assume f < (card F) - 1 ; :: thesis: F . f = (F ';' G) . f
then f < card (CutLastLoc F) by VALUED_1:38;
then A1: f in dom (CutLastLoc F) by AFINSQ_1:66;
dom (CutLastLoc F) misses dom (Reloc (G,((card F) -' 1))) by Th9;
then (dom (CutLastLoc F)) /\ (dom (Reloc (G,((card F) -' 1)))) = {} ;
then not f in dom (Reloc (G,((card F) -' 1))) by A1, XBOOLE_0:def 4;
hence (F ';' G) . f = (CutLastLoc F) . f by FUNCT_4:11
.= F . f by A1, GRFUNC_1:2 ;
:: thesis: verum