let i be Instruction of SCM+FSA ; :: thesis: for p being preProgram of SCM+FSA st i in rng p holds
UsedInt*Loc i c= UsedInt*Loc p
let p be preProgram of SCM+FSA ; :: thesis: ( i in rng p implies UsedInt*Loc i c= UsedInt*Loc p )
assume i in rng p ; :: thesis: UsedInt*Loc i c= UsedInt*Loc p
then consider x being set such that
A1: ( x in dom p & i = p . x ) by FUNCT_1:def 5;
consider UIL being Function of the Instructions of SCM+FSA ,(Fin FinSeq-Locations ) such that
A2: ( ( for i being Instruction of SCM+FSA holds UIL . i = UsedInt*Loc i ) & UsedInt*Loc p = Union (UIL * p) ) by Def4;
A3: (UIL * p) . x = UIL . i by A1, FUNCT_1:23
.= UsedInt*Loc i by A2 ;
dom UIL = the Instructions of SCM+FSA by FUNCT_2:def 1;
then x in dom (UIL * p) by A1, FUNCT_1:21;
then A4: (UIL * p) . x in rng (UIL * p) by FUNCT_1:def 5;
UsedInt*Loc p = union (rng (UIL * p)) by A2, CARD_3:def 4;
hence UsedInt*Loc i c= UsedInt*Loc p by A3, A4, ZFMISC_1:92; :: thesis: verum