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