let x be object ; :: thesis: for G being non empty multMagma
for A being Subset of G
for g being Element of G holds
( x in A * g iff ex h being Element of G st
( x = h * g & h in A ) )

let G be non empty multMagma ; :: thesis: for A being Subset of G
for g being Element of G holds
( x in A * g iff ex h being Element of G st
( x = h * g & h in A ) )

let A be Subset of G; :: thesis: for g being Element of G holds
( x in A * g iff ex h being Element of G st
( x = h * g & h in A ) )

let g be Element of G; :: thesis: ( x in A * g iff ex h being Element of G st
( x = h * g & h in A ) )

thus ( x in A * g implies ex h being Element of G st
( x = h * g & h in A ) ) :: thesis: ( ex h being Element of G st
( x = h * g & h in A ) implies x in A * g )
proof
assume x in A * g ; :: thesis: ex h being Element of G st
( x = h * g & h in A )

then consider g1, g2 being Element of G such that
A1: ( x = g1 * g2 & g1 in A ) and
A2: g2 in {g} ;
g2 = g by ;
hence ex h being Element of G st
( x = h * g & h in A ) by A1; :: thesis: verum
end;
given h being Element of G such that A3: ( x = h * g & h in A ) ; :: thesis: x in A * g
g in {g} by TARSKI:def 1;
hence x in A * g by A3; :: thesis: verum