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