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 ;
A5: B is linearly-independent by ;
A6: Lin B = ModuleStr(# the carrier of V, the addF of V, the ZeroF of V, the lmult of V #) by ;
A7: card B = n by ;
now :: thesis: card the carrier of V = q |^ n
per cases ( n = 0 or n <> 0 ) ;
suppose A8: n = 0 ; :: thesis: card the carrier of V = q |^ n
then (Omega). V = (0). V by ;
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;
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 ;
then A12: Seg n = dom bf by FINSEQ_1:def 3;
reconsider Vbf = bf as FinSequence of the carrier of V by ;
set cLinB = the carrier of (Lin B);
set ntocF = n -tuples_on the carrier of F;
defpred S1[ 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 S1[x,y]
proof
let f be Element of n -tuples_on the carrier of F; :: thesis: ex y being Element of the carrier of (Lin B) st S1[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
proof
deffunc H1( object ) -> set = f . (union (Vbf " {\$1}));
A14: for x being object st x in B holds
H1(x) in the carrier of F
proof
let x be object ; :: thesis: ( x in B implies H1(x) in the carrier of F )
assume x in B ; :: thesis: H1(x) in the carrier of F
then consider i being object such that
A15: Vbf " {x} = {i} by ;
A16: union (Vbf " {x}) = i by ;
i in Vbf " {x} by ;
then i in dom Vbf by FUNCT_1:def 7;
then i in dom f by ;
then f . i in rng f by FUNCT_1:3;
hence H1(x) in the carrier of F by A16; :: thesis: verum
end;
consider lc being Function of B, the carrier of F such that
A17: for y being object st y in B holds
lc . y = H1(y) from 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 ;
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
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 ;
then Vbf . i in B by ;
then consider y being Element of B such that
A23: y = Vbf . i ;
A24: Vbf . i in {y} by ;
consider ee being object such that
A25: Vbf " {y} c= {ee} by ;
A26: i in Vbf " {y} by ;
then {i} c= {ee} by ;
then i = ee by ZFMISC_1:18;
then A27: Vbf " {y} = {i} by ;
not y in the carrier of V \ B by ;
then (lc +* (( the carrier of V \ B) --> (0. F))) . y = lc . y by ;
then (lc +* (( the carrier of V \ B) --> (0. F))) . y = f . (union (Vbf " {y})) by ;
hence (lc +* (( the carrier of V \ B) --> (0. F))) . (Vbf . i) = f . i by ; :: thesis: verum
end;
A28: for v being Element of V st not v in B holds
(lc +* (( the carrier of V \ B) --> (0. F))) . v = 0. F
proof
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 ;
hence (lc +* (( the carrier of V \ B) --> (0. F))) . v = 0. F by ; :: thesis: verum
end;
then reconsider L = lc +* (( the carrier of V \ B) --> (0. F)) as Linear_Combination of V by ;
for v being Element of V st v in Carrier L holds
v in B
proof
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
now :: thesis: v in B
assume 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;
hence v in B ; :: thesis: verum
end;
then Carrier L c= 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;
then consider lc being Linear_Combination of B such that
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 S1[f,y] by ; :: thesis: verum
end;
consider G being Function of (n -tuples_on the carrier of F), the carrier of (Lin B) such that
A32: for tup being Element of n -tuples_on the carrier of F holds S1[tup,G . tup] from 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
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 H1( object ) -> set = L . (Vbf . \$1);
A35: for x being object st x in Seg n holds
H1(x) in the carrier of F
proof
let x be object ; :: thesis: ( x in Seg n implies H1(x) in the carrier of F )
assume x in Seg n ; :: thesis: H1(x) in the carrier of F
then Vbf . x in rng Vbf by ;
then consider vv being Element of V such that
A36: Vbf . x = vv ;
L . vv in the carrier of F ;
hence H1(x) in the carrier of F by A36; :: thesis: verum
end;
consider f being Function of (Seg n), the carrier of F such that
A37: for x being object st x in Seg n holds
f . x = H1(x) from 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 ;
then reconsider ff = f as FinSequence of the carrier of F by ;
len ff = n by ;
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 ; :: thesis: verum
end;
for c being object st c in the carrier of (Lin B) holds
ex x being object st
( x in n -tuples_on the carrier of F & c = G . x )
proof
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 ;
then A42: Sum (l (#) Vbf) = Sum l by ;
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
let v be Element of V; :: thesis: l . v = lc . v
now :: thesis: l . v = lc . v
per cases ( v in rng Vbf or not v in rng Vbf ) ;
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 ;
A48: Vbf . x = v by ;
A49: x in dom t by ;
then l . (Vbf . x) = t . x by A43;
hence l . v = lc . v by ; :: thesis: verum
end;
suppose A50: not v in rng Vbf ; :: thesis: l . v = lc . v
now :: thesis: not v in Carrier l
assume A51: v in Carrier l ; :: thesis: contradiction
Carrier l c= rng Vbf by ;
hence contradiction by A50, A51; :: thesis: verum
end;
then A52: l . v = 0. F by VECTSP_6:2;
now :: thesis: not v in Carrier lc
assume A53: v in Carrier lc ; :: thesis: contradiction
Carrier lc c= rng Vbf by ;
hence contradiction by A50, A53; :: thesis: verum
end;
hence l . v = lc . v by ; :: thesis: verum
end;
end;
end;
hence l . v = lc . v ; :: thesis: verum
end;
then G . t = Sum (l (#) Vbf) by ;
hence ex x being object st
( x in n -tuples_on the carrier of F & c = G . x ) by ; :: thesis: verum
end;
then A54: rng G = the carrier of (Lin B) by FUNCT_2:10;
for x1, x2 being object st x1 in dom G & x2 in dom G & G . x1 = G . x2 holds
x1 = x2
proof
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 ;
then A62: Sum L1 = Sum (L1 (#) Vbf) by ;
Carrier L2 c= rng Vbf by ;
then Sum L2 = Sum (L2 (#) Vbf) by ;
then (Sum L1) - (Sum L2) = 0. V by ;
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 ;
for v being Element of V holds L1 . v = L2 . v
proof
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 ;
then 0. F = (L1 . v) - (L2 . v) by VECTSP_6:40;
hence L1 . v = L2 . v by VECTSP_1:27; :: thesis: verum
end;
then A65: L1 = L2 by VECTSP_6:def 7;
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
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 ;
hence t1 . k = t2 . k by A60, A65, A66, A67, A68; :: thesis: verum
end;
hence x1 = x2 by ; :: thesis: verum
end;
then G is one-to-one ;
then n -tuples_on the carrier of F,G .: (n -tuples_on the carrier of F) are_equipotent by ;
then A69: n -tuples_on the carrier of F, the carrier of (Lin B) are_equipotent by ;
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
.= q |^ n by ;
hence card the carrier of V = q |^ n by ; :: thesis: verum
end;
end;
end;
hence card the carrier of V = q |^ n ; :: thesis: verum