let V be non empty right_complementable add-associative right_zeroed addLoopStr ; :: thesis: for F being FinSequence of V st len F = 1 holds
Sum F = F . 1
let F be FinSequence 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:2, FINSEQ_1:def 3;
then 1 in dom F by TARSKI:def 1;
then A2: F . 1 in rng F by FUNCT_1:def 3;
rng F c= the carrier of V by FINSEQ_1:def 4;
then reconsider v = F . 1 as Element of V by A2;
F = <*v*> by A1, FINSEQ_1:40;
hence Sum F = F . 1 by Lm6; :: thesis: verum