let L be non empty addLoopStr ; :: thesis: for F being FinSequence of the carrier of L * holds dom (Sum F) = dom F
let F be FinSequence of the carrier of L * ; :: thesis: dom (Sum F) = dom F
len (Sum F) = len F by MATRLIN:def 6;
hence dom (Sum F) = dom F by FINSEQ_3:29; :: thesis: verum