reconsider dp = dom p as finite set ;
consider UIL being Function of the Instructions of SCM+FSA , Fin FinSeq-Locations such that
for i being Instruction of holds UIL . i = UsedInt*Loc i and
A1: UsedInt*Loc p = Union (UIL * p) by Def4;
rng p c= the Instructions of SCM+FSA by AMI_1:118;
then reconsider p' = p as Function of dp,the Instructions of SCM+FSA by FUNCT_2:4;
reconsider Up = UIL * p' as Function of dp, Fin FinSeq-Locations ;
Union Up is finite ;
hence UsedInt*Loc p is finite by A1; :: thesis: verum