let G be non empty unital multMagma ; :: thesis: Product (<*> the carrier of G) = 1_ G
set g = the multF of G;
( len (<*> the carrier of G) = 0 & the multF of G is having_a_unity ) ;
hence Product (<*> the carrier of G) = the_unity_wrt the multF of G by FINSOP_1:def 1
.= 1_ G by GROUP_1:22 ;
:: thesis: verum