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 ` )
proof
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;
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 `
thus x in G ` by A2, GROUP_4:28; :: thesis: verum