let n be Element of NAT ; :: thesis: for I, J being NAT -defined the Instructions of SCM+FSA -valued finite Function holds IncAddr (I +* J),n = (IncAddr I,n) +* (IncAddr J,n)
let I, J be NAT -defined the Instructions of SCM+FSA -valued finite Function; :: thesis: IncAddr (I +* J),n = (IncAddr I,n) +* (IncAddr J,n)
A1: dom (IncAddr J,n) = dom J by AMISTD_2:def 15;

A2: now

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

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

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

A5: (I +* J) /. m = (I +* J) . m by A3, PARTFUN1:def 8
.= J . m by A4, FUNCT_4:14
.= J /. m by A4, PARTFUN1:def 8 ;
thus ((IncAddr I,n) +* (IncAddr J,n)) . m = (IncAddr J,n) . m by A1, A4, FUNCT_4:14
.= IncAddr ((I +* J) /. m),n by A4, A5, AMISTD_2:def 15 ; :: thesis: verum

end;

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

m in (dom I) \/ (dom J) by A3, FUNCT_4:def 1;
then A7: m in dom I by A6, XBOOLE_0:def 3;
A8: (I +* J) /. m = (I +* J) . m by A3, PARTFUN1:def 8
.= I . m by A6, FUNCT_4:12
.= I /. m by A7, PARTFUN1:def 8 ;
thus ((IncAddr I,n) +* (IncAddr J,n)) . m = (IncAddr I,n) . m by A1, A6, FUNCT_4:12
.= IncAddr ((I +* J) /. m),n by A7, A8, AMISTD_2:def 15 ; :: thesis: verum

end;

end;

end;

dom (IncAddr I,n) = dom I by AMISTD_2:def 15;
then dom ((IncAddr I,n) +* (IncAddr J,n)) = (dom I) \/ (dom J) by A1, FUNCT_4:def 1
.= dom (I +* J) by FUNCT_4:def 1 ;
hence IncAddr (I +* J),n = (IncAddr I,n) +* (IncAddr J,n) by A2, AMISTD_2:def 15; :: thesis: verum