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:4; :: thesis: verum