let F be FinPartState of S; :: thesis: ( F is empty implies ( F is the Instructions of S -valued & F is NAT -defined ) )
assume Z: F is empty ; :: thesis: ( F is the Instructions of S -valued & F is NAT -defined )
then rng F = {} ;
hence rng F c= the Instructions of S by XBOOLE_1:2; :: according to RELAT_1:def 19 :: thesis: F is NAT -defined
dom F = {} by Z;
hence dom F c= NAT by XBOOLE_1:2; :: according to RELAT_1:def 18 :: thesis: verum