E: dom (IncAddr F,k) = dom F by Def15;
hence dom (IncAddr F,k) c= NAT by RELAT_1:def 18; :: according to RELAT_1:def 18 :: thesis: IncAddr F,k is the Instructions of S -valued
let x be set ; :: according to TARSKI:def 3,RELAT_1:def 19 :: thesis: ( not x in proj2 (IncAddr F,k) or x in the Instructions of S )
assume x in rng (IncAddr F,k) ; :: thesis: x in the Instructions of S
then consider y being set such that
W1: y in dom F and
W2: x = (IncAddr F,k) . y by E, FUNCT_1:def 5;
dom F c= NAT by RELAT_1:def 18;
then y is Nat by W1;
then consider m being Nat such that
W3: y = il. S,m by AMISTD_1:26;
x = IncAddr (F /. (il. S,m)),k by W1, W2, Def15, W3;
hence x in the Instructions of S ; :: thesis: verum