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:46;
dom p = Seg (len p) by FINSEQ_1:def 3;
hence (f # ) * p is FinSequence by A2, FINSEQ_1:def 2; :: thesis: verum