per cases ( f is empty or not f is empty ) ;

suppose f is empty ; :: thesis: Sum f is zero

then f = <*> the carrier of R ;
hence Sum f is zero by RLVECT_1:43; :: thesis: verum

end;

suppose not f is empty ; :: thesis: Sum f is zero

then H: Seg 1 c= Seg (len f) by FINSEQ_1:20, FINSEQ_1:5;
( Seg 1 = {1} & 1 in {1} ) by FINSEQ_1:2, TARSKI:def 1;
then 1 in Seg (len f) by H;
then A: 1 in dom f by FINSEQ_1:def 3;
then B: f /. 1 = f . 1 by PARTFUN1:def 6;

now :: thesis: for i being Element of NAT st i in dom f & i <> 1 holds
f /. i = 0. R

let i be Element of NAT ; :: thesis: ( i in dom f & i <> 1 implies f /. i = 0. R )
assume C: ( i in dom f & i <> 1 ) ; :: thesis: f /. i = 0. R
then f /. i = f . i by PARTFUN1:def 6;
hence f /. i = 0. R by C, REALALG2:def 4; :: thesis: verum

end;

then Sum f = f /. 1 by A, POLYNOM2:3
.= 0. R by A, B, REALALG2:def 4 ;
hence Sum f is zero ; :: thesis: verum

end;

end;