let n be non zero Element of NAT ; :: thesis: for A being FinSequence of n -tuples_on BOOLEAN
for B being finite Subset of () 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 (), the addF of (), the ZeroF of (), the lmult of () #)

let A be FinSequence of n -tuples_on BOOLEAN; :: thesis: for B being finite Subset of () 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 (), the addF of (), the ZeroF of (), the lmult of () #)

let B be finite Subset of (); :: 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 (), the addF of (), the ZeroF of (), the lmult of () #) )

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 (), the addF of (), the ZeroF of (), the lmult of () #)
set V = n -BinaryVectSp ;
for x being object holds
( x in the carrier of (Lin B) iff x in the carrier of () )
proof
let x be object ; :: thesis: ( x in the carrier of (Lin B) iff x in the carrier of () )
hereby :: thesis: ( x in the carrier of () implies x in the carrier of (Lin B) )
assume A5: x in the carrier of (Lin B) ; :: thesis: x in the carrier of ()
the carrier of (Lin B) c= the carrier of () by VECTSP_4:def 2;
hence x in the carrier of () by A5; :: thesis: verum
end;
assume x in the carrier of () ; :: thesis: x in the carrier of (Lin B)
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
.= dom Suml by ;
for j being Nat st j in dom v holds
v . j = Suml . j
proof
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 ;
thus v . j = l . (A . j) by
.= Suml . j by Th9, A1, A2, A3, A4, A10 ; :: thesis: verum
end;
then x in Lin B by ;
hence x in the carrier of (Lin B) by STRUCT_0:def 5; :: thesis: verum
end;
hence Lin B = ModuleStr(# the carrier of (), the addF of (), the ZeroF of (), the lmult of () #) by ; :: thesis: verum