defpred S1[ object ] means ex g being Element of product () ex J being finite Subset of I ex f being ManySortedSet of J st
( g = 1_ () & \$1 = g +* f & ( for j being set st j in J holds
ex G being non empty Group-like multMagma st
( G = F . j & f . j in the carrier of G & f . j <> 1_ G ) ) );
let A, B be strict Subgroup of product F; :: thesis: ( ( for x being object holds
( x in the carrier of A iff ex g being Element of product () ex J being finite Subset of I ex f being ManySortedSet of J st
( g = 1_ () & x = g +* f & ( for j being set st j in J holds
ex G being non empty Group-like multMagma st
( G = F . j & f . j in the carrier of G & f . j <> 1_ G ) ) ) ) ) & ( for x being object holds
( x in the carrier of B iff ex g being Element of product () ex J being finite Subset of I ex f being ManySortedSet of J st
( g = 1_ () & x = g +* f & ( for j being set st j in J holds
ex G being non empty Group-like multMagma st
( G = F . j & f . j in the carrier of G & f . j <> 1_ G ) ) ) ) ) implies A = B )

assume that
A106: for x being object holds
( x in the carrier of A iff S1[x] ) and
A107: for x being object holds
( x in the carrier of B iff S1[x] ) ; :: thesis: A = B
the carrier of A = the carrier of B from hence A = B by GROUP_2:59; :: thesis: verum