let i1, k be Nat; :: thesis: IncAddr ((goto i1),k) = goto (i1 + k)
A1: InsCode (IncAddr ((goto i1),k)) = InsCode (goto i1) by COMPOS_0:def 9
.= 6
.= InsCode (goto (i1 + k)) ;
A2: AddressPart (IncAddr ((goto i1),k)) = AddressPart (goto i1) by COMPOS_0:def 9
.= {}
.= AddressPart (goto (i1 + k)) ;
A3: JumpPart (IncAddr ((goto i1),k)) = k + (JumpPart (goto i1)) by COMPOS_0:def 9;
then A4: dom (JumpPart (IncAddr ((goto i1),k))) = dom (JumpPart (goto i1)) by VALUED_1:def 2;
A5: for x being object st x in dom (JumpPart (goto i1)) holds
(JumpPart (IncAddr ((goto i1),k))) . x = (JumpPart (goto (i1 + k))) . x

proof

let x be object ; :: thesis: ( x in dom (JumpPart (goto i1)) implies (JumpPart (IncAddr ((goto i1),k))) . x = (JumpPart (goto (i1 + k))) . x )
assume A6: x in dom (JumpPart (goto i1)) ; :: thesis: (JumpPart (IncAddr ((goto i1),k))) . x = (JumpPart (goto (i1 + k))) . x
then x in dom <*i1*> ;
then A7: x = 1 by FINSEQ_1:90;
set f = (JumpPart (goto i1)) . x;
A8: (JumpPart (IncAddr ((goto i1),k))) . x = k + ((JumpPart (goto i1)) . x) by A4, A3, A6, VALUED_1:def 2;
thus (JumpPart (IncAddr ((goto i1),k))) . x = <*(i1 + k)*> . x by A7, A8
.= (JumpPart (goto (i1 + k))) . x ; :: thesis: verum

end;

dom (JumpPart (goto (i1 + k))) = dom <*(i1 + k)*>
.= Seg 1 by FINSEQ_1:def 8
.= dom <*i1*> by FINSEQ_1:def 8
.= dom (JumpPart (goto i1)) ;
then JumpPart (IncAddr ((goto i1),k)) = JumpPart (goto (i1 + k)) by A4, A5, FUNCT_1:2;
hence IncAddr ((goto i1),k) = goto (i1 + k) by A1, A2, COMPOS_0:1; :: thesis: verum