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

let I be Program of ; :: thesis: UsedILoc (I ";" j) = (UsedILoc I) \/ (UsedIntLoc j)

thus UsedILoc (I ";" j) = (UsedILoc I) \/ (UsedILoc (Macro j)) by Th27

.= (UsedILoc I) \/ (UsedIntLoc j) by Th28 ; :: thesis: verum

let I be Program of ; :: thesis: UsedILoc (I ";" j) = (UsedILoc I) \/ (UsedIntLoc j)

thus UsedILoc (I ";" j) = (UsedILoc I) \/ (UsedILoc (Macro j)) by Th27

.= (UsedILoc I) \/ (UsedIntLoc j) by Th28 ; :: thesis: verum