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

for H1, H2 being Subgroup of G st H1 * H2 = H2 * H1 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 st H1 * H2 = H2 * H1 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: ( H1 * H2 = H2 * H1 implies ( x in H1 "\/" H2 iff ex a, b being Element of G st

( x = a * b & a in H1 & b in H2 ) ) )

assume A1: H1 * H2 = H2 * H1 ; :: 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 )

x in H1 * H2 by A2, Th4;

then x in the carrier of (H1 "\/" H2) by A1, GROUP_4:51;

hence x in H1 "\/" H2 by STRUCT_0:def 5; :: thesis: verum

for H1, H2 being Subgroup of G st H1 * H2 = H2 * H1 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 st H1 * H2 = H2 * H1 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: ( H1 * H2 = H2 * H1 implies ( x in H1 "\/" H2 iff ex a, b being Element of G st

( x = a * b & a in H1 & b in H2 ) ) )

assume A1: H1 * H2 = H2 * H1 ; :: 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 A2:
( x = a * b & a in H1 & b in H2 )
; :: thesis: x in H1 "\/" H2
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 the carrier of (H1 "\/" H2) by STRUCT_0:def 5;

then x in H1 * H2 by A1, GROUP_4:51;

hence ex a, b being Element of G st

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

end;( x = a * b & a in H1 & b in H2 )

then x in the carrier of (H1 "\/" H2) by STRUCT_0:def 5;

then x in H1 * H2 by A1, GROUP_4:51;

hence ex a, b being Element of G st

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

x in H1 * H2 by A2, Th4;

then x in the carrier of (H1 "\/" H2) by A1, GROUP_4:51;

hence x in H1 "\/" H2 by STRUCT_0:def 5; :: thesis: verum