let n be non zero Element of NAT ; :: thesis: for A being FinSequence of n -tuples_on BOOLEAN

for B being finite Subset of (n -BinaryVectSp) st rng A = B & len A = n & A is one-to-one & ( for i, j being Nat st i in Seg n & j in Seg n holds

( ( i = j implies (A . i) . j = TRUE ) & ( i <> j implies (A . i) . j = FALSE ) ) ) holds

Lin B = ModuleStr(# the carrier of (n -BinaryVectSp), the addF of (n -BinaryVectSp), the ZeroF of (n -BinaryVectSp), the lmult of (n -BinaryVectSp) #)

let A be FinSequence of n -tuples_on BOOLEAN; :: thesis: for B being finite Subset of (n -BinaryVectSp) st rng A = B & len A = n & A is one-to-one & ( for i, j being Nat st i in Seg n & j in Seg n holds

( ( i = j implies (A . i) . j = TRUE ) & ( i <> j implies (A . i) . j = FALSE ) ) ) holds

Lin B = ModuleStr(# the carrier of (n -BinaryVectSp), the addF of (n -BinaryVectSp), the ZeroF of (n -BinaryVectSp), the lmult of (n -BinaryVectSp) #)

let B be finite Subset of (n -BinaryVectSp); :: thesis: ( rng A = B & len A = n & A is one-to-one & ( for i, j being Nat st i in Seg n & j in Seg n holds

( ( i = j implies (A . i) . j = TRUE ) & ( i <> j implies (A . i) . j = FALSE ) ) ) implies Lin B = ModuleStr(# the carrier of (n -BinaryVectSp), the addF of (n -BinaryVectSp), the ZeroF of (n -BinaryVectSp), the lmult of (n -BinaryVectSp) #) )

assume that

A1: rng A = B and

A2: len A = n and

A3: A is one-to-one and

A4: for i, j being Nat st i in Seg n & j in Seg n holds

( ( i = j implies (A . i) . j = TRUE ) & ( i <> j implies (A . i) . j = FALSE ) ) ; :: thesis: Lin B = ModuleStr(# the carrier of (n -BinaryVectSp), the addF of (n -BinaryVectSp), the ZeroF of (n -BinaryVectSp), the lmult of (n -BinaryVectSp) #)

set V = n -BinaryVectSp ;

for x being object holds

( x in the carrier of (Lin B) iff x in the carrier of (n -BinaryVectSp) )

for B being finite Subset of (n -BinaryVectSp) st rng A = B & len A = n & A is one-to-one & ( for i, j being Nat st i in Seg n & j in Seg n holds

( ( i = j implies (A . i) . j = TRUE ) & ( i <> j implies (A . i) . j = FALSE ) ) ) holds

Lin B = ModuleStr(# the carrier of (n -BinaryVectSp), the addF of (n -BinaryVectSp), the ZeroF of (n -BinaryVectSp), the lmult of (n -BinaryVectSp) #)

let A be FinSequence of n -tuples_on BOOLEAN; :: thesis: for B being finite Subset of (n -BinaryVectSp) st rng A = B & len A = n & A is one-to-one & ( for i, j being Nat st i in Seg n & j in Seg n holds

( ( i = j implies (A . i) . j = TRUE ) & ( i <> j implies (A . i) . j = FALSE ) ) ) holds

Lin B = ModuleStr(# the carrier of (n -BinaryVectSp), the addF of (n -BinaryVectSp), the ZeroF of (n -BinaryVectSp), the lmult of (n -BinaryVectSp) #)

let B be finite Subset of (n -BinaryVectSp); :: thesis: ( rng A = B & len A = n & A is one-to-one & ( for i, j being Nat st i in Seg n & j in Seg n holds

( ( i = j implies (A . i) . j = TRUE ) & ( i <> j implies (A . i) . j = FALSE ) ) ) implies Lin B = ModuleStr(# the carrier of (n -BinaryVectSp), the addF of (n -BinaryVectSp), the ZeroF of (n -BinaryVectSp), the lmult of (n -BinaryVectSp) #) )

assume that

A1: rng A = B and

A2: len A = n and

A3: A is one-to-one and

A4: for i, j being Nat st i in Seg n & j in Seg n holds

( ( i = j implies (A . i) . j = TRUE ) & ( i <> j implies (A . i) . j = FALSE ) ) ; :: thesis: Lin B = ModuleStr(# the carrier of (n -BinaryVectSp), the addF of (n -BinaryVectSp), the ZeroF of (n -BinaryVectSp), the lmult of (n -BinaryVectSp) #)

set V = n -BinaryVectSp ;

for x being object holds

( x in the carrier of (Lin B) iff x in the carrier of (n -BinaryVectSp) )

proof

hence
Lin B = ModuleStr(# the carrier of (n -BinaryVectSp), the addF of (n -BinaryVectSp), the ZeroF of (n -BinaryVectSp), the lmult of (n -BinaryVectSp) #)
by TARSKI:2, VECTSP_4:31; :: thesis: verum
let x be object ; :: thesis: ( x in the carrier of (Lin B) iff x in the carrier of (n -BinaryVectSp) )

then reconsider v = x as Element of n -tuples_on BOOLEAN ;

consider l being Linear_Combination of B such that

A6: for j being Nat st j in Seg n holds

v . j = l . (A . j) by Th11, A1, A2, A3;

reconsider Suml = Sum l as Element of n -tuples_on BOOLEAN ;

A7: len v = n by Lm1;

A8: len Suml = n by Lm1;

A9: dom v = Seg n by FINSEQ_1:def 3, A7

.= dom Suml by FINSEQ_1:def 3, A8 ;

for j being Nat st j in dom v holds

v . j = Suml . j

hence x in the carrier of (Lin B) by STRUCT_0:def 5; :: thesis: verum

end;hereby :: thesis: ( x in the carrier of (n -BinaryVectSp) implies x in the carrier of (Lin B) )

assume
x in the carrier of (n -BinaryVectSp)
; :: thesis: x in the carrier of (Lin B)assume A5:
x in the carrier of (Lin B)
; :: thesis: x in the carrier of (n -BinaryVectSp)

the carrier of (Lin B) c= the carrier of (n -BinaryVectSp) by VECTSP_4:def 2;

hence x in the carrier of (n -BinaryVectSp) by A5; :: thesis: verum

end;the carrier of (Lin B) c= the carrier of (n -BinaryVectSp) by VECTSP_4:def 2;

hence x in the carrier of (n -BinaryVectSp) by A5; :: thesis: verum

then reconsider v = x as Element of n -tuples_on BOOLEAN ;

consider l being Linear_Combination of B such that

A6: for j being Nat st j in Seg n holds

v . j = l . (A . j) by Th11, A1, A2, A3;

reconsider Suml = Sum l as Element of n -tuples_on BOOLEAN ;

A7: len v = n by Lm1;

A8: len Suml = n by Lm1;

A9: dom v = Seg n by FINSEQ_1:def 3, A7

.= dom Suml by FINSEQ_1:def 3, A8 ;

for j being Nat st j in dom v holds

v . j = Suml . j

proof

then
x in Lin B
by FINSEQ_1:13, A9, VECTSP_7:7;
let j be Nat; :: thesis: ( j in dom v implies v . j = Suml . j )

assume j in dom v ; :: thesis: v . j = Suml . j

then A10: j in Seg n by FINSEQ_1:def 3, A7;

thus v . j = l . (A . j) by A6, A10

.= Suml . j by Th9, A1, A2, A3, A4, A10 ; :: thesis: verum

end;assume j in dom v ; :: thesis: v . j = Suml . j

then A10: j in Seg n by FINSEQ_1:def 3, A7;

thus v . j = l . (A . j) by A6, A10

.= Suml . j by Th9, A1, A2, A3, A4, A10 ; :: thesis: verum

hence x in the carrier of (Lin B) by STRUCT_0:def 5; :: thesis: verum