let sq be FinSequence of REAL ; :: thesis: ( len sq > 0 implies Sum sq = (sq . 1) + (Sum (sq /^ 1)) )
assume A1: len sq > 0 ; :: thesis: Sum sq = (sq . 1) + (Sum (sq /^ 1))
then 0 + 1 <= len sq by NAT_1:13;
then A2: 1 in dom sq by FINSEQ_3:25;
thus Sum sq = Sum (<*(sq /. 1)*> ^ (sq /^ 1)) by A1, CARD_1:27, FINSEQ_5:29
.= Sum (<*(sq . 1)*> ^ (sq /^ 1)) by A2, PARTFUN1:def 6
.= (sq . 1) + (Sum (sq /^ 1)) by RVSUM_1:76 ; :: thesis: verum