reconsider p = <*> X as Element of X * by FINSEQ_1:def 11;
take p ; :: thesis: p is with_the_same_arity
thus p is with_the_same_arity ; :: thesis: verum