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 A3: for i being Instruction of SCM+FSA holds UIL1 . i = UsedIntLoc i and
A4: 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 A5: for i being Instruction of SCM+FSA holds UIL2 . i = UsedIntLoc i and
A6: 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 A3
.= UIL2 . c by A5 ; :: thesis: verum

end;

hence IT1 = IT2 by A4, A6, FUNCT_2:63; :: thesis: verum