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