let x be set ; 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; 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; ( 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
; ( 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 ) )
( ex a, b being Element of G st
( x = a * b & a in H1 & b in H2 ) implies x in H1 "\/" H2 )
given a, b being Element of G such that A2:
( x = a * b & a in H1 & b in H2 )
; 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; verum