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