[mizar] puzzling errors

[Jesse Alama <alama@stanford.edu>]

In the article I'm working on, the formula

  bounding-0-circuit-space(p) is Subspace of 0-circuit-space(p)

is flagged with *101 ("Unknown mode") underneath the use of Subspace.
At the stage where this formula occurs in my article, the term
bounding-0-circuit-space is just a VectSpStr over F2 (the field {0,1}
with the usual operations).  I'm trying to establish that it has type
VectSp of F2 by proving and then appealing to

for G being Field,
    U being VectSp of G,
    X being non empty Subset of the carrier of U,
    f being BinOp of X,
    l being Function of [:the carrier of G,X:],X,
    z being Element of X
  st f = (the add of U)||X &
     l = (the lmult of U)|[:the carrier of G,X:] &
     z = the Zero of U
  holds VectSpStr (# X, f, z, l #) is Subspace of U;

What surprises me is that this formula is flagged only with *4; it is
not flagged with *101.  That suggests that the last formula

  VectSpStr (# X, f, z, l #) is Subspace of U

is well-formed (in the sense that the use of Subspace there isn't
flagged with *101).  Why is my theorem about Subspaces not flagged
with *101 but my claim about bounding-0-circuit-space(p) is flagged
with that error?

Thanks,

Jesse

-- 
Jesse Alama (alama@stanford.edu)
*116: Invalid "qua" (http://www.mizar.org)