let a be Int-Location ; :: thesis: for I being Program of SCM+FSA holds UsedInt*Loc (if=0 (a,(I ';' (Goto 0)),(Stop SCM+FSA))) = UsedInt*Loc ((if=0 (a,(I ';' (Goto 0)),(Stop SCM+FSA))) +* (((card I) + 4) .--> (goto 0)))
let I be Program of SCM+FSA; :: thesis: UsedInt*Loc (if=0 (a,(I ';' (Goto 0)),(Stop SCM+FSA))) = UsedInt*Loc ((if=0 (a,(I ';' (Goto 0)),(Stop SCM+FSA))) +* (((card I) + 4) .--> (goto 0)))
set Lc4 = (card I) + 4;
set if0 = if=0 (a,(I ';' (Goto 0)),(Stop SCM+FSA));
set ic4 = ((card I) + 4) .--> (goto 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 0)),(Stop SCM+FSA))) = Union (UIL1 * (if=0 (a,(I ';' (Goto 0)),(Stop SCM+FSA)))) by SF_MASTR:def 4;
A3: dom UIL1 = the Instructions of SCM+FSA by FUNCT_2:def 1;

A4: now

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

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

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

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

end;

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

thus (UIL1 * (if=0 (a,(I ';' (Goto 0)),(Stop SCM+FSA)))) . x = UIL1 . ((if=0 (a,(I ';' (Goto 0)),(Stop SCM+FSA))) . x) by A10, FUNCT_1:12
.= UIL1 . (goto (0 + ((card I) + 4))) by A12, Lm1
.= UsedInt*Loc (goto (0 + ((card I) + 4))) by A1
.= {} by SF_MASTR:32
.= UsedInt*Loc (goto 0) by SF_MASTR:32
.= UIL1 . (goto 0) by A1
.= UIL1 . ((((card I) + 4) .--> (goto 0)) . x) by A12, FUNCOP_1:72
.= UIL1 . (((if=0 (a,(I ';' (Goto 0)),(Stop SCM+FSA))) +* (((card I) + 4) .--> (goto 0))) . x) by A7, A12, FUNCT_4:13
.= (UIL1 * ((if=0 (a,(I ';' (Goto 0)),(Stop SCM+FSA))) +* (((card I) + 4) .--> (goto 0)))) . x by A9, A10, FUNCT_1:12 ; :: thesis: verum

end;

end;

end;

consider UIL2 being Function of the Instructions of SCM+FSA,(Fin FinSeq-Locations) such that
A13: for i being Instruction of SCM+FSA holds UIL2 . i = UsedInt*Loc i and
A14: UsedInt*Loc ((if=0 (a,(I ';' (Goto 0)),(Stop SCM+FSA))) +* (((card I) + 4) .--> (goto 0))) = Union (UIL2 * ((if=0 (a,(I ';' (Goto 0)),(Stop SCM+FSA))) +* (((card I) + 4) .--> (goto 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 A13 ; :: thesis: verum

end;

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