let k, m be Nat; :: thesis: for S being non empty standard-ins homogeneous J/A-independent set
for I being Element of S holds IncAddr ((IncAddr (I,k)),m) = IncAddr (I,(k + m))
let S be non empty standard-ins homogeneous J/A-independent set ; :: thesis: for I being Element of S holds IncAddr ((IncAddr (I,k)),m) = IncAddr (I,(k + m))
let I be Element of S; :: thesis: IncAddr ((IncAddr (I,k)),m) = IncAddr (I,(k + m))
A1: InsCode (IncAddr ((IncAddr (I,k)),m)) = InsCode (IncAddr (I,k)) by Def8
.= InsCode I by Def8
.= InsCode (IncAddr (I,(k + m))) by Def8 ;
A2: AddressPart (IncAddr ((IncAddr (I,k)),m)) = AddressPart (IncAddr (I,k)) by Def8
.= AddressPart I by Def8
.= AddressPart (IncAddr (I,(k + m))) by Def8 ;
A3: JumpPart (IncAddr ((IncAddr (I,k)),m)) = m + (JumpPart (IncAddr (I,k))) by Def8;
A4: JumpPart (IncAddr (I,k)) = k + (JumpPart I) by Def8;
A5: JumpPart (IncAddr (I,(k + m))) = (k + m) + (JumpPart I) by Def8;
then A6: dom (JumpPart (IncAddr (I,(k + m)))) = dom (JumpPart I) by VALUED_1:def 2
.= dom (JumpPart (IncAddr (I,k))) by A4, VALUED_1:def 2
.= dom (JumpPart (IncAddr ((IncAddr (I,k)),m))) by A3, VALUED_1:def 2 ;
for n being object st n in dom (JumpPart (IncAddr ((IncAddr (I,k)),m))) holds
(JumpPart (IncAddr ((IncAddr (I,k)),m))) . n = (JumpPart (IncAddr (I,(k + m)))) . n

proof

let n be object ; :: thesis: ( n in dom (JumpPart (IncAddr ((IncAddr (I,k)),m))) implies (JumpPart (IncAddr ((IncAddr (I,k)),m))) . n = (JumpPart (IncAddr (I,(k + m)))) . n )
assume A7: n in dom (JumpPart (IncAddr ((IncAddr (I,k)),m))) ; :: thesis: (JumpPart (IncAddr ((IncAddr (I,k)),m))) . n = (JumpPart (IncAddr (I,(k + m)))) . n
then A8: n in dom (JumpPart (IncAddr (I,k))) by A3, VALUED_1:def 2;
then A9: n in dom (JumpPart I) by A4, VALUED_1:def 2;
A10: (JumpPart (IncAddr (I,k))) . n = k + ((JumpPart I) . n) by A4, A8, VALUED_1:def 2;
A11: (JumpPart (IncAddr ((IncAddr (I,k)),m))) . n = m + ((JumpPart (IncAddr (I,k))) . n) by A7, A3, VALUED_1:def 2;
n in dom (JumpPart (IncAddr (I,(k + m)))) by A5, A9, VALUED_1:def 2;
then (JumpPart (IncAddr (I,(k + m)))) . n = (k + m) + ((JumpPart I) . n) by A5, VALUED_1:def 2;
hence (JumpPart (IncAddr ((IncAddr (I,k)),m))) . n = (JumpPart (IncAddr (I,(k + m)))) . n by A11, A10; :: thesis: verum

end;

then JumpPart (IncAddr ((IncAddr (I,k)),m)) = JumpPart (IncAddr (I,(k + m))) by A6;
hence IncAddr ((IncAddr (I,k)),m) = IncAddr (I,(k + m)) by A1, A2, Th1; :: thesis: verum