let n be Element of NAT ; :: thesis: for I, J being preProgram of holds IncAddr (I +* J),n = (IncAddr I,n) +* (IncAddr J,n)
let I, J be preProgram of ; :: thesis: IncAddr (I +* J),n = (IncAddr I,n) +* (IncAddr J,n)
A1: dom (IncAddr J,n) = dom J by Def6;

A2: now

let m be Element of NAT ; :: thesis: ( insloc m in dom (I +* J) implies ((IncAddr I,n) +* (IncAddr J,n)) . (insloc b₁) = IncAddr (pi (I +* J),b₁),n )
assume A3: insloc m in dom (I +* J) ; :: thesis: ((IncAddr I,n) +* (IncAddr J,n)) . (insloc b₁) = IncAddr (pi (I +* J),b₁),n

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

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

A5: pi (I +* J),m = (I +* J) . (insloc m) by A3, AMI_1:def 47
.= J . (insloc m) by A4, FUNCT_4:14
.= pi J,m by A4, AMI_1:def 47 ;
thus ((IncAddr I,n) +* (IncAddr J,n)) . (insloc m) = (IncAddr J,n) . (insloc m) by A1, A4, FUNCT_4:14
.= IncAddr (pi (I +* J),m),n by A4, A5, Def6 ; :: thesis: verum

end;

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

insloc m in (dom I) \/ (dom J) by A3, FUNCT_4:def 1;
then A7: insloc m in dom I by A6, XBOOLE_0:def 3;
A8: pi (I +* J),m = (I +* J) . (insloc m) by A3, AMI_1:def 47
.= I . (insloc m) by A6, FUNCT_4:12
.= pi I,m by A7, AMI_1:def 47 ;
thus ((IncAddr I,n) +* (IncAddr J,n)) . (insloc m) = (IncAddr I,n) . (insloc m) by A1, A6, FUNCT_4:12
.= IncAddr (pi (I +* J),m),n by A7, A8, Def6 ; :: thesis: verum

end;

end;

end;

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