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

for A being Subset of G

for H being Subgroup of G holds

( x in H * A iff ex g1, g2 being Element of G st

( x = g1 * g2 & g1 in H & g2 in A ) )

let G be Group; :: thesis: for A being Subset of G

for H being Subgroup of G holds

( x in H * A iff ex g1, g2 being Element of G st

( x = g1 * g2 & g1 in H & g2 in A ) )

let A be Subset of G; :: thesis: for H being Subgroup of G holds

( x in H * A iff ex g1, g2 being Element of G st

( x = g1 * g2 & g1 in H & g2 in A ) )

let H be Subgroup of G; :: thesis: ( x in H * A iff ex g1, g2 being Element of G st

( x = g1 * g2 & g1 in H & g2 in A ) )

thus ( x in H * A implies ex g1, g2 being Element of G st

( x = g1 * g2 & g1 in H & g2 in A ) ) :: thesis: ( ex g1, g2 being Element of G st

( x = g1 * g2 & g1 in H & g2 in A ) implies x in H * A )

A5: g1 in H and

A6: g2 in A ; :: thesis: x in H * A

g1 in carr H by A5;

hence x in H * A by A4, A6; :: thesis: verum

for A being Subset of G

for H being Subgroup of G holds

( x in H * A iff ex g1, g2 being Element of G st

( x = g1 * g2 & g1 in H & g2 in A ) )

let G be Group; :: thesis: for A being Subset of G

for H being Subgroup of G holds

( x in H * A iff ex g1, g2 being Element of G st

( x = g1 * g2 & g1 in H & g2 in A ) )

let A be Subset of G; :: thesis: for H being Subgroup of G holds

( x in H * A iff ex g1, g2 being Element of G st

( x = g1 * g2 & g1 in H & g2 in A ) )

let H be Subgroup of G; :: thesis: ( x in H * A iff ex g1, g2 being Element of G st

( x = g1 * g2 & g1 in H & g2 in A ) )

thus ( x in H * A implies ex g1, g2 being Element of G st

( x = g1 * g2 & g1 in H & g2 in A ) ) :: thesis: ( ex g1, g2 being Element of G st

( x = g1 * g2 & g1 in H & g2 in A ) implies x in H * A )

proof

given g1, g2 being Element of G such that A4:
x = g1 * g2
and
assume
x in H * A
; :: thesis: ex g1, g2 being Element of G st

( x = g1 * g2 & g1 in H & g2 in A )

then consider g1, g2 being Element of G such that

A1: x = g1 * g2 and

A2: g1 in carr H and

A3: g2 in A ;

g1 in H by A2;

hence ex g1, g2 being Element of G st

( x = g1 * g2 & g1 in H & g2 in A ) by A1, A3; :: thesis: verum

end;( x = g1 * g2 & g1 in H & g2 in A )

then consider g1, g2 being Element of G such that

A1: x = g1 * g2 and

A2: g1 in carr H and

A3: g2 in A ;

g1 in H by A2;

hence ex g1, g2 being Element of G st

( x = g1 * g2 & g1 in H & g2 in A ) by A1, A3; :: thesis: verum

A5: g1 in H and

A6: g2 in A ; :: thesis: x in H * A

g1 in carr H by A5;

hence x in H * A by A4, A6; :: thesis: verum