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