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 )
proof
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;
given a being Element of G such that A5: z = (x * a) * y and
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