let m, n be Element of NAT ; :: thesis: for I being NAT -defined the Instructions of SCM+FSA -valued finite Function holds IncAddr (IncAddr I,m),n = IncAddr I,(m + n)
let I be NAT -defined the Instructions of SCM+FSA -valued finite Function; :: 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 (I /. l),(m + n) )
assume A3: l in dom I ; :: thesis: (IncAddr (IncAddr I,m),n) . l = IncAddr (I /. l),(m + n)
then (IncAddr I,m) /. l = (IncAddr I,m) . l by A1, PARTFUN1:def 8
.= IncAddr (I /. l),m by A3, Th24 ;
hence (IncAddr (IncAddr I,m),n) . l = IncAddr (IncAddr (I /. l),m),n by A1, A3, Th24
.= IncAddr (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