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 f being Function of the Instructions of S,the Instructions of S
for s being IL -defined FinPartState of S holds dom (f * s) = dom s
let N be with_non-empty_elements set ; :: thesis: for S being non empty stored-program definite AMI-Struct of IL,N
for f being Function of the Instructions of S,the Instructions of S
for s being IL -defined FinPartState of S holds dom (f * s) = dom s
let S be non empty stored-program definite AMI-Struct of IL,N; :: thesis: for f being Function of the Instructions of S,the Instructions of S
for s being IL -defined FinPartState of S holds dom (f * s) = dom s
let f be Function of the Instructions of S,the Instructions of S; :: thesis: for s being IL -defined FinPartState of S holds dom (f * s) = dom s
let s be IL -defined FinPartState of S; :: 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