let a be Int-Location ; :: thesis: for I being Program of SCM+FSA holds UsedIntLoc (if=0 a,(I ';' (Goto 0 )),(Stop SCM+FSA )) = UsedIntLoc ((if=0 a,(I ';' (Goto 0 )),(Stop SCM+FSA )) +* (((card I) + 4) .--> (goto 0 )))
let I be Program of SCM+FSA ; :: thesis: UsedIntLoc (if=0 a,(I ';' (Goto 0 )),(Stop SCM+FSA )) = UsedIntLoc ((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 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 0 )),(Stop SCM+FSA )) = Union (UIL1 * (if=0 a,(I ';' (Goto 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 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:19;
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:37;
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:46
.= dom (UIL1 * ((if=0 a,(I ';' (Goto 0 )),(Stop SCM+FSA )) +* (((card I) + 4) .--> (goto 0 )))) by A5, A8, RELAT_1:46 ;
:: 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:22
.= UIL1 . (((if=0 a,(I ';' (Goto 0 )),(Stop SCM+FSA )) +* (((card I) + 4) .--> (goto 0 ))) . x) by A11, FUNCT_4:12
.= (UIL1 * ((if=0 a,(I ';' (Goto 0 )),(Stop SCM+FSA )) +* (((card I) + 4) .--> (goto 0 )))) . x by A9, A10, FUNCT_1:22 ; :: 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:22
.= UIL1 . (goto (0 + ((card I) + 4))) by A12, Lm1
.= UsedIntLoc (goto (0 + ((card I) + 4))) by A1
.= {} by SF_MASTR:19
.= UsedIntLoc (goto 0 ) by SF_MASTR:19
.= UIL1 . (goto 0 ) by A1
.= UIL1 . ((((card I) + 4) .--> (goto 0 )) . x) by A12, FUNCOP_1:87
.= UIL1 . (((if=0 a,(I ';' (Goto 0 )),(Stop SCM+FSA )) +* (((card I) + 4) .--> (goto 0 ))) . x) by A7, A12, FUNCT_4:14
.= (UIL1 * ((if=0 a,(I ';' (Goto 0 )),(Stop SCM+FSA )) +* (((card I) + 4) .--> (goto 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 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 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 0 )),(Stop SCM+FSA )) = UsedIntLoc ((if=0 a,(I ';' (Goto 0 )),(Stop SCM+FSA )) +* (((card I) + 4) .--> (goto 0 ))) by A2, A14, A4, FUNCT_1:9; :: thesis: verum