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₁[ 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₁[F] holds
S₁[F ^ <*x*>]

proof

let F be FinSequence of the carrier of X; :: thesis: for x being Element of X st S₁[F] holds
S₁[F ^ <*x*>]
let x be Element of X; :: thesis: ( S₁[F] implies S₁[F ^ <*x*>] )
assume A2: S₁[F] ; :: thesis: S₁[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;

let F be FinSequence of the carrier of X; :: thesis: ( rng F c= {(0. X)} implies Sum F = 0. X )
assume A5: rng F c= {(0. X)} ; :: thesis: Sum F = 0. X
A6: S₁[ <*> the carrier of X] by RLVECT_1:43;
for F being FinSequence of the carrier of X holds S₁[F] from FINSEQ_2:sch 2(A6, A1);
hence Sum F = 0. X by A5; :: thesis: verum