let F be FinPartState of S; :: thesis: ( F is empty implies F is NAT -defined )
assume F is empty ; :: thesis: F is NAT -defined
then reconsider G = F as empty Function ;
dom G c= NAT ;
hence dom F c= NAT ; :: according to RELAT_1:def 18 :: thesis: verum