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