let D be set ; :: thesis: for f being XFinSequence of D holds f is PartFunc of NAT,D
let f be XFinSequence of D; :: thesis: f is PartFunc of NAT,D
( dom f c= NAT & rng f c= D ) by RELAT_1:def 19;
hence f is PartFunc of NAT,D by RELSET_1:4; :: thesis: verum