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 RELAT_1:def 19,TARSKI:def 3 :: 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;
x = IncAddr ((F /. y),k) by W1, W2, Def15;
hence x in the Instructions of S ; :: thesis: verum