let x be object ; :: thesis: for G being Group

for a being Element of G

for H being Subgroup of G holds

( x in a * H iff ex g being Element of G st

( x = a * g & g in H ) )

let G be Group; :: thesis: for a being Element of G

for H being Subgroup of G holds

( x in a * H iff ex g being Element of G st

( x = a * g & g in H ) )

let a be Element of G; :: thesis: for H being Subgroup of G holds

( x in a * H iff ex g being Element of G st

( x = a * g & g in H ) )

let H be Subgroup of G; :: thesis: ( x in a * H iff ex g being Element of G st

( x = a * g & g in H ) )

thus ( x in a * H implies ex g being Element of G st

( x = a * g & g in H ) ) :: thesis: ( ex g being Element of G st

( x = a * g & g in H ) implies x in a * H )

A3: g in H ; :: thesis: x in a * H

g in carr H by A3;

hence x in a * H by A2, Th27; :: thesis: verum

for a being Element of G

for H being Subgroup of G holds

( x in a * H iff ex g being Element of G st

( x = a * g & g in H ) )

let G be Group; :: thesis: for a being Element of G

for H being Subgroup of G holds

( x in a * H iff ex g being Element of G st

( x = a * g & g in H ) )

let a be Element of G; :: thesis: for H being Subgroup of G holds

( x in a * H iff ex g being Element of G st

( x = a * g & g in H ) )

let H be Subgroup of G; :: thesis: ( x in a * H iff ex g being Element of G st

( x = a * g & g in H ) )

thus ( x in a * H implies ex g being Element of G st

( x = a * g & g in H ) ) :: thesis: ( ex g being Element of G st

( x = a * g & g in H ) implies x in a * H )

proof

given g being Element of G such that A2:
x = a * g
and
assume
x in a * H
; :: thesis: ex g being Element of G st

( x = a * g & g in H )

then consider g being Element of G such that

A1: ( x = a * g & g in carr H ) by Th27;

take g ; :: thesis: ( x = a * g & g in H )

thus ( x = a * g & g in H ) by A1; :: thesis: verum

end;( x = a * g & g in H )

then consider g being Element of G such that

A1: ( x = a * g & g in carr H ) by Th27;

take g ; :: thesis: ( x = a * g & g in H )

thus ( x = a * g & g in H ) by A1; :: thesis: verum

A3: g in H ; :: thesis: x in a * H

g in carr H by A3;

hence x in a * H by A2, Th27; :: thesis: verum