let X be RealLinearSpace; :: thesis: for F being FinSequence of the carrier of X st rng F c= {(0. X)} holds

Sum F = 0. X

defpred S_{1}[ FinSequence of the carrier of X] means ( rng $1 c= {(0. X)} implies Sum $1 = 0. X );

A1: for F being FinSequence of the carrier of X

for x being Element of X st S_{1}[F] holds

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

assume A5: rng F c= {(0. X)} ; :: thesis: Sum F = 0. X

A6: S_{1}[ <*> the carrier of X]
by RLVECT_1:43;

for F being FinSequence of the carrier of X holds S_{1}[F]
from FINSEQ_2:sch 2(A6, A1);

hence Sum F = 0. X by A5; :: thesis: verum

Sum F = 0. X

defpred S

A1: for F being FinSequence of the carrier of X

for x being Element of X st S

S

proof

let F be FinSequence of the carrier of X; :: thesis: ( rng F c= {(0. X)} implies Sum F = 0. X )
let F be FinSequence of the carrier of X; :: thesis: for x being Element of X st S_{1}[F] holds

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

let x be Element of X; :: thesis: ( S_{1}[F] implies S_{1}[F ^ <*x*>] )

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

assume rng (F ^ <*x*>) c= {(0. X)} ; :: thesis: Sum (F ^ <*x*>) = 0. X

then A3: (rng F) \/ (rng <*x*>) c= {(0. X)} by FINSEQ_1:31;

then rng <*x*> c= {(0. X)} by XBOOLE_1:11;

then {x} c= {(0. X)} by FINSEQ_1:38;

then x in {(0. X)} by ZFMISC_1:31;

then A4: x = 0. X by TARSKI:def 1;

thus Sum (F ^ <*x*>) = (Sum F) + (Sum <*x*>) by RLVECT_1:41

.= (Sum F) + x by RLVECT_1:44

.= 0. X by A2, A3, A4, XBOOLE_1:11 ; :: thesis: verum

end;S

let x be Element of X; :: thesis: ( S

assume A2: S

assume rng (F ^ <*x*>) c= {(0. X)} ; :: thesis: Sum (F ^ <*x*>) = 0. X

then A3: (rng F) \/ (rng <*x*>) c= {(0. X)} by FINSEQ_1:31;

then rng <*x*> c= {(0. X)} by XBOOLE_1:11;

then {x} c= {(0. X)} by FINSEQ_1:38;

then x in {(0. X)} by ZFMISC_1:31;

then A4: x = 0. X by TARSKI:def 1;

thus Sum (F ^ <*x*>) = (Sum F) + (Sum <*x*>) by RLVECT_1:41

.= (Sum F) + x by RLVECT_1:44

.= 0. X by A2, A3, A4, XBOOLE_1:11 ; :: thesis: verum

assume A5: rng F c= {(0. X)} ; :: thesis: Sum F = 0. X

A6: S

for F being FinSequence of the carrier of X holds S

hence Sum F = 0. X by A5; :: thesis: verum