[mizar] unused loci

[Jesse Alama <alama@stanford.edu>]

In my proof of Euler's polyhedron formula, I'm considering functors
like this:

definition let p be polyhedron,
               f be enumeration of vertices(p),
               c be 0-chain of p;
  func Sum c -> Element of F2 means
  ex s being Element of V(p)-tuples_on the carrier of F2
    st f,s represents c & it = Sum s;          

This definition gives rise to error 100 ("unused locus").  A working
definition is

definition let p be polyhedron,
               c be 0-chain of p;
  func Sum c -> Element of F2 means
  ex f being enumeration of vertices(p),
     s being Element of V(p)-tuples_on the carrier of F2
    st f,s represents c & it = Sum s;          

It doesn't matter so much whether I use the first or the second
definition.  The first option, though, is nicer, since in its
uniqueness proof I can appeal to the fact (proved earlier) that

  f,s represents c & f,t represents c implies s = t

But in the uniqueness proof for the second case, I have to use the fact
(also proved earlier) that

  f,s represents c & g,t represents c implies Sum s = Sum t

(the antecedent implies that s is a permutation of t, and then I use
invariance of sums under permutations).

Apart from the mathematical niceness of being able to use the first
definition instead of the second, why is it that I get the unused
locus error?  I don't see why it's OK to write "Sum c" even though
there is a hidden parameters (p, the polyhedron) that doesn't need to
get expressed, but yet "Sum c" with two implicit parameters (the
polyhedron p and the enumeration f of the vertices of p) is malformed.
What's going on here?

Thanks,

Jesse

-- 
Jesse Alama (alama@stanford.edu)
*143: No implicit qualification (http://www.mizar.org)