[mizar] trouble with a term not having the expected type

[Jesse Alama <alama@stanford.edu>]

I'm working on a proof in which I'd like to use the treatment of sums
of finite sets of elements of a field as given in FVSUM_1.  That is,
I'm trying to use the symbol `Sum' whose meaning is defined in
FVSUM_1:def 8.  But the meaning attached to `Sum' in my proof comes
from RLVECT_1:def 12 rather than FVSUM_1:def 8.  I've confirmed this
by looking at the constructor explanation for the existence claim for
a definition of mine that uses `Sum', as well as by looking at the XML
file generated by the verifier.

Here's the definition I'm looking at:

definition let p be polyhedron, c be 0-chain of p;
  func boundary(p,c) -> -1-chain of p means :Def26:
  for x being -1-polytope of p
    holds it.x = Sum T(p,c,x);

The operator T in that definition is defined as:

definition let p be polyhedron, c be 0-chain of p, x be -1-polytope of p;
  func T(p,c,x) -> FinSequence of the carrier of F2 means
  ex f being FinSequence st
    rng f = V(p) &
    dom it = V(p) &
    for i being Element of NAT st i in V(p)
      ex v being vertex of p
        st v = f.i & it.i = cc(p,x,v);

F2 is a term of type Field (it represents the field whose carrier is
{0,1} and with the usual operations and constants).

The definition of the unary functor Sum in RLVECT_1 requires its
argument F to be of type

  FinSequence of the carrier of V,

where V has type

  non empty LoopStr.

The definition of the unary functor Sum in FVSUM_1 requires its
argument F to be of type

  FinSequence of the carrier of K,

where K has type 

  non empty Abelian add-associative right_zeroed right_complementable LoopStr.

I've set up the constructors environment in my file to be in MML.LAR
order; more precisely, it is

 constructors FINSET_1, XBOOLE_0, NAT_1, FUNCT_1, FUNCT_2, CARD_1,
   ZFMISC_1, SUBSET_1, TARSKI, MCART_1, RELAT_1, NUMBERS, ORDINAL2,
   RLVECT_1, LATTICES, GROUP_1, VECTSP_1, VECTSP_9, INT_1, STRUCT_0,
   BINOP_1, MCART_2, FRAENKEL, ENUMSET1, RELSET_1, PARTFUN1, REALSET1,
   FINSEQ_1, FINSOP_1, FVSUM_1, VECSP_9;

How can I ensure that the constructor attached to the symbol `Sum' in
my definition of boundary is the one in FVSUM_1 rather than the one in
RLVECT_1?

Thanks,

Jesse

-- 
Jesse Alama (alama@stanford.edu)
*14: Too many terms in an inference (http://www.mizar.org)