let a be Int-Location ; :: thesis: for I being Program of SCM+FSA holds UsedInt*Loc (if>0 a,(I ';' (Goto (insloc 0 ))),(Stop SCM+FSA )) = UsedInt*Loc ((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: UsedInt*Loc (if>0 a,(I ';' (Goto (insloc 0 ))),(Stop SCM+FSA )) = UsedInt*Loc ((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 FinSeq-Locations ) such that
A1: for i being Instruction of SCM+FSA holds UIL1 . i = UsedInt*Loc i and
A2: UsedInt*Loc (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 4;
consider UIL2 being Function of the Instructions of SCM+FSA ,(Fin FinSeq-Locations ) such that
A3: for i being Instruction of SCM+FSA holds UIL2 . i = UsedInt*Loc i and
A4: UsedInt*Loc ((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 4;
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 = UsedInt*Loc d by A1
.= UIL2 . c by A3 ; :: thesis: verum

end;

then A5: UIL1 = UIL2 by FUNCT_2:113;
A6: dom UIL1 = the Instructions of SCM+FSA by FUNCT_2:def 1;

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₂ ) )
A7: rng (if>0 a,(I ';' (Goto (insloc 0 ))),(Stop SCM+FSA )) c= dom UIL1 by A6, AMI_1:118;
A8: rng ((if>0 a,(I ';' (Goto (insloc 0 ))),(Stop SCM+FSA )) +* ((insloc ((card I) + 4)) .--> (goto (insloc 0 )))) c= dom UIL1 by A6, AMI_1:118;
A9: 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 )))) by FUNCT_4:def 1;
A10: dom ((insloc ((card I) + 4)) .--> (goto (insloc 0 ))) = {(insloc ((card I) + 4))} by FUNCOP_1:19;
insloc ((card I) + 4) in dom (if>0 a,(I ';' (Goto (insloc 0 ))),(Stop SCM+FSA )) by Lm4;
then dom ((insloc ((card I) + 4)) .--> (goto (insloc 0 ))) c= dom (if>0 a,(I ';' (Goto (insloc 0 ))),(Stop SCM+FSA )) by A10, ZFMISC_1:37;
then A11: 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 A9, XBOOLE_1:12;
thus A12: dom (UIL1 * (if>0 a,(I ';' (Goto (insloc 0 ))),(Stop SCM+FSA ))) = dom (if>0 a,(I ';' (Goto (insloc 0 ))),(Stop SCM+FSA )) by A7, RELAT_1:46
.= dom (UIL1 * ((if>0 a,(I ';' (Goto (insloc 0 ))),(Stop SCM+FSA )) +* ((insloc ((card I) + 4)) .--> (goto (insloc 0 ))))) by A8, A11, 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 A13: 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₁
A14: insloc ((card I) + 4) in dom ((insloc ((card I) + 4)) .--> (goto (insloc 0 ))) by A10, TARSKI:def 1;

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 A15: not x in dom ((insloc ((card I) + 4)) .--> (goto (insloc 0 ))) by A10, 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 A13, FUNCT_1:22
.= UIL1 . (((if>0 a,(I ';' (Goto (insloc 0 ))),(Stop SCM+FSA )) +* ((insloc ((card I) + 4)) .--> (goto (insloc 0 )))) . x) by A15, FUNCT_4:12
.= (UIL1 * ((if>0 a,(I ';' (Goto (insloc 0 ))),(Stop SCM+FSA )) +* ((insloc ((card I) + 4)) .--> (goto (insloc 0 ))))) . x by A12, A13, FUNCT_1:22 ; :: thesis: verum

end;

suppose A16: 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 A13, FUNCT_1:22
.= UIL1 . (goto ((insloc 0 ) + ((card I) + 4))) by A16, Lm4
.= UsedInt*Loc (goto ((insloc 0 ) + ((card I) + 4))) by A1
.= {} by SF_MASTR:36
.= UsedInt*Loc (goto (insloc 0 )) by SF_MASTR:36
.= UIL1 . (goto (insloc 0 )) by A1
.= UIL1 . (((insloc ((card I) + 4)) .--> (goto (insloc 0 ))) . x) by A16, FUNCOP_1:87
.= UIL1 . (((if>0 a,(I ';' (Goto (insloc 0 ))),(Stop SCM+FSA )) +* ((insloc ((card I) + 4)) .--> (goto (insloc 0 )))) . x) by A14, A16, FUNCT_4:14
.= (UIL1 * ((if>0 a,(I ';' (Goto (insloc 0 ))),(Stop SCM+FSA )) +* ((insloc ((card I) + 4)) .--> (goto (insloc 0 ))))) . x by A12, A13, FUNCT_1:22 ; :: thesis: verum

end;

end;

end;

hence UsedInt*Loc (if>0 a,(I ';' (Goto (insloc 0 ))),(Stop SCM+FSA )) = UsedInt*Loc ((if>0 a,(I ';' (Goto (insloc 0 ))),(Stop SCM+FSA )) +* ((insloc ((card I) + 4)) .--> (goto (insloc 0 )))) by A2, A4, A5, FUNCT_1:9; :: thesis: verum