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

for A being Subset of G

for H being Subgroup of G holds

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

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

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

for H being Subgroup of G holds

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

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

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

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

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

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

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

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

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

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

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

g2 in carr H by A4;

hence x in A * H by A3; :: thesis: verum

for A being Subset of G

for H being Subgroup of G holds

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

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

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

for H being Subgroup of G holds

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

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

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

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

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

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

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

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

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

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

proof

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

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

then consider g1, g2 being Element of G such that

A1: ( x = g1 * g2 & g1 in A ) and

A2: g2 in carr H ;

g2 in H by A2;

hence ex g1, g2 being Element of G st

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

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

then consider g1, g2 being Element of G such that

A1: ( x = g1 * g2 & g1 in A ) and

A2: g2 in carr H ;

g2 in H by A2;

hence ex g1, g2 being Element of G st

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

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

g2 in carr H by A4;

hence x in A * H by A3; :: thesis: verum