let x be set ; :: thesis: for G being Group
for g being Element of G
for A being Subset of G holds
( x in g |^ A iff ex h being Element of G st
( x = g |^ h & h in A ) )
let G be Group; :: thesis: for g being Element of G
for A being Subset 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: for A being Subset 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: ( 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 a, b being Element of G such that
A1: x = a |^ b and
A2: a in {g} and
A3: b in A ;
a = 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;

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