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

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