let L be non empty multMagma ; :: thesis: for a being Element of L holds (<*> the carrier of L) * a = <*> the carrier of L
let a be Element of L; :: thesis: (<*> the carrier of L) * a = <*> the carrier of L
dom ((<*> the carrier of L) * a) = dom (<*> the carrier of L) by Def2;
hence (<*> the carrier of L) * a = <*> the carrier of L ; :: thesis: verum