let S be COM-Struct ; :: thesis: for F, G being Program of S
for n being Nat st n < LastLoc F holds
F . n = (F ';' G) . n
let F, G be Program of S; :: thesis: for n being Nat st n < LastLoc F holds
F . n = (F ';' G) . n
let f be Nat; :: thesis: ( f < LastLoc F implies F . f = (F ';' G) . f )
assume f < LastLoc F ; :: thesis: F . f = (F ';' G) . f
then f < (card F) - 1 by AFINSQ_1:91;
hence F . f = (F ';' G) . f by Lm6; :: thesis: verum