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.] )

proof

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;

thus ( 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.] ) by GROUP_4:28; :: thesis: verum