let S be with_non_trivial_Instructions COM-Struct ; :: thesis: for I, J being MacroInstruction of S holds LastLoc (I ';' J) = (LastLoc I) + (LastLoc J)
let I, J be MacroInstruction of S; :: thesis: LastLoc (I ';' J) = (LastLoc I) + (LastLoc J)
thus LastLoc (I ';' J) = (card (I ';' J)) - 1 by AFINSQ_1:91
.= (((card I) + (card J)) - 1) - 1 by COMPOS_1:20
.= ((card I) - 1) + ((card J) - 1)
.= (LastLoc I) + ((card J) - 1) by AFINSQ_1:91
.= (LastLoc I) + (LastLoc J) by AFINSQ_1:91 ; :: thesis: verum