let K be non empty commutative well-unital multLoopStr ; :: thesis: Product (<*> the carrier of K) = 1. K
1. K = 1_ K ;
hence Product (<*> the carrier of K) = 1. K by GROUP_4:8; :: thesis: verum