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
A1:
u in dom (p | NAT)
and
A2:
e = (p | NAT) . u
by FUNCT_1:def 5;
A3:
dom (p | NAT) = NAT /\ (dom p)
by RELAT_1:90;
then A4:
u in NAT
by A1, XBOOLE_0:def 4;
then A5:
the Object-Kind of S . u = the Instructions of S
by Def8;
reconsider u = u as Nat by A1;
A6:
u in dom p
by A3, A1, XBOOLE_0:def 4;
(p | NAT) . u = p . u
by A4, FUNCT_1:72;
hence
e in the Instructions of S
by A2, A6, A5, FUNCT_1:def 20; verum