let n be Nat; :: thesis: for S being COM-Struct
for i being Instruction of S
for f being Function of the InstructionsF of S, the InstructionsF of S st f = (id the InstructionsF of S) +* ((halt S) .--> i) holds
for s being NAT -defined the InstructionsF of b₁ -valued finite Function holds IncAddr ((f * s),n) = ((id the InstructionsF of S) +* ((halt S) .--> (IncAddr (i,n)))) * (IncAddr (s,n))
let S be COM-Struct ; :: thesis: for i being Instruction of S
for f being Function of the InstructionsF of S, the InstructionsF of S st f = (id the InstructionsF of S) +* ((halt S) .--> i) holds
for s being NAT -defined the InstructionsF of S -valued finite Function holds IncAddr ((f * s),n) = ((id the InstructionsF of S) +* ((halt S) .--> (IncAddr (i,n)))) * (IncAddr (s,n))
let i be Instruction of S; :: thesis: for f being Function of the InstructionsF of S, the InstructionsF of S st f = (id the InstructionsF of S) +* ((halt S) .--> i) holds
for s being NAT -defined the InstructionsF of S -valued finite Function holds IncAddr ((f * s),n) = ((id the InstructionsF of S) +* ((halt S) .--> (IncAddr (i,n)))) * (IncAddr (s,n))
let f be Function of the InstructionsF of S, the InstructionsF of S; :: thesis: ( f = (id the InstructionsF of S) +* ((halt S) .--> i) implies for s being NAT -defined the InstructionsF of S -valued finite Function holds IncAddr ((f * s),n) = ((id the InstructionsF of S) +* ((halt S) .--> (IncAddr (i,n)))) * (IncAddr (s,n)) )
assume A1: f = (id the InstructionsF of S) +* ((halt S) .--> i) ; :: thesis: for s being NAT -defined the InstructionsF of S -valued finite Function holds IncAddr ((f * s),n) = ((id the InstructionsF of S) +* ((halt S) .--> (IncAddr (i,n)))) * (IncAddr (s,n))
let s be NAT -defined the InstructionsF of S -valued finite Function; :: thesis: IncAddr ((f * s),n) = ((id the InstructionsF of S) +* ((halt S) .--> (IncAddr (i,n)))) * (IncAddr (s,n))
rng ((halt S) .--> (IncAddr (i,n))) = {(IncAddr (i,n))} by FUNCOP_1:8;
then A2: rng ((id the InstructionsF of S) +* ((halt S) .--> (IncAddr (i,n)))) c= (rng (id the InstructionsF of S)) \/ {(IncAddr (i,n))} by FUNCT_4:17;
A3: (rng (id the InstructionsF of S)) \/ {(IncAddr (i,n))} = the InstructionsF of S by ZFMISC_1:40;
A4: dom ((halt S) .--> (IncAddr (i,n))) = {(halt S)} ;
then dom ((id the InstructionsF of S) +* ((halt S) .--> (IncAddr (i,n)))) = (dom (id the InstructionsF of S)) \/ {(halt S)} by FUNCT_4:def 1
.= the InstructionsF of S by ZFMISC_1:40 ;
then reconsider g = (id the InstructionsF of S) +* ((halt S) .--> (IncAddr (i,n))) as Function of the InstructionsF of S, the InstructionsF of S by A2, A3, RELSET_1:4;
A5: dom (IncAddr (s,n)) = dom s by Def9
.= dom (f * s) by FUNCT_2:123 ;
A6: dom ((halt S) .--> i) = {(halt S)} ;

A7: now :: thesis: for m being Nat st m in dom (f * s) holds
(g * (IncAddr (s,n))) . m = IncAddr (((f * s) /. m),n)

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

per cases ( s . m = halt S or s . m <> halt S ) ;

suppose A10: s . m = halt S ; :: thesis: (g * (IncAddr (s,n))) . b₁ = IncAddr (((f * s) /. b₁),n)

reconsider mm = m as Element of NAT by ORDINAL1:def 12;
A11: (IncAddr (s,n)) . m = IncAddr ((s /. mm),n) by A9, Def9
.= IncAddr ((halt S),n) by A9, A10, PARTFUN1:def 6
.= halt S by COMPOS_0:4 ;
A12: halt S in {(halt S)} by TARSKI:def 1;
A13: (f * s) /. m = (f * s) . m by A8, PARTFUN1:def 6
.= f . (halt S) by A9, A10, FUNCT_1:13
.= ((halt S) .--> i) . (halt S) by A1, A6, A12, FUNCT_4:13
.= i by FUNCOP_1:72 ;
thus (g * (IncAddr (s,n))) . m = g . ((IncAddr (s,n)) . m) by A5, A8, FUNCT_1:13
.= ((halt S) .--> (IncAddr (i,n))) . ((IncAddr (s,n)) . m) by A4, A11, A12, FUNCT_4:13
.= IncAddr (((f * s) /. m),n) by A11, A13, FUNCOP_1:72 ; :: thesis: verum

end;

suppose A14: s . m <> halt S ; :: thesis: (g * (IncAddr (s,n))) . b₁ = IncAddr (((f * s) /. b₁),n)

A15: s /. m = s . m by A9, PARTFUN1:def 6;
A16: not IncAddr ((s /. m),n) = halt S by A14, A15, COMPOS_0:12;
A17: not s /. m in {(halt S)} by A14, A15, TARSKI:def 1;
A18: not IncAddr ((s /. m),n) in {(halt S)} by A16, TARSKI:def 1;
A19: (f * s) /. m = (f * s) . m by A8, PARTFUN1:def 6
.= f . (s . m) by A9, FUNCT_1:13
.= (id the InstructionsF of S) . (s /. m) by A1, A6, A15, A17, FUNCT_4:11
.= s /. m ;
thus (g * (IncAddr (s,n))) . m = g . ((IncAddr (s,n)) . m) by A5, A8, FUNCT_1:13
.= g . (IncAddr ((s /. m),n)) by A9, Def9
.= (id the InstructionsF of S) . (IncAddr ((s /. m),n)) by A4, A18, FUNCT_4:11
.= IncAddr (((f * s) /. m),n) by A19 ; :: thesis: verum

end;

end;

end;

dom (g * (IncAddr (s,n))) = dom (IncAddr (s,n)) by FUNCT_2:123;
hence IncAddr ((f * s),n) = ((id the InstructionsF of S) +* ((halt S) .--> (IncAddr (i,n)))) * (IncAddr (s,n)) by A5, A7, Def9; :: thesis: verum