let i be Instruction of SCM+FSA; :: thesis: for J being Program of holds UsedILoc (i ";" J) = (UsedIntLoc i) \/ (UsedILoc J)

let J be Program of ; :: thesis: UsedILoc (i ";" J) = (UsedIntLoc i) \/ (UsedILoc J)

thus UsedILoc (i ";" J) = (UsedILoc (Macro i)) \/ (UsedILoc J) by Th27

.= (UsedIntLoc i) \/ (UsedILoc J) by Th28 ; :: thesis: verum

let J be Program of ; :: thesis: UsedILoc (i ";" J) = (UsedIntLoc i) \/ (UsedILoc J)

thus UsedILoc (i ";" J) = (UsedILoc (Macro i)) \/ (UsedILoc J) by Th27

.= (UsedIntLoc i) \/ (UsedILoc J) by Th28 ; :: thesis: verum