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