let V be RealLinearSpace; :: thesis: for L being Linear_Combination of V

for F being FinSequence of the carrier of V st Carrier L misses rng F holds

Sum (L (#) F) = 0. V

let L be Linear_Combination of V; :: thesis: for F being FinSequence of the carrier of V st Carrier L misses rng F holds

Sum (L (#) F) = 0. V

defpred S_{1}[ FinSequence] means for G being FinSequence of the carrier of V st G = $1 & Carrier L misses rng G holds

Sum (L (#) G) = 0. V;

A1: for p being FinSequence

for x being object st S_{1}[p] holds

S_{1}[p ^ <*x*>]
_{1}[ {} ]
_{1}[p]
from FINSEQ_1:sch 3(A10, A1);

let F be FinSequence of the carrier of V; :: thesis: ( Carrier L misses rng F implies Sum (L (#) F) = 0. V )

assume Carrier L misses rng F ; :: thesis: Sum (L (#) F) = 0. V

hence Sum (L (#) F) = 0. V by A12; :: thesis: verum

for F being FinSequence of the carrier of V st Carrier L misses rng F holds

Sum (L (#) F) = 0. V

let L be Linear_Combination of V; :: thesis: for F being FinSequence of the carrier of V st Carrier L misses rng F holds

Sum (L (#) F) = 0. V

defpred S

Sum (L (#) G) = 0. V;

A1: for p being FinSequence

for x being object st S

S

proof

A10:
S
let p be FinSequence; :: thesis: for x being object st S_{1}[p] holds

S_{1}[p ^ <*x*>]

let x be object ; :: thesis: ( S_{1}[p] implies S_{1}[p ^ <*x*>] )

assume A2: S_{1}[p]
; :: thesis: S_{1}[p ^ <*x*>]

let G be FinSequence of the carrier of V; :: thesis: ( G = p ^ <*x*> & Carrier L misses rng G implies Sum (L (#) G) = 0. V )

assume A3: G = p ^ <*x*> ; :: thesis: ( not Carrier L misses rng G or Sum (L (#) G) = 0. V )

then reconsider p = p, x9 = <*x*> as FinSequence of the carrier of V by FINSEQ_1:36;

x in {x} by TARSKI:def 1;

then A4: x in rng x9 by FINSEQ_1:38;

rng x9 c= the carrier of V by FINSEQ_1:def 4;

then reconsider x = x as VECTOR of V by A4;

assume Carrier L misses rng G ; :: thesis: Sum (L (#) G) = 0. V

then A5: {} = (Carrier L) /\ (rng G) by XBOOLE_0:def 7

.= (Carrier L) /\ ((rng p) \/ (rng <*x*>)) by A3, FINSEQ_1:31

.= (Carrier L) /\ ((rng p) \/ {x}) by FINSEQ_1:38

.= ((Carrier L) /\ (rng p)) \/ ((Carrier L) /\ {x}) by XBOOLE_1:23 ;

then (Carrier L) /\ (rng p) = {} ;

then Carrier L misses rng p by XBOOLE_0:def 7;

then A6: Sum (L (#) p) = 0. V by A2;

A7: (Carrier L) /\ {x} = {} by A5;

Sum (L (#) G) = Sum ((L (#) p) ^ (L (#) x9)) by A3, RLVECT_3:34

.= (Sum (L (#) p)) + (Sum (L (#) x9)) by RLVECT_1:41

.= (0. V) + (Sum <*((L . x) * x)*>) by A6, RLVECT_2:26

.= Sum <*((L . x) * x)*> by RLVECT_1:4

.= 0 * x by A9, RLVECT_1:44

.= 0. V by RLVECT_1:10 ;

hence Sum (L (#) G) = 0. V ; :: thesis: verum

end;S

let x be object ; :: thesis: ( S

assume A2: S

let G be FinSequence of the carrier of V; :: thesis: ( G = p ^ <*x*> & Carrier L misses rng G implies Sum (L (#) G) = 0. V )

assume A3: G = p ^ <*x*> ; :: thesis: ( not Carrier L misses rng G or Sum (L (#) G) = 0. V )

then reconsider p = p, x9 = <*x*> as FinSequence of the carrier of V by FINSEQ_1:36;

x in {x} by TARSKI:def 1;

then A4: x in rng x9 by FINSEQ_1:38;

rng x9 c= the carrier of V by FINSEQ_1:def 4;

then reconsider x = x as VECTOR of V by A4;

assume Carrier L misses rng G ; :: thesis: Sum (L (#) G) = 0. V

then A5: {} = (Carrier L) /\ (rng G) by XBOOLE_0:def 7

.= (Carrier L) /\ ((rng p) \/ (rng <*x*>)) by A3, FINSEQ_1:31

.= (Carrier L) /\ ((rng p) \/ {x}) by FINSEQ_1:38

.= ((Carrier L) /\ (rng p)) \/ ((Carrier L) /\ {x}) by XBOOLE_1:23 ;

then (Carrier L) /\ (rng p) = {} ;

then Carrier L misses rng p by XBOOLE_0:def 7;

then A6: Sum (L (#) p) = 0. V by A2;

A7: (Carrier L) /\ {x} = {} by A5;

now :: thesis: not x in Carrier L

then A9:
L . x = 0
by RLVECT_2:19;A8:
x in {x}
by TARSKI:def 1;

assume x in Carrier L ; :: thesis: contradiction

hence contradiction by A7, A8, XBOOLE_0:def 4; :: thesis: verum

end;assume x in Carrier L ; :: thesis: contradiction

hence contradiction by A7, A8, XBOOLE_0:def 4; :: thesis: verum

Sum (L (#) G) = Sum ((L (#) p) ^ (L (#) x9)) by A3, RLVECT_3:34

.= (Sum (L (#) p)) + (Sum (L (#) x9)) by RLVECT_1:41

.= (0. V) + (Sum <*((L . x) * x)*>) by A6, RLVECT_2:26

.= Sum <*((L . x) * x)*> by RLVECT_1:4

.= 0 * x by A9, RLVECT_1:44

.= 0. V by RLVECT_1:10 ;

hence Sum (L (#) G) = 0. V ; :: thesis: verum

proof

A12:
for p being FinSequence holds S
let G be FinSequence of the carrier of V; :: thesis: ( G = {} & Carrier L misses rng G implies Sum (L (#) G) = 0. V )

assume G = {} ; :: thesis: ( not Carrier L misses rng G or Sum (L (#) G) = 0. V )

then A11: L (#) G = <*> the carrier of V by RLVECT_2:25;

assume Carrier L misses rng G ; :: thesis: Sum (L (#) G) = 0. V

thus Sum (L (#) G) = 0. V by A11, RLVECT_1:43; :: thesis: verum

end;assume G = {} ; :: thesis: ( not Carrier L misses rng G or Sum (L (#) G) = 0. V )

then A11: L (#) G = <*> the carrier of V by RLVECT_2:25;

assume Carrier L misses rng G ; :: thesis: Sum (L (#) G) = 0. V

thus Sum (L (#) G) = 0. V by A11, RLVECT_1:43; :: thesis: verum

let F be FinSequence of the carrier of V; :: thesis: ( Carrier L misses rng F implies Sum (L (#) F) = 0. V )

assume Carrier L misses rng F ; :: thesis: Sum (L (#) F) = 0. V

hence Sum (L (#) F) = 0. V by A12; :: thesis: verum