let N be with_non-empty_elements set ; :: thesis: for S being non empty stored-program definite COM-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 COM-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;
thus f is PartState of S by A, RELAT_1:def 18; :: thesis: verum