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

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