let IL be non empty set ; :: thesis: for N being with_non-empty_elements set
for S being non empty stored-program definite AMI-Struct of IL,N
for p being programmed FinPartState of S holds rng p c= the Instructions of S
let N be with_non-empty_elements set ; :: thesis: for S being non empty stored-program definite AMI-Struct of IL,N
for p being programmed FinPartState of S holds rng p c= the Instructions of S
let S be non empty stored-program definite AMI-Struct of IL,N; :: thesis: for p being programmed FinPartState of S holds rng p c= the Instructions of S
let p be programmed FinPartState of S; :: thesis: rng p c= the Instructions of S
A1: dom p c= IL by Def40;
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in rng p or x in the Instructions of S )
assume x in rng p ; :: thesis: x in the Instructions of S
then consider y being set such that
A2: y in dom p and
A3: x = p . y by FUNCT_1:def 5;
reconsider y = y as Instruction-Location of S by A1, A2, Def4;
the Object-Kind of S . y = ObjectKind y
.= the Instructions of S by Def14 ;
hence x in the Instructions of S by A2, A3, CARD_3:65; :: thesis: verum