On Wed, 4 Apr 2007, Jesse Alama wrote:
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?
Is STRUCT_0 listed in the 'definitions' directive? - only then the
equals' definition works automatically - adding a subsequent reference
to a universal sentence (the definitional theorem of STRUCT_0:def 3)
won't help since the checker is able to use only one such universal
premise in one disjunct in an inference.