let L be non empty addLoopStr ; :: thesis: for p being Element of the carrier of L * holds <*(Sum p)*> = Sum <*p*>
let p be Element of the carrier of L * ; :: thesis: <*(Sum p)*> = Sum <*p*>
A1: dom <*(Sum p)*> = Seg 1 by FINSEQ_1:55
.= dom <*p*> by FINSEQ_1:55 ;
then A2: len <*(Sum p)*> = len <*p*> by FINSEQ_3:31;

now

let i be Nat; :: thesis: ( i in dom <*p*> implies <*(Sum p)*> /. i = Sum (<*p*> /. i) )
assume i in dom <*p*> ; :: thesis: <*(Sum p)*> /. i = Sum (<*p*> /. i)
then i in {1} by FINSEQ_1:4, FINSEQ_1:55;
then A3: i = 1 by TARSKI:def 1;
hence <*(Sum p)*> /. i = Sum p by FINSEQ_4:25
.= Sum (<*p*> /. i) by A3, FINSEQ_4:25 ;
:: thesis: verum

end;

hence <*(Sum p)*> = Sum <*p*> by A1, A2, MATRLIN:def 8; :: thesis: verum