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