consider i being object such that
A1: i in I by XBOOLE_0:def 1;
consider F being Group-Family of I, h being Homomorphism of (sum F),G such that
A2: ( h is bijective & F = (I --> ((1). G)) +* ({i} --> G) & ( for j being Element of I holds 1_ (F . j) = 1_ G ) & ( for x being Element of (sum F) holds h . x = x . i ) & ( for x being Element of (sum F) ex J being finite Subset of I ex a being ManySortedSet of J st
( J c= {i} & J = support (x,F) & ( support (x,F) = {} or support (x,F) = {i} ) & x = (1_ (product F)) +* a & ( for j being Element of I st j in I \ J holds
x . j = 1_ (F . j) ) & ( for j being object st j in J holds
x . j = a . j ) ) ) ) by A1, Th43;
thus ex b₁ being Group-Family of I ex h being Homomorphism of (sum b₁),G st h is bijective by A2; :: thesis: verum