let L be non empty addLoopStr ; :: thesis: for F being FinSequence of the carrier of L * holds Sum (<*> ( the carrier of L *)) = <*> the carrier of L
let F be FinSequence of the carrier of L * ; :: thesis: Sum (<*> ( the carrier of L *)) = <*> the carrier of L
dom (Sum (<*> ( the carrier of L *))) = dom (<*> ( the carrier of L *)) by Th2;
hence Sum (<*> ( the carrier of L *)) = <*> the carrier of L ; :: thesis: verum