let h1, h2 be Homomorphism of (sum F),G; :: thesis: ( h1 is bijective & ( for x being finite-support Function of I,G st x in sum F holds
h1 . x = Product x ) & h2 is bijective & ( for x being finite-support Function of I,G st x in sum F holds
h2 . x = Product x ) implies h1 = h2 )
assume that
A1: ( h1 is bijective & ( for x being finite-support Function of I,G st x in sum F holds
h1 . x = Product x ) ) and
A2: ( h2 is bijective & ( for x being finite-support Function of I,G st x in sum F holds
h2 . x = Product x ) ) ; :: thesis: h1 = h2
A3: for i being object st i in I holds
F . i is Subgroup of G by GROUP_19:def 9;
for x being Element of (sum F) holds h1 . x = h2 . x

proof

let x be Element of (sum F); :: thesis: h1 . x = h2 . x
A4: x in sum F ;
then reconsider x0 = x as finite-support Function of I,G by A3, GROUP_19:10;
thus h1 . x = Product x0 by A1, A4
.= h2 . x by A2, A4 ; :: thesis: verum

end;

hence h1 = h2 by FUNCT_2:63; :: thesis: verum