set B = Base (R,n);
set V = R ^* n;
now for l being Linear_Combination of Base (R,n) st Carrier l <> {} holds
Sum l <> 0. (R ^* n)let l be
Linear_Combination of
Base (
R,
n);
( Carrier l <> {} implies Sum l <> 0. (R ^* n) )assume A0:
Carrier l <> {}
;
Sum l <> 0. (R ^* n)set o = the
Element of
Carrier l;
A1:
( the
Element of
Carrier l in Carrier l &
Carrier l c= Base (
R,
n) )
by A0, VECTSP_6:def 4;
then
the
Element of
Carrier l in Base (
R,
n)
;
then consider i being
Nat such that A2:
( the
Element of
Carrier l = i _th_unit_vector (
n,
R) & 1
<= i &
i <= n )
;
consider v being
Element of
(R ^* n) such that A3:
( the
Element of
Carrier l = v &
l . v <> 0. R )
by A1;
Sum l in the
carrier of
(R ^* n)
;
then
Sum l in n -tuples_on the
carrier of
R
by DEF;
then reconsider w =
Sum l as
Tuple of
n, the
carrier of
R by FINSEQ_2:131;
A4:
w . i <> 0. R
by A3, A2, lemBase;
(n |-> (0. R)) . i =
((Seg n) --> (0. R)) . i
by FINSEQ_2:def 2
.=
0. R
by A2, FINSEQ_1:1, FUNCOP_1:7
;
hence
Sum l <> 0. (R ^* n)
by A4, DEF;
verum end;
then
for l being Linear_Combination of Base (R,n) st Sum l = 0. (R ^* n) holds
Carrier l = {}
;
hence
Base (R,n) is linearly-independent
by VECTSP_7:def 1; verum