let x be set ; :: thesis: for G being non empty multMagma
for A being Subset of G
for g being Element of G holds
( x in g * A iff ex h being Element of G st
( x = g * h & 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 g * A iff ex h being Element of G st
( x = g * h & h in A ) )
let A be Subset of G; :: thesis: for g being Element of G holds
( x in g * A iff ex h being Element of G st
( x = g * h & h in A ) )
let g be Element of G; :: thesis: ( x in g * A iff ex h being Element of G st
( x = g * h & h in A ) )
thus ( x in g * A implies ex h being Element of G st
( x = g * h & h in A ) ) :: thesis: ( ex h being Element of G st
( x = g * h & h in A ) implies x in g * A )

proof

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

end;

given h being Element of G such that A2: ( x = g * h & h in A ) ; :: thesis: x in g * A
g in {g} by TARSKI:def 1;
hence x in g * A by A2; :: thesis: verum