let f be XFinSequence; :: thesis: f is NAT -defined
thus dom f c= NAT ; :: according to RELAT_1:def 18 :: thesis: verum