let G be Group; :: thesis: for x, y, z being Element of G

for A being Subset of G holds

( z in (x * A) * y iff ex a being Element of G st

( z = (x * a) * y & a in A ) )

let x, y, z be Element of G; :: thesis: for A being Subset of G holds

( z in (x * A) * y iff ex a being Element of G st

( z = (x * a) * y & a in A ) )

let A be Subset of G; :: thesis: ( z in (x * A) * y iff ex a being Element of G st

( z = (x * a) * y & a in A ) )

thus ( z in (x * A) * y implies ex a being Element of G st

( z = (x * a) * y & a in A ) ) :: thesis: ( ex a being Element of G st

( z = (x * a) * y & a in A ) implies z in (x * A) * y )

A6: a in A ; :: thesis: z in (x * A) * y

ex h being Element of G st

( z = h * y & h in x * A ) by A5, A6, GROUP_2:27;

hence z in (x * A) * y by GROUP_2:28; :: thesis: verum

for A being Subset of G holds

( z in (x * A) * y iff ex a being Element of G st

( z = (x * a) * y & a in A ) )

let x, y, z be Element of G; :: thesis: for A being Subset of G holds

( z in (x * A) * y iff ex a being Element of G st

( z = (x * a) * y & a in A ) )

let A be Subset of G; :: thesis: ( z in (x * A) * y iff ex a being Element of G st

( z = (x * a) * y & a in A ) )

thus ( z in (x * A) * y implies ex a being Element of G st

( z = (x * a) * y & a in A ) ) :: thesis: ( ex a being Element of G st

( z = (x * a) * y & a in A ) implies z in (x * A) * y )

proof

given a being Element of G such that A5:
z = (x * a) * y
and
assume
z in (x * A) * y
; :: thesis: ex a being Element of G st

( z = (x * a) * y & a in A )

then consider b being Element of G such that

A1: z = b * y and

A2: b in x * A by GROUP_2:28;

consider u being Element of G such that

A3: b = x * u and

A4: u in A by A2, GROUP_2:27;

take u ; :: thesis: ( z = (x * u) * y & u in A )

thus ( z = (x * u) * y & u in A ) by A1, A3, A4; :: thesis: verum

end;( z = (x * a) * y & a in A )

then consider b being Element of G such that

A1: z = b * y and

A2: b in x * A by GROUP_2:28;

consider u being Element of G such that

A3: b = x * u and

A4: u in A by A2, GROUP_2:27;

take u ; :: thesis: ( z = (x * u) * y & u in A )

thus ( z = (x * u) * y & u in A ) by A1, A3, A4; :: thesis: verum

A6: a in A ; :: thesis: z in (x * A) * y

ex h being Element of G st

( z = h * y & h in x * A ) by A5, A6, GROUP_2:27;

hence z in (x * A) * y by GROUP_2:28; :: thesis: verum