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