let D be non empty set ; :: thesis: for p being FinSequence of D
for f being Function of (dom p),(dom p) holds p * f is FinSequence of D
let p be FinSequence of D; :: thesis: for f being Function of (dom p),(dom p) holds p * f is FinSequence of D
Seg (len p) = dom p by FINSEQ_1:def 3;
hence for f being Function of (dom p),(dom p) holds p * f is FinSequence of D by Th43; :: thesis: verum