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

A2: now

let l be Element of NAT ; :: thesis: ( l in dom I implies (IncAddr (IncAddr I,m),n) . l = IncAddr (pi I,l),(m + n) )
assume A3: l in dom I ; :: thesis: (IncAddr (IncAddr I,m),n) . l = IncAddr (pi I,l),(m + n)
then pi (IncAddr I,m),l = (IncAddr I,m) . l by A1, AMI_1:def 47
.= IncAddr (pi I,l),m by A3, Th24 ;
hence (IncAddr (IncAddr I,m),n) . l = IncAddr (IncAddr (pi I,l),m),n by A1, A3, Th24
.= IncAddr (pi I,l),(m + n) by Th23 ;
:: thesis: verum

end;

dom (IncAddr (IncAddr I,m),n) = dom (IncAddr I,m) by Def6;
hence IncAddr (IncAddr I,m),n = IncAddr I,(m + n) by A1, A2, Def6; :: thesis: verum