let D be set ; :: thesis: for f being FinSequence of D holds f is PartFunc of NAT ,D
let f be FinSequence of D; :: thesis: f is PartFunc of NAT ,D
( dom f c= NAT & rng f c= D ) by Def4;
hence f is PartFunc of NAT ,D by RELSET_1:11; :: thesis: verum