let V be non empty right_complementable add-associative right_zeroed addLoopStr ; :: thesis: for F being FinSequence of the carrier of V st len F = 1 holds
Sum F = F . 1
let F be FinSequence of the carrier of V; :: thesis: ( len F = 1 implies Sum F = F . 1 )
assume A1: len F = 1 ; :: thesis: Sum F = F . 1
then dom F = {1} by FINSEQ_1:4, FINSEQ_1:def 3;
then 1 in dom F by TARSKI:def 1;
then ( F . 1 in rng F & rng F c= the carrier of V ) by FINSEQ_1:def 4, FUNCT_1:def 5;
then reconsider v = F . 1 as Element of V ;
F = <*v*> by A1, FINSEQ_1:57;
hence Sum F = F . 1 by Lm6; :: thesis: verum