consider UIL being Function of the Instructions of SCM+FSA ,(Fin FinSeq-Locations ) such that
A1: ( ( for i being Instruction of SCM+FSA holds UIL . i = UsedInt*Loc i ) & UsedInt*Loc p = Union (UIL * p) ) by Def4;
reconsider dp = dom p as finite set ;
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