let x be object ; :: thesis:
assume x in [#] (sum F2) ; :: thesis:
then reconsider x = x as Element of (product F2) by GROUP_2:42;
dom x = I2 by GROUP_19:3;
then reconsider x = x as ManySortedSet of I2 by PARTFUN1:def 2, RELAT_1:def 18;
for i being set st i in I2 holds
ex G being non empty Group-like multMagma st
( G = F2 . i & x . i = 1_ G )

let i be set ; :: thesis:
assume i in I2 ; :: thesis:
then reconsider i = i as Element of I2 ;
reconsider G = F2 . i as Group ;
take G ; :: thesis:
A3: card G = 1 by A1;
then A4: [#] G is finite ;
A5: card {(1_ G)} = 1 by CARD_1:30;
A6: [#] G = {(1_ G)} by A3, A4, A5, CARD_2:102;
x in product F2 ;
then x . i in F2 . i by GROUP_19:5;
hence ( G = F2 . i & x . i = 1_ G ) by A6, TARSKI:def 1; :: thesis:

end;

end;