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
(A * g) * h = A * (g * h)
let A be Subset of G; :: thesis: for g, h being Element of G st G is associative holds
(A * g) * h = A * (g * h)
let g, h be Element of G; :: thesis: ( G is associative implies (A * g) * h = A * (g * h) )
assume G is associative ; :: thesis: (A * g) * h = A * (g * h)
hence (A * g) * h = A * ({g} * {h}) by Th10
.= A * (g * h) by Th18 ;
:: thesis: verum