let D be non empty set ; :: thesis: for p being FinSequence of D holds p is Function of (dom p),D
let p be FinSequence of D; :: thesis: p is Function of (dom p),D
rng p c= D by FINSEQ_1:def 4;
hence p is Function of (dom p),D by FUNCT_2:2; :: thesis: verum