let x be set ; :: according to RELAT_1:def 19,TARSKI:def 3 :: thesis: ( not x in proj2 (IncAddr p,k) or x in the Instructions of SCM )
assume x in rng (IncAddr p,k) ; :: thesis: x in the Instructions of SCM
then consider y being set such that
W1: y in dom (IncAddr p,k) and
W2: (IncAddr p,k) . y = x by FUNCT_1:def 5;
A: y in dom p by W1, Def5;
dom p c= NAT by RELAT_1:def 18;
then reconsider y = y as Element of NAT by A;
x = IncAddr (p /. y),k by W2, A, Def5;
hence x in the Instructions of SCM ; :: thesis: verum