let N be with_non-empty_elements set ; :: thesis: for S being non empty stored-program definite AMI-Struct of N
for f being NAT -defined the Instructions of b₁ -valued Function holds f is PartState of S
let S be non empty stored-program definite AMI-Struct of N; :: thesis: for f being NAT -defined the Instructions of S -valued Function holds f is PartState of S
let f be NAT -defined the Instructions of S -valued Function; :: thesis: f is PartState of S
B: dom f c= NAT by RELAT_1:def 18;
NAT c= the carrier of S by Def3;
then A: dom f c= the carrier of S by B, XBOOLE_1:1;
for x being set st x in dom f holds
f . x in the Object-Kind of S . x

proof

let x be set ; :: thesis: ( x in dom f implies f . x in the Object-Kind of S . x )
assume Z: x in dom f ; :: thesis: f . x in the Object-Kind of S . x
then reconsider x = x as Element of NAT by B;
f . x in the Instructions of S by Z, FUNCT_1:172;
hence f . x in the Object-Kind of S . x by Def14; :: thesis: verum

end;

hence f is PartState of S by A, RELAT_1:def 18, FUNCT_1:def 20; :: thesis: verum