defpred S₁[ object ] means ex g being Element of product (Carrier F) ex J being finite Subset of I ex f being ManySortedSet of J st
( g = 1_ (product F) & $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 (Carrier F) ex J being finite Subset of I ex f being ManySortedSet of J st
( g = 1_ (product F) & 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 (Carrier F) ex J being finite Subset of I ex f being ManySortedSet of J st
( g = 1_ (product F) & 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 S₁[x] ) and
A107: for x being object holds
( x in the carrier of B iff S₁[x] ) ; :: thesis: A = B
the carrier of A = the carrier of B from XBOOLE_0:sch 2(A106, A107);
hence A = B by GROUP_2:59; :: thesis: verum