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