let F be FinSequence of REAL ; :: thesis: ( rng F c= {0} implies Sum F = 0 )
defpred S₁[ 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₁[F] holds
S₁[F ^ <*x*>]

proof

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

assume A5: rng F c= {0} ; :: thesis: Sum F = 0
A6: S₁[ <*> REAL] by RVSUM_1:72;
for F being FinSequence of REAL holds S₁[F] from FINSEQ_2:sch 2(A6, A1);
hence Sum F = 0 by A5; :: thesis: verum