let s be State of SCMPDS ; :: thesis: for l1, l2 being Element of NAT
for i1, i2 being Instruction of SCMPDS 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 SCMPDS holds s +* (l1,l2 --> i1,i2) = (s +* l1,i1) +* l2,i2
let i1, i2 be Instruction of SCMPDS ; :: thesis: s +* (l1,l2 --> i1,i2) = (s +* l1,i1) +* l2,i2
A1: l1 in dom s by Th68;
A2: l2 in dom (s +* l1,i1) by Th68;
thus s +* (l1,l2 --> i1,i2) = s +* ((l1 .--> i1) +* (l2 .--> i2)) by FUNCT_4:def 4
.= (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