let k, loc be Nat; :: thesis: IncAddr ((SCM-goto loc),k) = SCM-goto (loc + k)
A1: InsCode (IncAddr ((SCM-goto loc),k)) = InsCode (SCM-goto loc) by COMPOS_1:def 17
.= 6 by RECDEF_2:def 1
.= InsCode (SCM-goto (loc + k)) by RECDEF_2:def 1 ;
A2: AddressPart (IncAddr ((SCM-goto loc),k)) = AddressPart (SCM-goto loc) by COMPOS_1:def 17
.= {} by RECDEF_2:def 3
.= AddressPart (SCM-goto (loc + k)) by RECDEF_2:def 3 ;
A3: JumpPart (IncAddr ((SCM-goto loc),k)) = k + (JumpPart (SCM-goto loc)) by COMPOS_1:def 17;
JumpPart (IncAddr ((SCM-goto loc),k)) = JumpPart (SCM-goto (loc + k))

proof

thus A4: dom (JumpPart (IncAddr ((SCM-goto loc),k))) = dom (JumpPart (SCM-goto (loc + k))) by A1, COMPOS_1:def 12; :: according to FUNCT_1:def 11 :: thesis: for b₁ being set holds
( not b₁ in proj1 (JumpPart (IncAddr ((SCM-goto loc),k))) or (JumpPart (IncAddr ((SCM-goto loc),k))) . b₁ = (JumpPart (SCM-goto (loc + k))) . b₁ )
A5: JumpPart (SCM-goto loc) = <*loc*> by RECDEF_2:def 2;
A6: JumpPart (SCM-goto (loc + k)) = <*(loc + k)*> by RECDEF_2:def 2;
let x be set ; :: thesis: ( not x in proj1 (JumpPart (IncAddr ((SCM-goto loc),k))) or (JumpPart (IncAddr ((SCM-goto loc),k))) . x = (JumpPart (SCM-goto (loc + k))) . x )
assume A7: x in dom (JumpPart (IncAddr ((SCM-goto loc),k))) ; :: thesis: (JumpPart (IncAddr ((SCM-goto loc),k))) . x = (JumpPart (SCM-goto (loc + k))) . x
dom <*(loc + k)*> = {1} by FINSEQ_1:2, FINSEQ_1:38;
then A8: x = 1 by A7, A4, A6, TARSKI:def 1;
thus (JumpPart (IncAddr ((SCM-goto loc),k))) . x = k + ((JumpPart (SCM-goto loc)) . x) by A3, A7, VALUED_1:def 2
.= loc + k by A5, A8, FINSEQ_1:40
.= (JumpPart (SCM-goto (loc + k))) . x by A6, A8, FINSEQ_1:40 ; :: thesis: verum

end;

hence IncAddr ((SCM-goto loc),k) = SCM-goto (loc + k) by A1, A2, COMPOS_1:1; :: thesis: verum