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

for H1, H2 being Subgroup of G holds

( x in commutators (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 commutators (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 commutators (H1,H2) iff ex a, b being Element of G st

( x = [.a,b.] & a in H1 & b in H2 ) )

thus ( x in commutators (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 commutators (H1,H2) )

A4: ( a in H1 & b in H2 ) ; :: thesis: x in commutators (H1,H2)

( a in carr H1 & b in carr H2 ) by A4, STRUCT_0:def 5;

hence x in commutators (H1,H2) by A3; :: thesis: verum

for H1, H2 being Subgroup of G holds

( x in commutators (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 commutators (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 commutators (H1,H2) iff ex a, b being Element of G st

( x = [.a,b.] & a in H1 & b in H2 ) )

thus ( x in commutators (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 commutators (H1,H2) )

proof

given a, b being Element of G such that A3:
x = [.a,b.]
and
assume
x in commutators (H1,H2)
; :: thesis: ex a, b being Element of G st

( x = [.a,b.] & a in H1 & b in H2 )

then consider a, b being Element of G such that

A1: x = [.a,b.] and

A2: ( a in carr H1 & b in carr H2 ) ;

( a in H1 & b in H2 ) 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; :: thesis: verum

end;( x = [.a,b.] & a in H1 & b in H2 )

then consider a, b being Element of G such that

A1: x = [.a,b.] and

A2: ( a in carr H1 & b in carr H2 ) ;

( a in H1 & b in H2 ) 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; :: thesis: verum

A4: ( a in H1 & b in H2 ) ; :: thesis: x in commutators (H1,H2)

( a in carr H1 & b in carr H2 ) by A4, STRUCT_0:def 5;

hence x in commutators (H1,H2) by A3; :: thesis: verum