let l be Nat; :: thesis: for i being Instruction of SCM+FSA holds UsedILoc (l .--> i) = UsedIntLoc i
let i be Instruction of SCM+FSA; :: thesis: UsedILoc (l .--> i) = UsedIntLoc i
rng (l .--> i) = {i} by FUNCOP_1:8;
hence UsedILoc (l .--> i) = union { (UsedIntLoc i1) where i1 is Instruction of SCM+FSA : i1 in {i} }
.= UsedIntLoc i from SUBSET_1:sch 5() ;
:: thesis: verum