theorem :: COMPOS_1:47

for n being Nat
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))