let F be Function; :: thesis: ( F is NAT -defined implies F is the carrier of SCM+FSA -defined )
assume A1: 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 A1, XBOOLE_1:1, Lm2; :: according to RELAT_1:def 18 :: thesis: verum