Args (o,U1) = product ( the Sorts of U1 * (the_arity_of o)) by PRALG_2:3;
hence Args (o,U1) is functional ; :: thesis: verum