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