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

proof

assume x in H |^ a ; :: thesis: ex g being Element of G st
( x = g |^ a & g in H )
then x in the carrier of (H |^ a) by STRUCT_0:def 5;
then x in (carr H) |^ a by Def6;
then consider b being Element of G such that
A1: ( x = b |^ a & b in carr H ) by Th50;
take b ; :: thesis: ( x = b |^ a & b in H )
thus ( x = b |^ a & b in H ) by A1, STRUCT_0:def 5; :: thesis: verum

end;

given g being Element of G such that A2: x = g |^ a and
A3: g in H ; :: thesis: x in H |^ a
g in carr H by A3, STRUCT_0:def 5;
then x in (carr H) |^ a by A2, Th50;
then x in the carrier of (H |^ a) by Def6;
hence x in H |^ a by STRUCT_0:def 5; :: thesis: verum