let I be Program of SCM+FSA ; :: thesis: for l being Instruction-Location of SCM+FSA holds UsedIntLoc (Directed I,l) = UsedIntLoc I
let l be Instruction-Location of SCM+FSA ; :: thesis: UsedIntLoc (Directed I,l) = UsedIntLoc 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 ) & UsedIntLoc I = Union (UIL * I) ) by SF_MASTR:def 2;
consider UIL2 being Function of the Instructions of SCM+FSA ,(Fin Int-Locations ) such that
A2: ( ( for i being Instruction of SCM+FSA holds UIL2 . i = UsedIntLoc i ) & UsedIntLoc (Directed I,l) = Union (UIL2 * (Directed I,l)) ) by SF_MASTR:def 2;
A3: 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 A2 ; :: thesis: verum

end;

A4: dom UIL = the Instructions of SCM+FSA by FUNCT_2:def 1;
A6: UIL . (halt SCM+FSA ) = {} by A1, SF_MASTR:17;
A7: UIL . (goto l) = UsedIntLoc (goto l) by A1
.= {} by SF_MASTR:19 ;
rng I c= the Instructions of SCM+FSA by AMI_1:118;
then UIL * (Directed I,l) = UIL * (((id the Instructions of SCM+FSA ) +* (halt SCM+FSA ),(goto l)) * I) by FUNCT_7:118
.= (UIL * ((id the Instructions of SCM+FSA ) +* (halt SCM+FSA ),(goto l))) * I by RELAT_1:55
.= UIL * I by A4, A6, A7, FUNCT_7:110 ;
hence UsedIntLoc (Directed I,l) = UsedIntLoc I by A1, A2, A3, FUNCT_2:113; :: thesis: verum