let b be Int-Location; for I being MacroInstruction of SCM+FSA holds {b} \/ (UsedILoc I) c= UsedILoc (times (b,I))
let I be MacroInstruction of SCM+FSA ; {b} \/ (UsedILoc I) c= UsedILoc (times (b,I))
set a = b;
set aux = 1 -stRWNotIn ({b} \/ (UsedILoc I));
UsedILoc (times (b,I)) =
(UsedIntLoc ((1 -stRWNotIn ({b} \/ (UsedILoc I))) := b)) \/ (UsedILoc (while>0 ((1 -stRWNotIn ({b} \/ (UsedILoc I))),(I ";" (SubFrom ((1 -stRWNotIn ({b} \/ (UsedILoc I))),(intloc 0)))))))
by SF_MASTR:29
.=
{(1 -stRWNotIn ({b} \/ (UsedILoc I))),b} \/ (UsedILoc (while>0 ((1 -stRWNotIn ({b} \/ (UsedILoc I))),(I ";" (SubFrom ((1 -stRWNotIn ({b} \/ (UsedILoc I))),(intloc 0)))))))
by SF_MASTR:14
.=
{(1 -stRWNotIn ({b} \/ (UsedILoc I))),b} \/ ({(1 -stRWNotIn ({b} \/ (UsedILoc I)))} \/ (UsedILoc (I ";" (SubFrom ((1 -stRWNotIn ({b} \/ (UsedILoc I))),(intloc 0))))))
by SCMFSA9A:24
.=
({(1 -stRWNotIn ({b} \/ (UsedILoc I))),b} \/ {(1 -stRWNotIn ({b} \/ (UsedILoc I)))}) \/ (UsedILoc (I ";" (SubFrom ((1 -stRWNotIn ({b} \/ (UsedILoc I))),(intloc 0)))))
by XBOOLE_1:4
.=
{(1 -stRWNotIn ({b} \/ (UsedILoc I))),b} \/ (UsedILoc (I ";" (SubFrom ((1 -stRWNotIn ({b} \/ (UsedILoc I))),(intloc 0)))))
by ZFMISC_1:9
.=
{(1 -stRWNotIn ({b} \/ (UsedILoc I))),b} \/ ((UsedILoc I) \/ (UsedIntLoc (SubFrom ((1 -stRWNotIn ({b} \/ (UsedILoc I))),(intloc 0)))))
by SF_MASTR:30
.=
{(1 -stRWNotIn ({b} \/ (UsedILoc I))),b} \/ ((UsedILoc I) \/ {(1 -stRWNotIn ({b} \/ (UsedILoc I))),(intloc 0)})
by SF_MASTR:14
.=
({(1 -stRWNotIn ({b} \/ (UsedILoc I))),b} \/ (UsedILoc I)) \/ {(1 -stRWNotIn ({b} \/ (UsedILoc I))),(intloc 0)}
by XBOOLE_1:4
;
then A1:
{(1 -stRWNotIn ({b} \/ (UsedILoc I))),b} \/ (UsedILoc I) c= UsedILoc (times (b,I))
by XBOOLE_1:7;
UsedILoc I c= {(1 -stRWNotIn ({b} \/ (UsedILoc I))),b} \/ (UsedILoc I)
by XBOOLE_1:7;
then A2:
UsedILoc I c= UsedILoc (times (b,I))
by A1, XBOOLE_1:1;
( {b} c= {(1 -stRWNotIn ({b} \/ (UsedILoc I))),b} & {(1 -stRWNotIn ({b} \/ (UsedILoc I))),b} c= {(1 -stRWNotIn ({b} \/ (UsedILoc I))),b} \/ (UsedILoc I) )
by XBOOLE_1:7, ZFMISC_1:7;
then
{b} c= {(1 -stRWNotIn ({b} \/ (UsedILoc I))),b} \/ (UsedILoc I)
by XBOOLE_1:1;
then
{b} c= UsedILoc (times (b,I))
by A1, XBOOLE_1:1;
hence
{b} \/ (UsedILoc I) c= UsedILoc (times (b,I))
by A2, XBOOLE_1:8; verum