let I be Program of ; :: thesis: UsedIntLoc I = UsedIntLoc (Directed I)
consider UIL being Function of the Instructions of SCM+FSA,(Fin Int-Locations) such that
A1: for i being Instruction of SCM+FSA holds UIL . i = UsedIntLoc i and
A2: UsedIntLoc I = Union (UIL * I) by Def2;
A3: ( dom UIL = the Instructions of SCM+FSA & UIL . (halt SCM+FSA) = {} ) by A1, Th17, FUNCT_2:def 1;
consider UIL2 being Function of the Instructions of SCM+FSA,(Fin Int-Locations) such that
A4: for i being Instruction of SCM+FSA holds UIL2 . i = UsedIntLoc i and
A5: UsedIntLoc (Directed I) = Union (UIL2 * (Directed I)) by Def2;
A6: for c being Element of the Instructions of SCM+FSA holds UIL . c = UIL2 . c

proof

let c be Element of the Instructions of SCM+FSA; :: thesis: UIL . c = UIL2 . c
reconsider d = c as Instruction of SCM+FSA ;
thus UIL . c = UsedIntLoc d by A1
.= UIL2 . c by A4 ; :: thesis: verum

end;

A7: UIL . (goto (card I)) = UsedIntLoc (goto (card I)) by A1
.= {} by Th19 ;
rng I c= the Instructions of SCM+FSA by RELAT_1:def 19;
then UIL * (Directed I) = UIL * (((id the Instructions of SCM+FSA) +* ((halt SCM+FSA),(goto (card I)))) * I) by FUNCT_7:116
.= (UIL * ((id the Instructions of SCM+FSA) +* ((halt SCM+FSA),(goto (card I))))) * I by RELAT_1:36
.= UIL * I by A3, A7, FUNCT_7:108 ;
hence UsedIntLoc I = UsedIntLoc (Directed I) by A2, A5, A6, FUNCT_2:63; :: thesis: verum