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 Th15;
hence Sum (<*> (the carrier of L * )) = <*> the carrier of L ; :: thesis: verum