let F be Function; :: thesis: ( F is NAT -defined implies F is the carrier of SCM+FSA -defined )
assume Z: dom F c= NAT ; :: according to RELAT_1:def 18 :: thesis: F is the carrier of SCM+FSA -defined
thus dom F c= the carrier of SCM+FSA by Z, XBOOLE_1:1; :: according to RELAT_1:def 18 :: thesis: verum