let G be non empty multMagma ; :: thesis: for A being Subset of G
for g, h being Element of G st G is associative holds
(g * h) * A = g * (h * A)
let A be Subset of G; :: thesis: for g, h being Element of G st G is associative holds
(g * h) * A = g * (h * A)
let g, h be Element of G; :: thesis: ( G is associative implies (g * h) * A = g * (h * A) )
assume A1: G is associative ; :: thesis: (g * h) * A = g * (h * A)
thus (g * h) * A = ({g} * {h}) * A by Th18
.= g * (h * A) by A1, Th10 ; :: thesis: verum