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

( x in G ` 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 G & x = Product (F |^ I) ) )

let G be Group; :: thesis: ( x in G ` 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 G & x = Product (F |^ I) ) )

thus ( x in G ` 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 G & 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 G & x = Product (F |^ I) ) implies x in G ` )

thus x in G ` by A2, GROUP_4:28; :: thesis: verum

( x in G ` 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 G & x = Product (F |^ I) ) )

let G be Group; :: thesis: ( x in G ` 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 G & x = Product (F |^ I) ) )

thus ( x in G ` 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 G & 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 G & x = Product (F |^ I) ) implies x in G ` )

proof

given F being FinSequence of the carrier of G, I being FinSequence of INT such that A2:
( len F = len I & rng F c= commutators G & x = Product (F |^ I) )
; :: thesis: x in G `
assume A1:
x in G `
; :: 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 G & 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;

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

( len F = len I & rng F c= commutators G & a = Product (F |^ I) ) by A1, GROUP_4:28;

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 G & x = Product (F |^ I) ) ; :: thesis: verum

end;( len F = len I & rng F c= commutators G & 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;

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

( len F = len I & rng F c= commutators G & a = Product (F |^ I) ) by A1, GROUP_4:28;

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 G & x = Product (F |^ I) ) ; :: thesis: verum

thus x in G ` by A2, GROUP_4:28; :: thesis: verum