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

for A, B being Subset of G holds

( x in [.A,B.] iff ex F being FinSequence of the carrier of G ex I being FinSequence of INT st

( len F = len I & rng F c= commutators (A,B) & x = Product (F |^ I) ) )

let G be Group; :: thesis: for A, B being Subset of G holds

( x in [.A,B.] iff ex F being FinSequence of the carrier of G ex I being FinSequence of INT st

( len F = len I & rng F c= commutators (A,B) & x = Product (F |^ I) ) )

let A, B be Subset of G; :: thesis: ( x in [.A,B.] iff ex F being FinSequence of the carrier of G ex I being FinSequence of INT st

( len F = len I & rng F c= commutators (A,B) & x = Product (F |^ I) ) )

thus ( x in [.A,B.] implies ex F being FinSequence of the carrier of G ex I being FinSequence of INT st

( len F = len I & rng F c= commutators (A,B) & x = Product (F |^ I) ) ) :: thesis: ( ex F being FinSequence of the carrier of G ex I being FinSequence of INT st

( len F = len I & rng F c= commutators (A,B) & x = Product (F |^ I) ) implies x in [.A,B.] )

( len F = len I & rng F c= commutators (A,B) & x = Product (F |^ I) ) implies x in [.A,B.] ) by GROUP_4:28; :: thesis: verum

for A, B being Subset of G holds

( x in [.A,B.] iff ex F being FinSequence of the carrier of G ex I being FinSequence of INT st

( len F = len I & rng F c= commutators (A,B) & x = Product (F |^ I) ) )

let G be Group; :: thesis: for A, B being Subset of G holds

( x in [.A,B.] iff ex F being FinSequence of the carrier of G ex I being FinSequence of INT st

( len F = len I & rng F c= commutators (A,B) & x = Product (F |^ I) ) )

let A, B be Subset of G; :: thesis: ( x in [.A,B.] iff ex F being FinSequence of the carrier of G ex I being FinSequence of INT st

( len F = len I & rng F c= commutators (A,B) & x = Product (F |^ I) ) )

thus ( x in [.A,B.] implies ex F being FinSequence of the carrier of G ex I being FinSequence of INT st

( len F = len I & rng F c= commutators (A,B) & x = Product (F |^ I) ) ) :: thesis: ( ex F being FinSequence of the carrier of G ex I being FinSequence of INT st

( len F = len I & rng F c= commutators (A,B) & x = Product (F |^ I) ) implies x in [.A,B.] )

proof

thus
( ex F being FinSequence of the carrier of G ex I being FinSequence of INT st
assume A1:
x in [.A,B.]
; :: thesis: ex F being FinSequence of the carrier of G ex I being FinSequence of INT st

( len F = len I & rng F c= commutators (A,B) & x = Product (F |^ I) )

then x in G by GROUP_2:40;

then reconsider a = x as Element of G by STRUCT_0:def 5;

a in gr (commutators (A,B)) by A1;

hence ex F being FinSequence of the carrier of G ex I being FinSequence of INT st

( len F = len I & rng F c= commutators (A,B) & x = Product (F |^ I) ) by GROUP_4:28; :: thesis: verum

end;( len F = len I & rng F c= commutators (A,B) & x = Product (F |^ I) )

then x in G by GROUP_2:40;

then reconsider a = x as Element of G by STRUCT_0:def 5;

a in gr (commutators (A,B)) by A1;

hence ex F being FinSequence of the carrier of G ex I being FinSequence of INT st

( len F = len I & rng F c= commutators (A,B) & x = Product (F |^ I) ) by GROUP_4:28; :: thesis: verum

( len F = len I & rng F c= commutators (A,B) & x = Product (F |^ I) ) implies x in [.A,B.] ) by GROUP_4:28; :: thesis: verum