defpred S_{1}[ 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_{1}[x] )
and

A107: for x being object holds

( x in the carrier of B iff S_{1}[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

( 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

A107: for x being object holds

( x in the carrier of B iff S

the carrier of A = the carrier of B from XBOOLE_0:sch 2(A106, A107);

hence A = B by GROUP_2:59; :: thesis: verum