let N be non empty with_non-empty_elements set ; :: thesis: for S being non empty stored-program IC-Ins-separated definite realistic COM-Struct of N
for s being State of S
for l1, l2 being Element of NAT
for i1, i2 being Instruction of S holds s +* ((l1,l2) --> (i1,i2)) = (s +* (l1,i1)) +* (l2,i2)
let S be non empty stored-program IC-Ins-separated definite realistic COM-Struct of N; :: thesis: for s being State of S
for l1, l2 being Element of NAT
for i1, i2 being Instruction of S holds s +* ((l1,l2) --> (i1,i2)) = (s +* (l1,i1)) +* (l2,i2)
let s be State of S; :: thesis: for l1, l2 being Element of NAT
for i1, i2 being Instruction of S holds s +* ((l1,l2) --> (i1,i2)) = (s +* (l1,i1)) +* (l2,i2)
let l1, l2 be Element of NAT ; :: thesis: for i1, i2 being Instruction of S holds s +* ((l1,l2) --> (i1,i2)) = (s +* (l1,i1)) +* (l2,i2)
let i1, i2 be Instruction of S; :: thesis: s +* ((l1,l2) --> (i1,i2)) = (s +* (l1,i1)) +* (l2,i2)
A1: l1 in dom s by Th23;
A2: l2 in dom (s +* (l1,i1)) by Th23;
thus s +* ((l1,l2) --> (i1,i2)) = s +* ((l1 .--> i1) +* (l2 .--> i2))
.= (s +* (l1 .--> i1)) +* (l2 .--> i2) by FUNCT_4:15
.= (s +* (l1,i1)) +* (l2 .--> i2) by A1, FUNCT_7:def 3
.= (s +* (l1,i1)) +* (l2,i2) by A2, FUNCT_7:def 3 ; :: thesis: verum