let N be non empty with_non-empty_elements set ; :: thesis: for S being non empty stored-program IC-Ins-separated definite realistic COM-Struct of N
for s being State of S
for X being set st X c= NAT holds
rng (s | X) c= the Instructions of S
let S be non empty stored-program IC-Ins-separated definite realistic COM-Struct of N; :: thesis: for s being State of S
for X being set st X c= NAT holds
rng (s | X) c= the Instructions of S
let s be State of S; :: thesis: for X being set st X c= NAT holds
rng (s | X) c= the Instructions of S
let X be set ; :: thesis: ( X c= NAT implies rng (s | X) c= the Instructions of S )
assume A1: X c= NAT ; :: thesis: rng (s | X) c= the Instructions of S
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in rng (s | X) or x in the Instructions of S )
assume x in rng (s | X) ; :: thesis: x in the Instructions of S
then consider y being set such that
A2: y in dom (s | X) and
A3: (s | X) . y = x by FUNCT_1:def 5;
A4: dom (s | X) c= X by RELAT_1:87;
then dom (s | X) c= NAT by A1, XBOOLE_1:1;
then reconsider y = y as Element of NAT by A2;
x = s . y by A2, A3, A4, FUNCT_1:72;
hence x in the Instructions of S ; :: thesis: verum