let x be set ; :: 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 )

proof

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 & g1 in carr H & g2 in A ) ;
g1 in H by A1, STRUCT_0:def 5;
hence ex g1, g2 being Element of G st
( x = g1 * g2 & g1 in H & g2 in A ) by A1; :: thesis: verum

end;

given g1, g2 being Element of G such that A2: ( x = g1 * g2 & g1 in H & g2 in A ) ; :: thesis: x in H * A
g1 in carr H by A2, STRUCT_0:def 5;
hence x in H * A by A2; :: thesis: verum