let I be Program of ; :: thesis: for l being Element of NAT holds UsedInt*Loc (Directed (I,l)) = UsedInt*Loc I
let l be Element of NAT ; :: thesis: UsedInt*Loc (Directed (I,l)) = UsedInt*Loc I
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 and
A2: UsedInt*Loc I = Union (UIL * I) by SF_MASTR:def 4;
consider UIL2 being Function of the Instructions of SCM+FSA,(Fin FinSeq-Locations) such that
A3: for i being Instruction of SCM+FSA holds UIL2 . i = UsedInt*Loc i and
A4: UsedInt*Loc (Directed (I,l)) = Union (UIL2 * (Directed (I,l))) by SF_MASTR:def 4;
A5: 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 = UsedInt*Loc d by A1
.= UIL2 . c by A3 ; :: thesis: verum

end;

A6: dom UIL = the Instructions of SCM+FSA by FUNCT_2:def 1;
A7: UIL . (halt SCM+FSA) = UsedInt*Loc (halt SCM+FSA) by A1
.= {} by SF_MASTR:32 ;
A8: UIL . (goto l) = UsedInt*Loc (goto l) by A1
.= {} by SF_MASTR:32 ;
A9: rng I c= the Instructions of SCM+FSA by RELAT_1:def 19;
UIL * (Directed (I,l)) = UIL * (I +~ ((halt SCM+FSA),(goto l))) by SCMFSA6A:def 1
.= UIL * (((id the Instructions of SCM+FSA) +* ((halt SCM+FSA),(goto l))) * I) by A9, FUNCT_7:116
.= (UIL * ((id the Instructions of SCM+FSA) +* ((halt SCM+FSA),(goto l)))) * I by RELAT_1:36
.= UIL * I by A6, A7, A8, FUNCT_7:108 ;
hence UsedInt*Loc (Directed (I,l)) = UsedInt*Loc I by A2, A4, A5, FUNCT_2:63; :: thesis: verum