let j be Instruction of SCM+FSA; :: thesis: for I being Program of {INT,(INT *)} holds UsedIntLoc (I ';' j) = (UsedIntLoc I) \/ (UsedIntLoc j)
let I be Program of {INT,(INT *)}; :: thesis: UsedIntLoc (I ';' j) = (UsedIntLoc I) \/ (UsedIntLoc j)
thus UsedIntLoc (I ';' j) = (UsedIntLoc I) \/ (UsedIntLoc (Macro j)) by Th31
.= (UsedIntLoc I) \/ (UsedIntLoc j) by Th32 ; :: thesis: verum