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: now :: thesis: for i being Nat st i in dom <*p*> holds
<*(Sum p)*> /. i = Sum (<*p*> /. i)

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:2, FINSEQ_1:38;
then A2: i = 1 by TARSKI:def 1;
hence <*(Sum p)*> /. i = Sum p by FINSEQ_4:16
.= Sum (<*p*> /. i) by A2, FINSEQ_4:16 ;
:: thesis: verum

end;

A3: dom <*(Sum p)*> = Seg 1 by FINSEQ_1:38
.= dom <*p*> by FINSEQ_1:38 ;
then len <*(Sum p)*> = len <*p*> by FINSEQ_3:29;
hence <*(Sum p)*> = Sum <*p*> by A3, A1, MATRLIN:def 6; :: thesis: verum