let n be Nat; :: thesis: for S being COM-Struct
for p, q being NAT -defined the InstructionsF of b₁ -valued finite Function holds IncAddr ((p +* q),n) = (IncAddr (p,n)) +* (IncAddr (q,n))
let S be COM-Struct ; :: thesis: for p, q being NAT -defined the InstructionsF of S -valued finite Function holds IncAddr ((p +* q),n) = (IncAddr (p,n)) +* (IncAddr (q,n))
let p, q be NAT -defined the InstructionsF of S -valued finite Function; :: thesis: IncAddr ((p +* q),n) = (IncAddr (p,n)) +* (IncAddr (q,n))
A1: dom (IncAddr (q,n)) = dom q by Def9;

A2: now :: thesis: for m being Nat st m in dom (p +* q) holds
((IncAddr (p,n)) +* (IncAddr (q,n))) . m = IncAddr (((p +* q) /. m),n)

let m be Nat; :: thesis: ( m in dom (p +* q) implies ((IncAddr (p,n)) +* (IncAddr (q,n))) . b₁ = IncAddr (((p +* q) /. b₁),n) )
assume A3: m in dom (p +* q) ; :: thesis: ((IncAddr (p,n)) +* (IncAddr (q,n))) . b₁ = IncAddr (((p +* q) /. b₁),n)

per cases ( m in dom q or not m in dom q ) ;

suppose A4: m in dom q ; :: thesis: ((IncAddr (p,n)) +* (IncAddr (q,n))) . b₁ = IncAddr (((p +* q) /. b₁),n)

A5: (p +* q) /. m = (p +* q) . m by A3, PARTFUN1:def 6
.= q . m by A4, FUNCT_4:13
.= q /. m by A4, PARTFUN1:def 6 ;
thus ((IncAddr (p,n)) +* (IncAddr (q,n))) . m = (IncAddr (q,n)) . m by A1, A4, FUNCT_4:13
.= IncAddr (((p +* q) /. m),n) by A4, A5, Def9 ; :: thesis: verum

end;

suppose A6: not m in dom q ; :: thesis: ((IncAddr (p,n)) +* (IncAddr (q,n))) . b₁ = IncAddr (((p +* q) /. b₁),n)

m in (dom p) \/ (dom q) by A3, FUNCT_4:def 1;
then A7: m in dom p by A6, XBOOLE_0:def 3;
A8: (p +* q) /. m = (p +* q) . m by A3, PARTFUN1:def 6
.= p . m by A6, FUNCT_4:11
.= p /. m by A7, PARTFUN1:def 6 ;
thus ((IncAddr (p,n)) +* (IncAddr (q,n))) . m = (IncAddr (p,n)) . m by A1, A6, FUNCT_4:11
.= IncAddr (((p +* q) /. m),n) by A7, A8, Def9 ; :: thesis: verum

end;

end;

end;

dom (IncAddr (p,n)) = dom p by Def9;
then dom ((IncAddr (p,n)) +* (IncAddr (q,n))) = (dom p) \/ (dom q) by A1, FUNCT_4:def 1
.= dom (p +* q) by FUNCT_4:def 1 ;
hence IncAddr ((p +* q),n) = (IncAddr (p,n)) +* (IncAddr (q,n)) by A2, Def9; :: thesis: verum