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 S1[ 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 S1[F] holds
S1[F ^ <*x*>]
proof
let F be FinSequence of the carrier of X; :: thesis: for x being Element of X st S1[F] holds
S1[F ^ <*x*>]

let x be Element of X; :: thesis: ( S1[F] implies S1[F ^ <*x*>] )
assume A2: S1[F] ; :: thesis: S1[F ^ <*x*>]
assume rng (F ^ <*x*>) c= {(0. X)} ; :: thesis: Sum (F ^ <*x*>) = 0. X
then A3: (rng F) \/ () 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) + () by RLVECT_1:41
.= (Sum F) + x by RLVECT_1:44
.= 0. X by ; :: 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: S1[ <*> the carrier of X] by RLVECT_1:43;
for F being FinSequence of the carrier of X holds S1[F] from hence Sum F = 0. X by A5; :: thesis: verum