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 COMPOS_1:def 40;

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, COMPOS_1:def 40 ; :: 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, COMPOS_1:def 40 ; :: thesis: verum

end;

end;

end;

dom (IncAddr (I,n)) = dom I by COMPOS_1:def 40;
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, COMPOS_1:def 40; :: thesis: verum