let i, j be Nat; :: thesis: IncAddr ((Goto i),j) = <%(goto (i + j))%>
A1: dom <%(goto (i + j))%> = Segm 1 by AFINSQ_1:33
.= dom (Goto i) by AFINSQ_1:33 ;
for m being Nat st m in dom (Goto i) holds
<%(goto (i + j))%> . m = IncAddr (((Goto i) /. m),j)
proof
let m be Nat; :: thesis: ( m in dom (Goto i) implies <%(goto (i + j))%> . m = IncAddr (((Goto i) /. m),j) )
assume A2: m in dom (Goto i) ; :: thesis: <%(goto (i + j))%> . m = IncAddr (((Goto i) /. m),j)
then m in {0} by CARD_1:49, AFINSQ_1:33;
then A3: m = 0 by TARSKI:def 1;
A4: (Goto i) /. m = (Goto i) . m by A2, PARTFUN1:def 6
.= goto i by A3 ;
thus <%(goto (i + j))%> . m = goto (i + j) by A3
.= IncAddr (((Goto i) /. m),j) by A4, SCMFSA10:41 ; :: thesis: verum
end;
hence IncAddr ((Goto i),j) = <%(goto (i + j))%> by A1, COMPOS_1:def 21; :: thesis: verum