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 )

A5: b in H2 ; :: thesis: x in H1 * H2

b in carr H2 by A5, STRUCT_0:def 5;

then x in H1 * (carr H2) by A4, GROUP_2:95;

hence x in H1 * H2 ; :: thesis: verum

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

given a, b being Element of G such that A4:
( x = a * b & a in H1 )
and
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 and

A2: a in carr H1 and

A3: b in H2 by GROUP_2:94;

a in H1 by A2, STRUCT_0:def 5;

hence ex a, b being Element of G st

( x = a * b & a in H1 & b in H2 ) by A1, A3; :: thesis: verum

end;( 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 and

A2: a in carr H1 and

A3: b in H2 by GROUP_2:94;

a in H1 by A2, STRUCT_0:def 5;

hence ex a, b being Element of G st

( x = a * b & a in H1 & b in H2 ) by A1, A3; :: thesis: verum

A5: b in H2 ; :: thesis: x in H1 * H2

b in carr H2 by A5, STRUCT_0:def 5;

then x in H1 * (carr H2) by A4, GROUP_2:95;

hence x in H1 * H2 ; :: thesis: verum