set A = Free (C,(MSVars C));
dom (f #) = Union the Sorts of (Free (C,(MSVars C))) by FUNCT_2:def 1;
then A2: dom ((f #) * p) = dom p by A1, RELAT_1:27;
dom p = Seg (len p) by FINSEQ_1:def 3;
hence (f #) * p is FinSequence by A2, FINSEQ_1:def 2; :: thesis: verum