[mizar] the carrier of and [#]

[Jesse Alama <alama@stanford.edu>]

I faced a surprising problem recently concerning a seeming lack of
equality of

  [#]V

and

  the carrier of V,

where V has type VectSp of F, and F has type Field.  Specifically, the
statement

  consider G being FinSequence of [#]V such that
    G is one-to-one and
    rng G = Carrier l and
    x - y = Sum (l (#) G) by VECTSP_6:def 9;
::>                  *103

where l is type Linear_Combination of A, A has type Subset of V, and x
and y have type Element of V, is rejected.  For reference,
VECTSP_6:def 9 is

  definition let GF be non empty LoopStr;
             let V be non empty VectSpStr over GF;
             let L be Linear_Combination of V;
   assume A1: V is Abelian add-associative right_zeroed right_complementable;
   func Sum(L) -> Element of V means
    :Def9: ex F being FinSequence of the carrier of V st
      F is one-to-one & rng F = Carrier(L) & it = Sum(L (#) F);

However, by changing "[#]V" to "the carrier of V", my statement is
accepted.  This surprised me, since, according to STRUCT_0:def 3, we
have [#]V = the carrier of V, and my original statement is rejected
even if I cite STRUCT_0:def 3.  What might be going on?

Thanks,

Jesse

-- 
Jesse Alama (alama@stanford.edu)
*950: Too many schemes (http://www.mizar.org)