let F be FinSequence of REAL ; :: thesis: ( rng F c= {0} implies Sum F = 0 )

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

A1: for F being FinSequence of REAL

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

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

A6: S_{1}[ <*> REAL]
by RVSUM_1:72;

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

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

defpred S

A1: for F being FinSequence of REAL

for x being Element of REAL st S

S

proof

assume A5:
rng F c= {0}
; :: thesis: Sum F = 0
let F be FinSequence of REAL ; :: thesis: for x being Element of REAL st S_{1}[F] holds

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

let x be Element of REAL ; :: 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} ; :: thesis: Sum (F ^ <*x*>) = 0

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

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

then {x} c= {0} by FINSEQ_1:38;

then A4: x in {0} by ZFMISC_1:31;

thus Sum (F ^ <*x*>) = (Sum F) + x by RVSUM_1:74

.= 0 by A2, A3, A4, TARSKI:def 1, XBOOLE_1:11 ; :: thesis: verum

end;S

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

assume A2: S

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

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

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

then {x} c= {0} by FINSEQ_1:38;

then A4: x in {0} by ZFMISC_1:31;

thus Sum (F ^ <*x*>) = (Sum F) + x by RVSUM_1:74

.= 0 by A2, A3, A4, TARSKI:def 1, XBOOLE_1:11 ; :: thesis: verum

A6: S

for F being FinSequence of REAL holds S

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