let N be with_non-empty_elements set ; :: thesis: for S being non empty stored-program definite AMI-Struct of N
for f being Function of the Instructions of S,the Instructions of S
for s being NAT -defined FinPartState of holds dom (f * s) = dom s
let S be non empty stored-program definite AMI-Struct of N; :: thesis: for f being Function of the Instructions of S,the Instructions of S
for s being NAT -defined FinPartState of holds dom (f * s) = dom s
let f be Function of the Instructions of S,the Instructions of S; :: thesis: for s being NAT -defined FinPartState of holds dom (f * s) = dom s
let s be NAT -defined FinPartState of ; :: thesis: dom (f * s) = dom s
dom f = the Instructions of S by FUNCT_2:def 1;
then rng s c= dom f by Th118;
hence dom (f * s) = dom s by RELAT_1:46; :: thesis: verum