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