reconsider Z = {} as FinPartState of S by FUNCT_1:174, RELAT_1:206;
take Z ; :: thesis: ( Z is NAT -defined & Z is the Instructions of S -valued )
thus dom Z c= NAT by RELAT_1:60, XBOOLE_1:2; :: according to RELAT_1:def 18 :: thesis: Z is the Instructions of S -valued
thus rng Z c= the Instructions of S by RELAT_1:60, XBOOLE_1:2; :: according to RELAT_1:def 19 :: thesis: verum