let Bn be Subset of (REAL-US n); ( Bn is R-orthonormal implies Bn is linearly-independent )
assume A1:
Bn is R-orthonormal
; Bn is linearly-independent
let l be Linear_Combination of Bn; RLVECT_3:def 1 ( not Sum l = 0. (REAL-US n) or Carrier l = {} )
assume A2:
Sum l = 0. (REAL-US n)
; Carrier l = {}
set v0 = the Element of Carrier l;
consider F being FinSequence of the carrier of (REAL-US n) such that
A3:
F is one-to-one
and
A4:
rng F = Carrier l
and
A5:
Sum l = Sum (l (#) F)
by RLVECT_2:def 8;
assume A6:
Carrier l <> {}
; contradiction
then A7:
the Element of Carrier l in Carrier l
;
then
the Element of Carrier l in { v2 where v2 is Element of (REAL-US n) : l . v2 <> 0 }
by RLVECT_2:def 4;
then consider v being Element of (REAL-US n) such that
A8:
the Element of Carrier l = v
and
l . v <> 0
;
reconsider xv = v as Element of REAL n by REAL_NS1:def 6;
0. (REAL-US n) = 0* n
by REAL_NS1:def 6;
then A9: (Euclid_scalar n) . (v,(Sum (l (#) F))) =
|(xv,(0* n))|
by A2, A5, REAL_NS1:def 5
.=
0
by EUCLID_4:18
;
consider x0 being object such that
A10:
x0 in dom F
and
A11:
the Element of Carrier l = F . x0
by A6, A4, FUNCT_1:def 3;
reconsider nx0 = x0 as Element of NAT by A10;
F . x0 = F /. x0
by A10, PARTFUN1:def 6;
then
F /. nx0 in rng F
by A10, FUNCT_1:def 3;
then
F /. nx0 in { v3 where v3 is Element of (REAL-US n) : l . v3 <> 0 }
by A4, RLVECT_2:def 4;
then A12:
ex v3 being Element of (REAL-US n) st
( v3 = F /. nx0 & l . v3 <> 0 )
;
A13:
dom F = Seg (len F)
by FINSEQ_1:def 3;
A14:
Carrier l c= Bn
by RLVECT_2:def 6;
len (l (#) F) = len F
by RLVECT_2:def 7;
then
nx0 in dom (l (#) F)
by A10, A13, FINSEQ_1:def 3;
then (Euclid_scalar n) . (v,(Sum (l (#) F))) =
(Euclid_scalar n) . (v,((l . (F /. nx0)) * v))
by A1, A14, A7, A8, A3, A4, A11, Th32
.=
|(xv,((l . (F /. nx0)) * xv))|
by REAL_NS1:def 5
.=
(l . (F /. nx0)) * |(xv,xv)|
by EUCLID_4:22
.=
(l . (F /. nx0)) * (|.xv.| ^2)
by EUCLID_2:4
.=
(l . (F /. nx0)) * (1 ^2)
by A1, A14, A7, A8, Def4
.=
l . (F /. nx0)
;
hence
contradiction
by A12, A9; verum