let F be finite Field; :: thesis: for V being VectSp of F

for n, q being Nat st V is finite-dimensional & n = dim V & q = card the carrier of F holds

card the carrier of V = q |^ n

let V be VectSp of F; :: thesis: for n, q being Nat st V is finite-dimensional & n = dim V & q = card the carrier of F holds

card the carrier of V = q |^ n

let n, q be Nat; :: thesis: ( V is finite-dimensional & n = dim V & q = card the carrier of F implies card the carrier of V = q |^ n )

assume that

A1: V is finite-dimensional and

A2: n = dim V and

A3: q = card the carrier of F ; :: thesis: card the carrier of V = q |^ n

consider B being finite Subset of V such that

A4: B is Basis of V by A1, MATRLIN:def 1;

A5: B is linearly-independent by A4, VECTSP_7:def 3;

A6: Lin B = ModuleStr(# the carrier of V, the addF of V, the ZeroF of V, the lmult of V #) by A4, VECTSP_7:def 3;

A7: card B = n by A1, A2, A4, VECTSP_9:def 1;

for n, q being Nat st V is finite-dimensional & n = dim V & q = card the carrier of F holds

card the carrier of V = q |^ n

let V be VectSp of F; :: thesis: for n, q being Nat st V is finite-dimensional & n = dim V & q = card the carrier of F holds

card the carrier of V = q |^ n

let n, q be Nat; :: thesis: ( V is finite-dimensional & n = dim V & q = card the carrier of F implies card the carrier of V = q |^ n )

assume that

A1: V is finite-dimensional and

A2: n = dim V and

A3: q = card the carrier of F ; :: thesis: card the carrier of V = q |^ n

consider B being finite Subset of V such that

A4: B is Basis of V by A1, MATRLIN:def 1;

A5: B is linearly-independent by A4, VECTSP_7:def 3;

A6: Lin B = ModuleStr(# the carrier of V, the addF of V, the ZeroF of V, the lmult of V #) by A4, VECTSP_7:def 3;

A7: card B = n by A1, A2, A4, VECTSP_9:def 1;

now :: thesis: card the carrier of V = q |^ nend;

hence
card the carrier of V = q |^ n
; :: thesis: verumper cases
( n = 0 or n <> 0 )
;

end;

suppose A8:
n = 0
; :: thesis: card the carrier of V = q |^ n

then
(Omega). V = (0). V
by A1, A2, VECTSP_9:29;

then ModuleStr(# the carrier of V, the addF of V, the ZeroF of V, the lmult of V #) = (0). V by VECTSP_4:def 4;

then the carrier of V = {(0. V)} by VECTSP_4:def 3;

then card the carrier of V = 1 by CARD_1:30

.= q #Z 0 by PREPOWER:34

.= q |^ 0 by PREPOWER:36 ;

hence card the carrier of V = q |^ n by A8; :: thesis: verum

end;then ModuleStr(# the carrier of V, the addF of V, the ZeroF of V, the lmult of V #) = (0). V by VECTSP_4:def 4;

then the carrier of V = {(0. V)} by VECTSP_4:def 3;

then card the carrier of V = 1 by CARD_1:30

.= q #Z 0 by PREPOWER:34

.= q |^ 0 by PREPOWER:36 ;

hence card the carrier of V = q |^ n by A8; :: thesis: verum

suppose
n <> 0
; :: thesis: card the carrier of V = q |^ n

then A9:
B <> 0
by A7;

consider bf being FinSequence such that

A10: rng bf = B and

A11: bf is one-to-one by FINSEQ_4:58;

len bf = n by A7, A10, A11, FINSEQ_4:62;

then A12: Seg n = dom bf by FINSEQ_1:def 3;

reconsider Vbf = bf as FinSequence of the carrier of V by A10, FINSEQ_1:def 4;

set cLinB = the carrier of (Lin B);

set ntocF = n -tuples_on the carrier of F;

defpred S_{1}[ Function, set ] means ex lc being Linear_Combination of B st

( ( for i being set st i in dom $1 holds

lc . (Vbf . i) = $1 . i ) & $2 = Sum (lc (#) Vbf) );

A13: for x being Element of n -tuples_on the carrier of F ex y being Element of the carrier of (Lin B) st S_{1}[x,y]

A32: for tup being Element of n -tuples_on the carrier of F holds S_{1}[tup,G . tup]
from FUNCT_2:sch 3(A13);

A33: dom G = n -tuples_on the carrier of F by FUNCT_2:def 1;

A34: for L being Linear_Combination of B ex nt being Element of n -tuples_on the carrier of F st

for i being object st i in dom nt holds

nt . i = L . (Vbf . i)

ex x being object st

( x in n -tuples_on the carrier of F & c = G . x )

for x1, x2 being object st x1 in dom G & x2 in dom G & G . x1 = G . x2 holds

x1 = x2

then n -tuples_on the carrier of F,G .: (n -tuples_on the carrier of F) are_equipotent by A33, CARD_1:33;

then A69: n -tuples_on the carrier of F, the carrier of (Lin B) are_equipotent by A33, A54, RELAT_1:113;

A70: card (Seg n) = card n by FINSEQ_1:55;

A71: card q = card the carrier of F by A3;

card (n -tuples_on the carrier of F) = card (Funcs ((Seg n), the carrier of F)) by FINSEQ_2:93

.= card (Funcs (n,q)) by A70, A71, FUNCT_5:61

.= q |^ n by A3, Th4 ;

hence card the carrier of V = q |^ n by A6, A69, CARD_1:5; :: thesis: verum

end;consider bf being FinSequence such that

A10: rng bf = B and

A11: bf is one-to-one by FINSEQ_4:58;

len bf = n by A7, A10, A11, FINSEQ_4:62;

then A12: Seg n = dom bf by FINSEQ_1:def 3;

reconsider Vbf = bf as FinSequence of the carrier of V by A10, FINSEQ_1:def 4;

set cLinB = the carrier of (Lin B);

set ntocF = n -tuples_on the carrier of F;

defpred S

( ( for i being set st i in dom $1 holds

lc . (Vbf . i) = $1 . i ) & $2 = Sum (lc (#) Vbf) );

A13: for x being Element of n -tuples_on the carrier of F ex y being Element of the carrier of (Lin B) st S

proof

consider G being Function of (n -tuples_on the carrier of F), the carrier of (Lin B) such that
let f be Element of n -tuples_on the carrier of F; :: thesis: ex y being Element of the carrier of (Lin B) st S_{1}[f,y]

ex lc being Linear_Combination of B st

for i being set st i in dom f holds

lc . (Vbf . i) = f . i

A31: for i being set st i in dom f holds

lc . (Vbf . i) = f . i ;

ex y being Element of V st y = Sum (lc (#) Vbf) ;

hence ex y being Element of the carrier of (Lin B) st S_{1}[f,y]
by A6, A31; :: thesis: verum

end;ex lc being Linear_Combination of B st

for i being set st i in dom f holds

lc . (Vbf . i) = f . i

proof

then consider lc being Linear_Combination of B such that
deffunc H_{1}( object ) -> set = f . (union (Vbf " {$1}));

A14: for x being object st x in B holds

H_{1}(x) in the carrier of F

A17: for y being object st y in B holds

lc . y = H_{1}(y)
from FUNCT_2:sch 2(A14);

set ll = lc +* (( the carrier of V \ B) --> (0. F));

A18: dom (( the carrier of V \ B) --> (0. F)) = the carrier of V \ B ;

then dom (lc +* (( the carrier of V \ B) --> (0. F))) = (dom lc) \/ ( the carrier of V \ B) by FUNCT_4:def 1;

then dom (lc +* (( the carrier of V \ B) --> (0. F))) = B \/ ( the carrier of V \ B) by FUNCT_2:def 1;

then dom (lc +* (( the carrier of V \ B) --> (0. F))) = B \/ the carrier of V by XBOOLE_1:39;

then A19: dom (lc +* (( the carrier of V \ B) --> (0. F))) = the carrier of V by XBOOLE_1:12;

rng (lc +* (( the carrier of V \ B) --> (0. F))) c= (rng lc) \/ (rng (( the carrier of V \ B) --> (0. F))) by FUNCT_4:17;

then lc +* (( the carrier of V \ B) --> (0. F)) is Function of the carrier of V, the carrier of F by A19, FUNCT_2:2, XBOOLE_1:1;

then A20: lc +* (( the carrier of V \ B) --> (0. F)) is Element of Funcs ( the carrier of V, the carrier of F) by FUNCT_2:8;

A21: for i being set st i in dom f holds

(lc +* (( the carrier of V \ B) --> (0. F))) . (Vbf . i) = f . i

(lc +* (( the carrier of V \ B) --> (0. F))) . v = 0. F

for v being Element of V st v in Carrier L holds

v in B

then L is Linear_Combination of B by VECTSP_6:def 4;

hence ex lc being Linear_Combination of B st

for i being set st i in dom f holds

lc . (Vbf . i) = f . i by A21; :: thesis: verum

end;A14: for x being object st x in B holds

H

proof

consider lc being Function of B, the carrier of F such that
let x be object ; :: thesis: ( x in B implies H_{1}(x) in the carrier of F )

assume x in B ; :: thesis: H_{1}(x) in the carrier of F

then consider i being object such that

A15: Vbf " {x} = {i} by A10, A11, FUNCT_1:74;

A16: union (Vbf " {x}) = i by A15, ZFMISC_1:25;

i in Vbf " {x} by A15, TARSKI:def 1;

then i in dom Vbf by FUNCT_1:def 7;

then i in dom f by A12, FINSEQ_2:124;

then f . i in rng f by FUNCT_1:3;

hence H_{1}(x) in the carrier of F
by A16; :: thesis: verum

end;assume x in B ; :: thesis: H

then consider i being object such that

A15: Vbf " {x} = {i} by A10, A11, FUNCT_1:74;

A16: union (Vbf " {x}) = i by A15, ZFMISC_1:25;

i in Vbf " {x} by A15, TARSKI:def 1;

then i in dom Vbf by FUNCT_1:def 7;

then i in dom f by A12, FINSEQ_2:124;

then f . i in rng f by FUNCT_1:3;

hence H

A17: for y being object st y in B holds

lc . y = H

set ll = lc +* (( the carrier of V \ B) --> (0. F));

A18: dom (( the carrier of V \ B) --> (0. F)) = the carrier of V \ B ;

then dom (lc +* (( the carrier of V \ B) --> (0. F))) = (dom lc) \/ ( the carrier of V \ B) by FUNCT_4:def 1;

then dom (lc +* (( the carrier of V \ B) --> (0. F))) = B \/ ( the carrier of V \ B) by FUNCT_2:def 1;

then dom (lc +* (( the carrier of V \ B) --> (0. F))) = B \/ the carrier of V by XBOOLE_1:39;

then A19: dom (lc +* (( the carrier of V \ B) --> (0. F))) = the carrier of V by XBOOLE_1:12;

rng (lc +* (( the carrier of V \ B) --> (0. F))) c= (rng lc) \/ (rng (( the carrier of V \ B) --> (0. F))) by FUNCT_4:17;

then lc +* (( the carrier of V \ B) --> (0. F)) is Function of the carrier of V, the carrier of F by A19, FUNCT_2:2, XBOOLE_1:1;

then A20: lc +* (( the carrier of V \ B) --> (0. F)) is Element of Funcs ( the carrier of V, the carrier of F) by FUNCT_2:8;

A21: for i being set st i in dom f holds

(lc +* (( the carrier of V \ B) --> (0. F))) . (Vbf . i) = f . i

proof

A28:
for v being Element of V st not v in B holds
let i be set ; :: thesis: ( i in dom f implies (lc +* (( the carrier of V \ B) --> (0. F))) . (Vbf . i) = f . i )

assume i in dom f ; :: thesis: (lc +* (( the carrier of V \ B) --> (0. F))) . (Vbf . i) = f . i

then A22: i in dom Vbf by A12, FINSEQ_2:124;

then Vbf . i in B by A10, FUNCT_1:3;

then consider y being Element of B such that

A23: y = Vbf . i ;

A24: Vbf . i in {y} by A23, TARSKI:def 1;

consider ee being object such that

A25: Vbf " {y} c= {ee} by A11, FUNCT_1:89;

A26: i in Vbf " {y} by A22, A24, FUNCT_1:def 7;

then {i} c= {ee} by A25, ZFMISC_1:31;

then i = ee by ZFMISC_1:18;

then A27: Vbf " {y} = {i} by A25, A26, ZFMISC_1:33;

not y in the carrier of V \ B by A9, XBOOLE_0:def 5;

then (lc +* (( the carrier of V \ B) --> (0. F))) . y = lc . y by A18, FUNCT_4:11;

then (lc +* (( the carrier of V \ B) --> (0. F))) . y = f . (union (Vbf " {y})) by A9, A17;

hence (lc +* (( the carrier of V \ B) --> (0. F))) . (Vbf . i) = f . i by A23, A27, ZFMISC_1:25; :: thesis: verum

end;assume i in dom f ; :: thesis: (lc +* (( the carrier of V \ B) --> (0. F))) . (Vbf . i) = f . i

then A22: i in dom Vbf by A12, FINSEQ_2:124;

then Vbf . i in B by A10, FUNCT_1:3;

then consider y being Element of B such that

A23: y = Vbf . i ;

A24: Vbf . i in {y} by A23, TARSKI:def 1;

consider ee being object such that

A25: Vbf " {y} c= {ee} by A11, FUNCT_1:89;

A26: i in Vbf " {y} by A22, A24, FUNCT_1:def 7;

then {i} c= {ee} by A25, ZFMISC_1:31;

then i = ee by ZFMISC_1:18;

then A27: Vbf " {y} = {i} by A25, A26, ZFMISC_1:33;

not y in the carrier of V \ B by A9, XBOOLE_0:def 5;

then (lc +* (( the carrier of V \ B) --> (0. F))) . y = lc . y by A18, FUNCT_4:11;

then (lc +* (( the carrier of V \ B) --> (0. F))) . y = f . (union (Vbf " {y})) by A9, A17;

hence (lc +* (( the carrier of V \ B) --> (0. F))) . (Vbf . i) = f . i by A23, A27, ZFMISC_1:25; :: thesis: verum

(lc +* (( the carrier of V \ B) --> (0. F))) . v = 0. F

proof

then reconsider L = lc +* (( the carrier of V \ B) --> (0. F)) as Linear_Combination of V by A20, VECTSP_6:def 1;
let v be Element of V; :: thesis: ( not v in B implies (lc +* (( the carrier of V \ B) --> (0. F))) . v = 0. F )

assume not v in B ; :: thesis: (lc +* (( the carrier of V \ B) --> (0. F))) . v = 0. F

then A29: v in the carrier of V \ B by XBOOLE_0:def 5;

then (lc +* (( the carrier of V \ B) --> (0. F))) . v = (( the carrier of V \ B) --> (0. F)) . v by A18, FUNCT_4:13;

hence (lc +* (( the carrier of V \ B) --> (0. F))) . v = 0. F by A29, FUNCOP_1:7; :: thesis: verum

end;assume not v in B ; :: thesis: (lc +* (( the carrier of V \ B) --> (0. F))) . v = 0. F

then A29: v in the carrier of V \ B by XBOOLE_0:def 5;

then (lc +* (( the carrier of V \ B) --> (0. F))) . v = (( the carrier of V \ B) --> (0. F)) . v by A18, FUNCT_4:13;

hence (lc +* (( the carrier of V \ B) --> (0. F))) . v = 0. F by A29, FUNCOP_1:7; :: thesis: verum

for v being Element of V st v in Carrier L holds

v in B

proof

then
Carrier L c= B
;
let v be Element of V; :: thesis: ( v in Carrier L implies v in B )

assume A30: v in Carrier L ; :: thesis: v in B

end;assume A30: v in Carrier L ; :: thesis: v in B

now :: thesis: v in B

hence
v in B
; :: thesis: verumassume
not v in B
; :: thesis: contradiction

then (lc +* (( the carrier of V \ B) --> (0. F))) . v = 0. F by A28;

hence contradiction by A30, VECTSP_6:2; :: thesis: verum

end;then (lc +* (( the carrier of V \ B) --> (0. F))) . v = 0. F by A28;

hence contradiction by A30, VECTSP_6:2; :: thesis: verum

then L is Linear_Combination of B by VECTSP_6:def 4;

hence ex lc being Linear_Combination of B st

for i being set st i in dom f holds

lc . (Vbf . i) = f . i by A21; :: thesis: verum

A31: for i being set st i in dom f holds

lc . (Vbf . i) = f . i ;

ex y being Element of V st y = Sum (lc (#) Vbf) ;

hence ex y being Element of the carrier of (Lin B) st S

A32: for tup being Element of n -tuples_on the carrier of F holds S

A33: dom G = n -tuples_on the carrier of F by FUNCT_2:def 1;

A34: for L being Linear_Combination of B ex nt being Element of n -tuples_on the carrier of F st

for i being object st i in dom nt holds

nt . i = L . (Vbf . i)

proof

for c being object st c in the carrier of (Lin B) holds
let L be Linear_Combination of B; :: thesis: ex nt being Element of n -tuples_on the carrier of F st

for i being object st i in dom nt holds

nt . i = L . (Vbf . i)

deffunc H_{1}( object ) -> set = L . (Vbf . $1);

A35: for x being object st x in Seg n holds

H_{1}(x) in the carrier of F

A37: for x being object st x in Seg n holds

f . x = H_{1}(x)
from FUNCT_2:sch 2(A35);

A38: dom f = Seg n by FUNCT_2:def 1;

A39: rng f c= the carrier of F ;

A40: n is Element of NAT by ORDINAL1:def 12;

f is FinSequence-like by A38, FINSEQ_1:def 2;

then reconsider ff = f as FinSequence of the carrier of F by A39, FINSEQ_1:def 4;

len ff = n by A38, A40, FINSEQ_1:def 3;

then ff is Element of n -tuples_on the carrier of F by FINSEQ_2:92;

hence ex nt being Element of n -tuples_on the carrier of F st

for i being object st i in dom nt holds

nt . i = L . (Vbf . i) by A37, A38; :: thesis: verum

end;for i being object st i in dom nt holds

nt . i = L . (Vbf . i)

deffunc H

A35: for x being object st x in Seg n holds

H

proof

consider f being Function of (Seg n), the carrier of F such that
let x be object ; :: thesis: ( x in Seg n implies H_{1}(x) in the carrier of F )

assume x in Seg n ; :: thesis: H_{1}(x) in the carrier of F

then Vbf . x in rng Vbf by A12, FUNCT_1:3;

then consider vv being Element of V such that

A36: Vbf . x = vv ;

L . vv in the carrier of F ;

hence H_{1}(x) in the carrier of F
by A36; :: thesis: verum

end;assume x in Seg n ; :: thesis: H

then Vbf . x in rng Vbf by A12, FUNCT_1:3;

then consider vv being Element of V such that

A36: Vbf . x = vv ;

L . vv in the carrier of F ;

hence H

A37: for x being object st x in Seg n holds

f . x = H

A38: dom f = Seg n by FUNCT_2:def 1;

A39: rng f c= the carrier of F ;

A40: n is Element of NAT by ORDINAL1:def 12;

f is FinSequence-like by A38, FINSEQ_1:def 2;

then reconsider ff = f as FinSequence of the carrier of F by A39, FINSEQ_1:def 4;

len ff = n by A38, A40, FINSEQ_1:def 3;

then ff is Element of n -tuples_on the carrier of F by FINSEQ_2:92;

hence ex nt being Element of n -tuples_on the carrier of F st

for i being object st i in dom nt holds

nt . i = L . (Vbf . i) by A37, A38; :: thesis: verum

ex x being object st

( x in n -tuples_on the carrier of F & c = G . x )

proof

then A54:
rng G = the carrier of (Lin B)
by FUNCT_2:10;
let c be object ; :: thesis: ( c in the carrier of (Lin B) implies ex x being object st

( x in n -tuples_on the carrier of F & c = G . x ) )

assume c in the carrier of (Lin B) ; :: thesis: ex x being object st

( x in n -tuples_on the carrier of F & c = G . x )

then c in Lin B ;

then consider l being Linear_Combination of B such that

A41: c = Sum l by VECTSP_7:7;

Carrier l c= rng Vbf by A10, VECTSP_6:def 4;

then A42: Sum (l (#) Vbf) = Sum l by A11, VECTSP_9:3;

consider t being Element of n -tuples_on the carrier of F such that

A43: for i being object st i in dom t holds

t . i = l . (Vbf . i) by A34;

consider lc being Linear_Combination of B such that

A44: for i being set st i in dom t holds

lc . (Vbf . i) = t . i and

A45: G . t = Sum (lc (#) Vbf) by A32;

for v being Element of V holds l . v = lc . v

hence ex x being object st

( x in n -tuples_on the carrier of F & c = G . x ) by A41, A42; :: thesis: verum

end;( x in n -tuples_on the carrier of F & c = G . x ) )

assume c in the carrier of (Lin B) ; :: thesis: ex x being object st

( x in n -tuples_on the carrier of F & c = G . x )

then c in Lin B ;

then consider l being Linear_Combination of B such that

A41: c = Sum l by VECTSP_7:7;

Carrier l c= rng Vbf by A10, VECTSP_6:def 4;

then A42: Sum (l (#) Vbf) = Sum l by A11, VECTSP_9:3;

consider t being Element of n -tuples_on the carrier of F such that

A43: for i being object st i in dom t holds

t . i = l . (Vbf . i) by A34;

consider lc being Linear_Combination of B such that

A44: for i being set st i in dom t holds

lc . (Vbf . i) = t . i and

A45: G . t = Sum (lc (#) Vbf) by A32;

for v being Element of V holds l . v = lc . v

proof

then
G . t = Sum (l (#) Vbf)
by A45, VECTSP_6:def 7;
let v be Element of V; :: thesis: l . v = lc . v

end;now :: thesis: l . v = lc . vend;

hence
l . v = lc . v
; :: thesis: verumper cases
( v in rng Vbf or not v in rng Vbf )
;

end;

suppose
v in rng Vbf
; :: thesis: l . v = lc . v

then consider x being object such that

A46: [x,v] in Vbf by XTUPLE_0:def 13;

A47: x in dom Vbf by A46, FUNCT_1:1;

A48: Vbf . x = v by A46, FUNCT_1:1;

A49: x in dom t by A12, A47, FINSEQ_2:124;

then l . (Vbf . x) = t . x by A43;

hence l . v = lc . v by A44, A48, A49; :: thesis: verum

end;A46: [x,v] in Vbf by XTUPLE_0:def 13;

A47: x in dom Vbf by A46, FUNCT_1:1;

A48: Vbf . x = v by A46, FUNCT_1:1;

A49: x in dom t by A12, A47, FINSEQ_2:124;

then l . (Vbf . x) = t . x by A43;

hence l . v = lc . v by A44, A48, A49; :: thesis: verum

suppose A50:
not v in rng Vbf
; :: thesis: l . v = lc . v

end;

now :: thesis: not v in Carrier l

then A52:
l . v = 0. F
by VECTSP_6:2;assume A51:
v in Carrier l
; :: thesis: contradiction

Carrier l c= rng Vbf by A10, VECTSP_6:def 4;

hence contradiction by A50, A51; :: thesis: verum

end;Carrier l c= rng Vbf by A10, VECTSP_6:def 4;

hence contradiction by A50, A51; :: thesis: verum

now :: thesis: not v in Carrier lc

hence
l . v = lc . v
by A52, VECTSP_6:2; :: thesis: verumassume A53:
v in Carrier lc
; :: thesis: contradiction

Carrier lc c= rng Vbf by A10, VECTSP_6:def 4;

hence contradiction by A50, A53; :: thesis: verum

end;Carrier lc c= rng Vbf by A10, VECTSP_6:def 4;

hence contradiction by A50, A53; :: thesis: verum

hence ex x being object st

( x in n -tuples_on the carrier of F & c = G . x ) by A41, A42; :: thesis: verum

for x1, x2 being object st x1 in dom G & x2 in dom G & G . x1 = G . x2 holds

x1 = x2

proof

then
G is one-to-one
;
let x1, x2 be object ; :: thesis: ( x1 in dom G & x2 in dom G & G . x1 = G . x2 implies x1 = x2 )

assume that

A55: x1 in dom G and

A56: x2 in dom G and

A57: G . x1 = G . x2 ; :: thesis: x1 = x2

reconsider t1 = x1 as Element of n -tuples_on the carrier of F by A55;

reconsider t2 = x2 as Element of n -tuples_on the carrier of F by A56;

consider L1 being Linear_Combination of B such that

A58: for i being set st i in dom t1 holds

L1 . (Vbf . i) = t1 . i and

A59: G . t1 = Sum (L1 (#) Vbf) by A32;

consider L2 being Linear_Combination of B such that

A60: for i being set st i in dom t2 holds

L2 . (Vbf . i) = t2 . i and

A61: G . t2 = Sum (L2 (#) Vbf) by A32;

Carrier L1 c= rng Vbf by A10, VECTSP_6:def 4;

then A62: Sum L1 = Sum (L1 (#) Vbf) by A11, VECTSP_9:3;

Carrier L2 c= rng Vbf by A10, VECTSP_6:def 4;

then Sum L2 = Sum (L2 (#) Vbf) by A11, VECTSP_9:3;

then (Sum L1) - (Sum L2) = 0. V by A57, A59, A61, A62, VECTSP_1:19;

then A63: Sum (L1 - L2) = 0. V by VECTSP_6:47;

L1 - L2 is Linear_Combination of B by VECTSP_6:42;

then A64: Carrier (L1 - L2) = {} by A5, A63, VECTSP_7:def 1;

for v being Element of V holds L1 . v = L2 . v

A66: dom t1 = Seg n by FINSEQ_2:124;

A67: dom t2 = Seg n by FINSEQ_2:124;

for k being Nat st k in dom t1 holds

t1 . k = t2 . k

end;assume that

A55: x1 in dom G and

A56: x2 in dom G and

A57: G . x1 = G . x2 ; :: thesis: x1 = x2

reconsider t1 = x1 as Element of n -tuples_on the carrier of F by A55;

reconsider t2 = x2 as Element of n -tuples_on the carrier of F by A56;

consider L1 being Linear_Combination of B such that

A58: for i being set st i in dom t1 holds

L1 . (Vbf . i) = t1 . i and

A59: G . t1 = Sum (L1 (#) Vbf) by A32;

consider L2 being Linear_Combination of B such that

A60: for i being set st i in dom t2 holds

L2 . (Vbf . i) = t2 . i and

A61: G . t2 = Sum (L2 (#) Vbf) by A32;

Carrier L1 c= rng Vbf by A10, VECTSP_6:def 4;

then A62: Sum L1 = Sum (L1 (#) Vbf) by A11, VECTSP_9:3;

Carrier L2 c= rng Vbf by A10, VECTSP_6:def 4;

then Sum L2 = Sum (L2 (#) Vbf) by A11, VECTSP_9:3;

then (Sum L1) - (Sum L2) = 0. V by A57, A59, A61, A62, VECTSP_1:19;

then A63: Sum (L1 - L2) = 0. V by VECTSP_6:47;

L1 - L2 is Linear_Combination of B by VECTSP_6:42;

then A64: Carrier (L1 - L2) = {} by A5, A63, VECTSP_7:def 1;

for v being Element of V holds L1 . v = L2 . v

proof

then A65:
L1 = L2
by VECTSP_6:def 7;
let v be Element of V; :: thesis: L1 . v = L2 . v

reconsider LL = L1 - L2 as Linear_Combination of B by VECTSP_6:42;

LL . v = 0. F by A64, VECTSP_6:2;

then 0. F = (L1 . v) - (L2 . v) by VECTSP_6:40;

hence L1 . v = L2 . v by VECTSP_1:27; :: thesis: verum

end;reconsider LL = L1 - L2 as Linear_Combination of B by VECTSP_6:42;

LL . v = 0. F by A64, VECTSP_6:2;

then 0. F = (L1 . v) - (L2 . v) by VECTSP_6:40;

hence L1 . v = L2 . v by VECTSP_1:27; :: thesis: verum

A66: dom t1 = Seg n by FINSEQ_2:124;

A67: dom t2 = Seg n by FINSEQ_2:124;

for k being Nat st k in dom t1 holds

t1 . k = t2 . k

proof

hence
x1 = x2
by A67, FINSEQ_1:13, FINSEQ_2:124; :: thesis: verum
let k be Nat; :: thesis: ( k in dom t1 implies t1 . k = t2 . k )

assume A68: k in dom t1 ; :: thesis: t1 . k = t2 . k

t1 . k = L1 . (Vbf . k) by A58, A68;

hence t1 . k = t2 . k by A60, A65, A66, A67, A68; :: thesis: verum

end;assume A68: k in dom t1 ; :: thesis: t1 . k = t2 . k

t1 . k = L1 . (Vbf . k) by A58, A68;

hence t1 . k = t2 . k by A60, A65, A66, A67, A68; :: thesis: verum

then n -tuples_on the carrier of F,G .: (n -tuples_on the carrier of F) are_equipotent by A33, CARD_1:33;

then A69: n -tuples_on the carrier of F, the carrier of (Lin B) are_equipotent by A33, A54, RELAT_1:113;

A70: card (Seg n) = card n by FINSEQ_1:55;

A71: card q = card the carrier of F by A3;

card (n -tuples_on the carrier of F) = card (Funcs ((Seg n), the carrier of F)) by FINSEQ_2:93

.= card (Funcs (n,q)) by A70, A71, FUNCT_5:61

.= q |^ n by A3, Th4 ;

hence card the carrier of V = q |^ n by A6, A69, CARD_1:5; :: thesis: verum