for L being non empty unital multMagma holds FPower ((1_ L),1) = id the carrier of L