let x be set ; :: thesis: for G being Group
for g being Element of
for A being Subset of holds
( x in A |^ g iff ex h being Element of st
( x = h |^ g & h in A ) )
let G be Group; :: thesis: for g being Element of
for A being Subset of holds
( x in A |^ g iff ex h being Element of st
( x = h |^ g & h in A ) )
let g be Element of ; :: thesis: for A being Subset of holds
( x in A |^ g iff ex h being Element of st
( x = h |^ g & h in A ) )
let A be Subset of ; :: thesis: ( x in A |^ g iff ex h being Element of st
( x = h |^ g & h in A ) )
thus ( x in A |^ g implies ex h being Element of st
( x = h |^ g & h in A ) ) :: thesis: ( ex h being Element of st
( x = h |^ g & h in A ) implies x in A |^ g )

proof

assume x in A |^ g ; :: thesis: ex h being Element of st
( x = h |^ g & h in A )
then consider a, b being Element of such that
A1: ( x = a |^ b & a in A ) and
A2: b in {g} ;
b = g by A2, TARSKI:def 1;
hence ex h being Element of st
( x = h |^ g & h in A ) by A1; :: thesis: verum

end;

given h being Element of 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