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

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