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 RELAT_1:def 19;
then reconsider p9 = p as Function of dp, the Instructions of SCM+FSA by FUNCT_2:2;
reconsider Up = UIL * p9 as Function of dp,(Fin Int-Locations) ;
Union Up is finite ;
hence UsedIntLoc p is finite by A1; :: thesis: verum