let n be Element of NAT ; :: thesis: for I, J being preProgram of SCM+FSA holds IncAddr (I +* J),n = (IncAddr I,n) +* (IncAddr J,n)
let I, J be preProgram of SCM+FSA ; :: 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: ( m in dom (I +* J) implies ((IncAddr I,n) +* (IncAddr J,n)) . b₁ = IncAddr (pi (I +* J),b₁),n )
assume A3: m in dom (I +* J) ; :: thesis: ((IncAddr I,n) +* (IncAddr J,n)) . b₁ = IncAddr (pi (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 (pi (I +* J),b₁),n

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

end;

suppose A6: not m in dom J ; :: thesis: ((IncAddr I,n) +* (IncAddr J,n)) . b₁ = IncAddr (pi (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: pi (I +* J),m = (I +* J) . m by A3, AMI_1:def 47
.= I . m by A6, FUNCT_4:12
.= pi I,m by A7, AMI_1:def 47 ;
thus ((IncAddr I,n) +* (IncAddr J,n)) . m = (IncAddr I,n) . 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