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 3;
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 and
A3: UsedInt*Loc p = Union (UIL * p) by Def4;
A4: UsedInt*Loc 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
.= UsedInt*Loc i by A2 ;
hence UsedInt*Loc i c= UsedInt*Loc p by A5, A4, ZFMISC_1:74; :: thesis: verum