let a be Int-Location ; :: thesis: for I being Program of SCM+FSA holds UsedIntLoc (if>0 a,(I ';' (Goto (insloc 0 ))),(Stop SCM+FSA )) = UsedIntLoc ((if>0 a,(I ';' (Goto (insloc 0 ))),(Stop SCM+FSA )) +* ((insloc ((card I) + 4)) .--> (goto (insloc 0 ))))
let I be Program of SCM+FSA ; :: thesis: UsedIntLoc (if>0 a,(I ';' (Goto (insloc 0 ))),(Stop SCM+FSA )) = UsedIntLoc ((if>0 a,(I ';' (Goto (insloc 0 ))),(Stop SCM+FSA )) +* ((insloc ((card I) + 4)) .--> (goto (insloc 0 ))))
set Lc4 = insloc ((card I) + 4);
set if0 = if>0 a,(I ';' (Goto (insloc 0 ))),(Stop SCM+FSA );
set ic4 = (insloc ((card I) + 4)) .--> (goto (insloc 0 ));
consider UIL1 being Function of the Instructions of SCM+FSA ,(Fin Int-Locations ) such that
A1: for i being Instruction of SCM+FSA holds UIL1 . i = UsedIntLoc i and
A2: UsedIntLoc (if>0 a,(I ';' (Goto (insloc 0 ))),(Stop SCM+FSA )) = Union (UIL1 * (if>0 a,(I ';' (Goto (insloc 0 ))),(Stop SCM+FSA ))) by SF_MASTR:def 2;
A3: dom UIL1 = the Instructions of SCM+FSA by FUNCT_2:def 1;

A4: now

thus dom (UIL1 * (if>0 a,(I ';' (Goto (insloc 0 ))),(Stop SCM+FSA ))) = dom (UIL1 * (if>0 a,(I ';' (Goto (insloc 0 ))),(Stop SCM+FSA ))) ; :: thesis: ( dom (UIL1 * (if>0 a,(I ';' (Goto (insloc 0 ))),(Stop SCM+FSA ))) = dom (UIL1 * ((if>0 a,(I ';' (Goto (insloc 0 ))),(Stop SCM+FSA )) +* ((insloc ((card I) + 4)) .--> (goto (insloc 0 ))))) & ( for x being set st x in dom (UIL1 * (if>0 a,(I ';' (Goto (insloc 0 ))),(Stop SCM+FSA ))) holds
(UIL1 * (if>0 a,(I ';' (Goto (insloc 0 ))),(Stop SCM+FSA ))) . b₂ = (UIL1 * ((if>0 a,(I ';' (Goto (insloc 0 ))),(Stop SCM+FSA )) +* ((insloc ((card I) + 4)) .--> (goto (insloc 0 ))))) . b₂ ) )
A5: rng ((if>0 a,(I ';' (Goto (insloc 0 ))),(Stop SCM+FSA )) +* ((insloc ((card I) + 4)) .--> (goto (insloc 0 )))) c= dom UIL1 by A3, AMI_1:118;
A6: dom ((insloc ((card I) + 4)) .--> (goto (insloc 0 ))) = {(insloc ((card I) + 4))} by FUNCOP_1:19;
then A7: insloc ((card I) + 4) in dom ((insloc ((card I) + 4)) .--> (goto (insloc 0 ))) by TARSKI:def 1;
insloc ((card I) + 4) in dom (if>0 a,(I ';' (Goto (insloc 0 ))),(Stop SCM+FSA )) by Lm4;
then ( dom ((if>0 a,(I ';' (Goto (insloc 0 ))),(Stop SCM+FSA )) +* ((insloc ((card I) + 4)) .--> (goto (insloc 0 )))) = (dom (if>0 a,(I ';' (Goto (insloc 0 ))),(Stop SCM+FSA ))) \/ (dom ((insloc ((card I) + 4)) .--> (goto (insloc 0 )))) & dom ((insloc ((card I) + 4)) .--> (goto (insloc 0 ))) c= dom (if>0 a,(I ';' (Goto (insloc 0 ))),(Stop SCM+FSA )) ) by A6, FUNCT_4:def 1, ZFMISC_1:37;
then A8: dom (if>0 a,(I ';' (Goto (insloc 0 ))),(Stop SCM+FSA )) = dom ((if>0 a,(I ';' (Goto (insloc 0 ))),(Stop SCM+FSA )) +* ((insloc ((card I) + 4)) .--> (goto (insloc 0 )))) by XBOOLE_1:12;
rng (if>0 a,(I ';' (Goto (insloc 0 ))),(Stop SCM+FSA )) c= dom UIL1 by A3, AMI_1:118;
hence A9: dom (UIL1 * (if>0 a,(I ';' (Goto (insloc 0 ))),(Stop SCM+FSA ))) = dom (if>0 a,(I ';' (Goto (insloc 0 ))),(Stop SCM+FSA )) by RELAT_1:46
.= dom (UIL1 * ((if>0 a,(I ';' (Goto (insloc 0 ))),(Stop SCM+FSA )) +* ((insloc ((card I) + 4)) .--> (goto (insloc 0 ))))) by A5, A8, RELAT_1:46 ;
:: thesis: for x being set st x in dom (UIL1 * (if>0 a,(I ';' (Goto (insloc 0 ))),(Stop SCM+FSA ))) holds
(UIL1 * (if>0 a,(I ';' (Goto (insloc 0 ))),(Stop SCM+FSA ))) . b₂ = (UIL1 * ((if>0 a,(I ';' (Goto (insloc 0 ))),(Stop SCM+FSA )) +* ((insloc ((card I) + 4)) .--> (goto (insloc 0 ))))) . b₂
let x be set ; :: thesis: ( x in dom (UIL1 * (if>0 a,(I ';' (Goto (insloc 0 ))),(Stop SCM+FSA ))) implies (UIL1 * (if>0 a,(I ';' (Goto (insloc 0 ))),(Stop SCM+FSA ))) . b₁ = (UIL1 * ((if>0 a,(I ';' (Goto (insloc 0 ))),(Stop SCM+FSA )) +* ((insloc ((card I) + 4)) .--> (goto (insloc 0 ))))) . b₁ )
assume A10: x in dom (UIL1 * (if>0 a,(I ';' (Goto (insloc 0 ))),(Stop SCM+FSA ))) ; :: thesis: (UIL1 * (if>0 a,(I ';' (Goto (insloc 0 ))),(Stop SCM+FSA ))) . b₁ = (UIL1 * ((if>0 a,(I ';' (Goto (insloc 0 ))),(Stop SCM+FSA )) +* ((insloc ((card I) + 4)) .--> (goto (insloc 0 ))))) . b₁

per cases ( x <> insloc ((card I) + 4) or x = insloc ((card I) + 4) ) ;

suppose x <> insloc ((card I) + 4) ; :: thesis: (UIL1 * (if>0 a,(I ';' (Goto (insloc 0 ))),(Stop SCM+FSA ))) . b₁ = (UIL1 * ((if>0 a,(I ';' (Goto (insloc 0 ))),(Stop SCM+FSA )) +* ((insloc ((card I) + 4)) .--> (goto (insloc 0 ))))) . b₁

then A11: not x in dom ((insloc ((card I) + 4)) .--> (goto (insloc 0 ))) by A6, TARSKI:def 1;
thus (UIL1 * (if>0 a,(I ';' (Goto (insloc 0 ))),(Stop SCM+FSA ))) . x = UIL1 . ((if>0 a,(I ';' (Goto (insloc 0 ))),(Stop SCM+FSA )) . x) by A10, FUNCT_1:22
.= UIL1 . (((if>0 a,(I ';' (Goto (insloc 0 ))),(Stop SCM+FSA )) +* ((insloc ((card I) + 4)) .--> (goto (insloc 0 )))) . x) by A11, FUNCT_4:12
.= (UIL1 * ((if>0 a,(I ';' (Goto (insloc 0 ))),(Stop SCM+FSA )) +* ((insloc ((card I) + 4)) .--> (goto (insloc 0 ))))) . x by A9, A10, FUNCT_1:22 ; :: thesis: verum

end;

suppose A12: x = insloc ((card I) + 4) ; :: thesis: (UIL1 * (if>0 a,(I ';' (Goto (insloc 0 ))),(Stop SCM+FSA ))) . b₁ = (UIL1 * ((if>0 a,(I ';' (Goto (insloc 0 ))),(Stop SCM+FSA )) +* ((insloc ((card I) + 4)) .--> (goto (insloc 0 ))))) . b₁

thus (UIL1 * (if>0 a,(I ';' (Goto (insloc 0 ))),(Stop SCM+FSA ))) . x = UIL1 . ((if>0 a,(I ';' (Goto (insloc 0 ))),(Stop SCM+FSA )) . x) by A10, FUNCT_1:22
.= UIL1 . (goto ((insloc 0 ) + ((card I) + 4))) by A12, Lm4
.= UsedIntLoc (goto ((insloc 0 ) + ((card I) + 4))) by A1
.= {} by SF_MASTR:19
.= UsedIntLoc (goto (insloc 0 )) by SF_MASTR:19
.= UIL1 . (goto (insloc 0 )) by A1
.= UIL1 . (((insloc ((card I) + 4)) .--> (goto (insloc 0 ))) . x) by A12, FUNCOP_1:87
.= UIL1 . (((if>0 a,(I ';' (Goto (insloc 0 ))),(Stop SCM+FSA )) +* ((insloc ((card I) + 4)) .--> (goto (insloc 0 )))) . x) by A7, A12, FUNCT_4:14
.= (UIL1 * ((if>0 a,(I ';' (Goto (insloc 0 ))),(Stop SCM+FSA )) +* ((insloc ((card I) + 4)) .--> (goto (insloc 0 ))))) . x by A9, A10, FUNCT_1:22 ; :: thesis: verum

end;

end;

end;

consider UIL2 being Function of the Instructions of SCM+FSA ,(Fin Int-Locations ) such that
A13: for i being Instruction of SCM+FSA holds UIL2 . i = UsedIntLoc i and
A14: UsedIntLoc ((if>0 a,(I ';' (Goto (insloc 0 ))),(Stop SCM+FSA )) +* ((insloc ((card I) + 4)) .--> (goto (insloc 0 )))) = Union (UIL2 * ((if>0 a,(I ';' (Goto (insloc 0 ))),(Stop SCM+FSA )) +* ((insloc ((card I) + 4)) .--> (goto (insloc 0 ))))) by SF_MASTR:def 2;
for c being Element of the Instructions of SCM+FSA holds UIL1 . c = UIL2 . c

proof

let c be Element of the Instructions of SCM+FSA ; :: thesis: UIL1 . c = UIL2 . c
reconsider d = c as Instruction of SCM+FSA ;
thus UIL1 . c = UsedIntLoc d by A1
.= UIL2 . c by A13 ; :: thesis: verum

end;

then UIL1 = UIL2 by FUNCT_2:113;
hence UsedIntLoc (if>0 a,(I ';' (Goto (insloc 0 ))),(Stop SCM+FSA )) = UsedIntLoc ((if>0 a,(I ';' (Goto (insloc 0 ))),(Stop SCM+FSA )) +* ((insloc ((card I) + 4)) .--> (goto (insloc 0 )))) by A2, A14, A4, FUNCT_1:9; :: thesis: verum