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