let N be with_non-empty_elements set ; :: thesis: for S being non empty stored-program definite AMI-Struct of N
for p being NAT -defined FinPartState of holds rng p c= the Instructions of S
let S be non empty stored-program definite AMI-Struct of N; :: thesis: for p being NAT -defined FinPartState of holds rng p c= the Instructions of S
let p be NAT -defined FinPartState of ; :: thesis: rng p c= the Instructions of S
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
A1: y in dom p and
A2: x = p . y by FUNCT_1:def 5;
dom p c= NAT by RELAT_1:def 18;
then reconsider y = y as Element of NAT by A1;
the Object-Kind of S . y = the Instructions of S by Def14;
hence x in the Instructions of S by A1, A2, FUNCT_1:def 20; :: thesis: verum