let e be set ; RELAT_1:def 19,TARSKI:def 3 ( not e in proj2 (p | NAT) or e in the Instructions of S )
assume
e in rng (p | NAT)
; e in the Instructions of S
then consider u being set such that
W1:
u in dom (p | NAT)
and
W2:
e = (p | NAT) . u
by FUNCT_1:def 5;
B:
dom (p | NAT) = NAT /\ (dom p)
by RELAT_1:90;
then D:
u in NAT
by W1, XBOOLE_0:def 4;
then A:
the Object-Kind of S . u = the Instructions of S
by Def8;
reconsider u = u as Nat by D;
E:
u in dom p
by B, W1, XBOOLE_0:def 4;
C:
(p | NAT) . u = p . u
by D, FUNCT_1:72;
p . u in the Object-Kind of S . u
by E, FUNCT_1:def 20;
hence
e in the Instructions of S
by W2, C, A; verum