let l be Element of NAT ; :: thesis: for k being Integer holds NIC ((goto k),l) = {(abs (k + l))}
let k be Integer; :: thesis: NIC ((goto k),l) = {(abs (k + l))}
consider s being State of SCMPDS;
set i = goto k;
set t = abs (k + l);
reconsider I = goto k as Element of the Object-Kind of SCMPDS . l by COMPOS_1:def 8;
reconsider n = l as Element of NAT ;
reconsider il1 = l as Element of ObjectKind (IC SCMPDS) by COMPOS_1:def 6;
((IC SCMPDS),l) --> (il1,I) = ((IC SCMPDS) .--> il1) +* (l .--> I) by FUNCT_4:def 4;
then reconsider u = s +* (((IC SCMPDS),l) --> (il1,(goto k))) as Element of product the Object-Kind of SCMPDS by PBOOLE:155;

hereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: {(abs (k + l))} c= NIC ((goto k),l)

let x be set ; :: thesis: ( x in NIC ((goto k),l) implies x in {(abs (k + l))} )
assume x in NIC ((goto k),l) ; :: thesis: x in {(abs (k + l))}
then consider s being Element of product the Object-Kind of SCMPDS such that
A3: x = IC (Exec ((goto k),s)) and
A4: IC s = l ;
A6: ex m1 being Element of NAT st
( m1 = IC s & ICplusConst (s,k) = abs (m1 + k) ) by SCMPDS_2:def 20;
x = abs (k + l) by A3, A4, A6, SCMPDS_2:66;
hence x in {(abs (k + l))} by TARSKI:def 1; :: thesis: verum

end;

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in {(abs (k + l))} or x in NIC ((goto k),l) )
A7: IC u = n by EXTPRO_1:26;
consider m1 being Element of NAT such that
A8: m1 = IC u and
A9: ICplusConst (u,k) = abs (m1 + k) by SCMPDS_2:def 20;
assume x in {(abs (k + l))} ; :: thesis: x in NIC ((goto k),l)
then x = abs (m1 + k) by A7, A8, TARSKI:def 1
.= IC (Exec ((goto k),u)) by A9, SCMPDS_2:66 ;
hence x in NIC ((goto k),l) by A7; :: thesis: verum