let n be Element of NAT ; :: thesis: for i being Instruction of SCM+FSA
for f being Function of the Instructions of SCM+FSA ,the Instructions of SCM+FSA st f = (id the Instructions of SCM+FSA ) +* ((halt SCM+FSA ) .--> i) holds
for s being NAT -defined the Instructions of SCM+FSA -valued finite Function holds IncAddr (f * s),n = ((id the Instructions of SCM+FSA ) +* ((halt SCM+FSA ) .--> (IncAddr i,n))) * (IncAddr s,n)
let i be Instruction of SCM+FSA ; :: thesis: for f being Function of the Instructions of SCM+FSA ,the Instructions of SCM+FSA st f = (id the Instructions of SCM+FSA ) +* ((halt SCM+FSA ) .--> i) holds
for s being NAT -defined the Instructions of SCM+FSA -valued finite Function holds IncAddr (f * s),n = ((id the Instructions of SCM+FSA ) +* ((halt SCM+FSA ) .--> (IncAddr i,n))) * (IncAddr s,n)
A1: dom (id the Instructions of SCM+FSA ) = the Instructions of SCM+FSA by RELAT_1:71;
let f be Function of the Instructions of SCM+FSA ,the Instructions of SCM+FSA ; :: thesis: ( f = (id the Instructions of SCM+FSA ) +* ((halt SCM+FSA ) .--> i) implies for s being NAT -defined the Instructions of SCM+FSA -valued finite Function holds IncAddr (f * s),n = ((id the Instructions of SCM+FSA ) +* ((halt SCM+FSA ) .--> (IncAddr i,n))) * (IncAddr s,n) )
assume A2: f = (id the Instructions of SCM+FSA ) +* ((halt SCM+FSA ) .--> i) ; :: thesis: for s being NAT -defined the Instructions of SCM+FSA -valued finite Function holds IncAddr (f * s),n = ((id the Instructions of SCM+FSA ) +* ((halt SCM+FSA ) .--> (IncAddr i,n))) * (IncAddr s,n)
let s be NAT -defined the Instructions of SCM+FSA -valued finite Function; :: thesis: IncAddr (f * s),n = ((id the Instructions of SCM+FSA ) +* ((halt SCM+FSA ) .--> (IncAddr i,n))) * (IncAddr s,n)
rng ((halt SCM+FSA ) .--> (IncAddr i,n)) = {(IncAddr i,n)} by FUNCOP_1:14;
then A3: rng ((id the Instructions of SCM+FSA ) +* ((halt SCM+FSA ) .--> (IncAddr i,n))) c= (rng (id the Instructions of SCM+FSA )) \/ {(IncAddr i,n)} by FUNCT_4:18;
rng (id the Instructions of SCM+FSA ) = the Instructions of SCM+FSA by RELAT_1:71;
then A4: (rng (id the Instructions of SCM+FSA )) \/ {(IncAddr i,n)} = the Instructions of SCM+FSA by ZFMISC_1:46;
A5: dom ((halt SCM+FSA ) .--> (IncAddr i,n)) = {(halt SCM+FSA )} by FUNCOP_1:19;
then dom ((id the Instructions of SCM+FSA ) +* ((halt SCM+FSA ) .--> (IncAddr i,n))) = (dom (id the Instructions of SCM+FSA )) \/ {(halt SCM+FSA )} by FUNCT_4:def 1
.= the Instructions of SCM+FSA by A1, ZFMISC_1:46 ;
then reconsider g = (id the Instructions of SCM+FSA ) +* ((halt SCM+FSA ) .--> (IncAddr i,n)) as Function of the Instructions of SCM+FSA ,the Instructions of SCM+FSA by A3, A4, FUNCT_2:def 1, RELSET_1:11;
A6: dom (IncAddr s,n) = dom s by AMISTD_2:def 15
.= dom (f * s) by FUNCT_2:200 ;
A7: dom ((halt SCM+FSA ) .--> i) = {(halt SCM+FSA )} by FUNCOP_1:19;

A8: now

let m be Nat; :: thesis: ( m in dom (f * s) implies (g * (IncAddr s,n)) . b₁ = IncAddr ((f * s) /. b₁),n )
assume A9: m in dom (f * s) ; :: thesis: (g * (IncAddr s,n)) . b₁ = IncAddr ((f * s) /. b₁),n
then A10: m in dom s by FUNCT_2:200;

per cases ( s . m = halt SCM+FSA or s . m <> halt SCM+FSA ) ;

suppose A11: s . m = halt SCM+FSA ; :: thesis: (g * (IncAddr s,n)) . b₁ = IncAddr ((f * s) /. b₁),n

reconsider mm = m as Element of NAT by ORDINAL1:def 13;
A12: (IncAddr s,n) . m = IncAddr (s /. mm),n by A10, Th24
.= IncAddr (halt SCM+FSA ),n by A10, A11, PARTFUN1:def 8
.= halt SCM+FSA by Th8 ;
A13: halt SCM+FSA in {(halt SCM+FSA )} by TARSKI:def 1;
A14: (f * s) /. m = (f * s) . m by A9, PARTFUN1:def 8
.= f . (halt SCM+FSA ) by A10, A11, FUNCT_1:23
.= ((halt SCM+FSA ) .--> i) . (halt SCM+FSA ) by A2, A7, A13, FUNCT_4:14
.= i by FUNCOP_1:87 ;
thus (g * (IncAddr s,n)) . m = g . ((IncAddr s,n) . m) by A6, A9, FUNCT_1:23
.= ((halt SCM+FSA ) .--> (IncAddr i,n)) . ((IncAddr s,n) . m) by A5, A12, A13, FUNCT_4:14
.= IncAddr ((f * s) /. m),n by A12, A14, FUNCOP_1:87 ; :: thesis: verum

end;

suppose A15: s . m <> halt SCM+FSA ; :: thesis: (g * (IncAddr s,n)) . b₁ = IncAddr ((f * s) /. b₁),n

A16: InsCode (IncAddr (s /. m),n) = InsCode (s /. m) by Th22;
A17: s /. m = s . m by A10, PARTFUN1:def 8;
then A18: not s /. m in {(halt SCM+FSA )} by A15, TARSKI:def 1;
InsCode (s /. m) <> 0 by A15, A17, SCMFSA_2:122;
then A19: not IncAddr (s /. m),n in {(halt SCM+FSA )} by A16, SCMFSA_2:124, TARSKI:def 1;
A20: (f * s) /. m = (f * s) . m by A9, PARTFUN1:def 8
.= f . (s . m) by A10, FUNCT_1:23
.= (id the Instructions of SCM+FSA ) . (s /. m) by A2, A7, A17, A18, FUNCT_4:12
.= s /. m by FUNCT_1:35 ;
thus (g * (IncAddr s,n)) . m = g . ((IncAddr s,n) . m) by A6, A9, FUNCT_1:23
.= g . (IncAddr (s /. m),n) by A10, AMISTD_2:def 15
.= (id the Instructions of SCM+FSA ) . (IncAddr (s /. m),n) by A5, A19, FUNCT_4:12
.= IncAddr ((f * s) /. m),n by A20, FUNCT_1:35 ; :: thesis: verum

end;

end;

end;

dom (g * (IncAddr s,n)) = dom (IncAddr s,n) by FUNCT_2:200;
hence IncAddr (f * s),n = ((id the Instructions of SCM+FSA ) +* ((halt SCM+FSA ) .--> (IncAddr i,n))) * (IncAddr s,n) by A6, A8, AMISTD_2:def 15; :: thesis: verum