let i be Instruction of SCM+FSA; :: thesis: for p being preProgram of SCM+FSA st i in rng p holds
UsedIntLoc i c= UsedIntLoc p
let p be preProgram of SCM+FSA; :: thesis: ( i in rng p implies UsedIntLoc i c= UsedIntLoc p )
assume i in rng p ; :: thesis: UsedIntLoc i c= UsedIntLoc p
then consider x being set such that
A1: ( x in dom p & i = p . x ) by FUNCT_1:def 3;
consider UIL being Function of the Instructions of SCM+FSA,(Fin Int-Locations) such that
A2: for i being Instruction of SCM+FSA holds UIL . i = UsedIntLoc i and
A3: UsedIntLoc p = Union (UIL * p) by Def2;
A4: UsedIntLoc p = union (rng (UIL * p)) by A3, CARD_3:def 4;
dom UIL = the Instructions of SCM+FSA by FUNCT_2:def 1;
then x in dom (UIL * p) by A1, FUNCT_1:11;
then A5: (UIL * p) . x in rng (UIL * p) by FUNCT_1:def 3;
(UIL * p) . x = UIL . i by A1, FUNCT_1:13
.= UsedIntLoc i by A2 ;
hence UsedIntLoc i c= UsedIntLoc p by A5, A4, ZFMISC_1:74; :: thesis: verum