let x be object ; :: 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 consider g being Element of G such that
A1: ( x = g * a & g in carr H ) by Th28;
take g ; :: thesis: ( x = g * a & g in H )
thus ( x = g * a & g in H ) by A1; :: 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;
hence x in H * a by ; :: thesis: verum