let x be set ; :: thesis: for G being Group
for H1, H2 being Subgroup of G holds
( x in H1 * H2 iff ex a, b being Element of G st
( x = a * b & a in H1 & b in H2 ) )
let G be Group; :: thesis: for H1, H2 being Subgroup of G holds
( x in H1 * H2 iff ex a, b being Element of G st
( x = a * b & a in H1 & b in H2 ) )
let H1, H2 be Subgroup of G; :: thesis: ( x in H1 * H2 iff ex a, b being Element of G st
( x = a * b & a in H1 & b in H2 ) )
thus ( x in H1 * H2 implies ex a, b being Element of G st
( x = a * b & a in H1 & b in H2 ) ) :: thesis: ( ex a, b being Element of G st
( x = a * b & a in H1 & b in H2 ) implies x in H1 * H2 )

proof

assume x in H1 * H2 ; :: thesis: ex a, b being Element of G st
( x = a * b & a in H1 & b in H2 )
then x in (carr H1) * H2 ;
then consider a, b being Element of G such that
A1: ( x = a * b & a in carr H1 & b in H2 ) by GROUP_2:114;
a in H1 by A1, STRUCT_0:def 5;
hence ex a, b being Element of G st
( x = a * b & a in H1 & b in H2 ) by A1; :: thesis: verum

end;

given a, b being Element of G such that A2: ( x = a * b & a in H1 & b in H2 ) ; :: thesis: x in H1 * H2
b in carr H2 by A2, STRUCT_0:def 5;
then x in H1 * (carr H2) by A2, GROUP_2:115;
hence x in H1 * H2 ; :: thesis: verum