let aa, bb be Int-Location ; :: thesis: for I, J being Program of SCM+FSA holds UsedIntLoc (if>0 aa,bb,I,J) = ({aa,bb} \/ (UsedIntLoc I)) \/ (UsedIntLoc J)
let I, J be Program of SCM+FSA ; :: thesis: UsedIntLoc (if>0 aa,bb,I,J) = ({aa,bb} \/ (UsedIntLoc I)) \/ (UsedIntLoc J)
set a = aa;
thus UsedIntLoc (if>0 aa,bb,I,J) = UsedIntLoc ((SubFrom aa,bb) ';' (if>0 aa,I,J)) by SCMFSA8B:def 5
.= (UsedIntLoc (SubFrom aa,bb)) \/ (UsedIntLoc (if>0 aa,I,J)) by SF_MASTR:33
.= {aa,bb} \/ (UsedIntLoc (if>0 aa,I,J)) by SF_MASTR:18
.= {aa,bb} \/ (({aa} \/ (UsedIntLoc I)) \/ (UsedIntLoc J)) by SCMFSA9A:15
.= {aa,bb} \/ ({aa} \/ ((UsedIntLoc I) \/ (UsedIntLoc J))) by XBOOLE_1:4
.= ({aa,bb} \/ {aa}) \/ ((UsedIntLoc I) \/ (UsedIntLoc J)) by XBOOLE_1:4
.= {aa,bb} \/ ((UsedIntLoc I) \/ (UsedIntLoc J)) by ZFMISC_1:14
.= ({aa,bb} \/ (UsedIntLoc I)) \/ (UsedIntLoc J) by XBOOLE_1:4 ; :: thesis: verum