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