let e be set ; RELAT_1:def 19,TARSKI:def 3 ( not e in proj2 (ProgramPart s) or e in the Instructions of S )
assume
e in rng (ProgramPart s)
; e in the Instructions of S
then consider u being set such that
W1:
u in dom (ProgramPart s)
and
W2:
e = (ProgramPart s) . u
by FUNCT_1:def 5;
B:
dom (ProgramPart s) = NAT /\ (dom s)
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 s
by B, W1, XBOOLE_0:def 4;
then C:
(ProgramPart s) . u = s . u
by BWL2;
s . 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