let I2 be non empty set ; :: thesis: for F2 being Group-Family of I2 st ( for i being Element of I2 holds card (F2 . i) = 1 ) holds
card the carrier of (sum F2) = 1
let F2 be Group-Family of I2; :: thesis: ( ( for i being Element of I2 holds card (F2 . i) = 1 ) implies card the carrier of (sum F2) = 1 )
assume A1: for i being Element of I2 holds card (F2 . i) = 1 ; :: thesis: card the carrier of (sum F2) = 1
A2: for x being object st 1_ (sum F2) = x holds
x in [#] (sum F2) ;
for x being object st x in [#] (sum F2) holds
x = 1_ (sum F2)

proof

let x be object ; :: thesis: ( x in [#] (sum F2) implies x = 1_ (sum F2) )
assume x in [#] (sum F2) ; :: thesis: x = 1_ (sum F2)
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 )

proof

let i be set ; :: thesis: ( i in I2 implies ex G being non empty Group-like multMagma st
( G = F2 . i & x . i = 1_ G ) )
assume i in I2 ; :: thesis: ex G being non empty Group-like multMagma st
( G = F2 . i & x . i = 1_ G )
then reconsider i = i as Element of I2 ;
reconsider G = F2 . i as Group ;
take G ; :: thesis: ( G = F2 . i & x . i = 1_ G )
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: verum

end;

then x = 1_ (product F2) by GROUP_7:5;
hence x = 1_ (sum F2) by GROUP_2:44; :: thesis: verum

end;

then [#] (sum F2) = {(1_ (sum F2))} by A2, TARSKI:def 1;
hence card the carrier of (sum F2) = 1 by CARD_1:30; :: thesis: verum