let IL be non empty set ; :: thesis: for N being with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite realistic AMI-Struct of IL,N
for s being State of S
for X being set st X c= IL holds
rng (s | X) c= the Instructions of S
let N be with_non-empty_elements set ; :: thesis: for S being non empty stored-program IC-Ins-separated definite realistic AMI-Struct of IL,N
for s being State of S
for X being set st X c= IL holds
rng (s | X) c= the Instructions of S
let S be non empty stored-program IC-Ins-separated definite realistic AMI-Struct of IL,N; :: thesis: for s being State of S
for X being set st X c= IL holds
rng (s | X) c= the Instructions of S
let s be State of S; :: thesis: for X being set st X c= IL holds
rng (s | X) c= the Instructions of S
let X be set ; :: thesis: ( X c= IL implies rng (s | X) c= the Instructions of S )
assume Z: X c= IL ; :: 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
W1: y in dom (s | X) and
W2: (s | X) . y = x by FUNCT_1:def 5;
X: dom (s | X) c= X by RELAT_1:87;
then dom (s | X) c= IL by Z, XBOOLE_1:1;
then reconsider y = y as Instruction-Location of S by W1, Def4;
x = s . y by W2, W1, X, FUNCT_1:72;
hence x in the Instructions of S ; :: thesis: verum