let IT1, IT2 be Subset of Int-Locations ; :: thesis: ( ex UIL being Function of the Instructions of SCM+FSA ,(Fin Int-Locations ) st
( ( for i being Instruction of SCM+FSA holds UIL . i = UsedIntLoc i ) & IT1 = Union (UIL * p) ) & ex UIL being Function of the Instructions of SCM+FSA ,(Fin Int-Locations ) st
( ( for i being Instruction of SCM+FSA holds UIL . i = UsedIntLoc i ) & IT2 = Union (UIL * p) ) implies IT1 = IT2 )
given UIL1 being Function of the Instructions of SCM+FSA ,(Fin Int-Locations ) such that A5: ( ( for i being Instruction of SCM+FSA holds UIL1 . i = UsedIntLoc i ) & IT1 = Union (UIL1 * p) ) ; :: thesis: ( for UIL being Function of the Instructions of SCM+FSA ,(Fin Int-Locations ) holds
( ex i being Instruction of SCM+FSA st not UIL . i = UsedIntLoc i or not IT2 = Union (UIL * p) ) or IT1 = IT2 )
given UIL2 being Function of the Instructions of SCM+FSA ,(Fin Int-Locations ) such that A6: ( ( for i being Instruction of SCM+FSA holds UIL2 . i = UsedIntLoc i ) & IT2 = Union (UIL2 * p) ) ; :: thesis: IT1 = IT2
for c being Element of the Instructions of SCM+FSA holds UIL1 . c = UIL2 . c

proof

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

end;

hence IT1 = IT2 by A5, A6, FUNCT_2:113; :: thesis: verum