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 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 )

g in {g} by TARSKI:def 1;

hence x in g * A by A4; :: thesis: verum

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

given h being Element of G such that A4:
( x = g * h & h in A )
; :: thesis: x in g * A
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 and

A2: g1 in {g} and

A3: g2 in A ;

g1 = g by A2, TARSKI:def 1;

hence ex h being Element of G st

( x = g * h & h in A ) by A1, A3; :: thesis: verum

end;( x = g * h & h in A )

then consider g1, g2 being Element of G such that

A1: x = g1 * g2 and

A2: g1 in {g} and

A3: g2 in A ;

g1 = g by A2, TARSKI:def 1;

hence ex h being Element of G st

( x = g * h & h in A ) by A1, A3; :: thesis: verum

g in {g} by TARSKI:def 1;

hence x in g * A by A4; :: thesis: verum