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

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

assume A1: rng F c= {0.} ; :: thesis: Sum F = 0.

A2: for F being FinSequence of ExtREAL

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

S_{1}[F ^ <*x*>]
_{1}[ <*> ExtREAL]
by EXTREAL1:7;

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

hence Sum F = 0. by A1; :: thesis: verum

defpred S

assume A1: rng F c= {0.} ; :: thesis: Sum F = 0.

A2: for F being FinSequence of ExtREAL

for x being Element of ExtREAL st S

S

proof

A6:
S
let F be FinSequence of ExtREAL ; :: thesis: for x being Element of ExtREAL st S_{1}[F] holds

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

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

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

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

then A4: (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 x in {0.} by ZFMISC_1:31;

then A5: x = 0. by TARSKI:def 1;

thus Sum (F ^ <*x*>) = (Sum F) + x by Lm4

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

end;S

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

assume A3: S

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

then A4: (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 x in {0.} by ZFMISC_1:31;

then A5: x = 0. by TARSKI:def 1;

thus Sum (F ^ <*x*>) = (Sum F) + x by Lm4

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

for F being FinSequence of ExtREAL holds S

hence Sum F = 0. by A1; :: thesis: verum