let I be non empty set ; :: thesis:
let F, G be Group-Family of I; :: thesis:
let h be non empty Function; :: thesis:
assume that
A1: I = dom h and
A2: for i being Element of I ex hi being Homomorphism of (F . i),(G . i) st
( hi = h . i & hi is bijective ) ; :: thesis:
A3: for i being Element of I holds h . i is Homomorphism of (F . i),(G . i)

let i be Element of I; :: thesis:
consider hi being Homomorphism of (F . i),(G . i) such that
A4: ( hi = h . i & hi is bijective ) by A2;
thus h . i is Homomorphism of (F . i),(G . i) by A4; :: thesis:

end;

set p = ProductMap (F,G,h);
set s = SumMap (F,G,h);
A5: ProductMap (F,G,h) is bijective by A1, A2, Th40;
A6: SumMap (F,G,h) = (ProductMap (F,G,h)) | (sum F) by A1, A3, Def7;
then A7: SumMap (F,G,h) is one-to-one by A5, FUNCT_1:52;
A9: rng (SumMap (F,G,h)) c= [#] (sum G) ;
for y being object st y in [#] (sum G) holds
y in rng (SumMap (F,G,h))

let y be object ; :: thesis:
assume A10: y in [#] (sum G) ; :: thesis:
then y in sum G ;
then A11: y in product G by GROUP_2:40;
then y in rng (ProductMap (F,G,h)) by A5, GROUP_6:61;
then consider x being object such that
A12: x in dom (ProductMap (F,G,h)) and
A13: y = (ProductMap (F,G,h)) . x by FUNCT_1:def 3;
reconsider x = x as Element of (product F) by A12;
reconsider y = y as Element of (product G) by A11;
A15: x in sum F

assume A16: not x in sum F ; :: thesis:
for i being Element of I ex ki being Homomorphism of (G . i),(F . i) st x . i = ki . (y . i)

let i be Element of I; :: thesis:
consider hi being Homomorphism of (F . i),(G . i) such that
A18: hi = h . i and
A19: y . i = hi . (x . i) by A1, A3, A13, Th39;
consider li being Homomorphism of (F . i),(G . i) such that
A20: ( li = h . i & li is bijective ) by A2;
reconsider ki = hi " as Homomorphism of (G . i),(F . i) by A18, A20, GROUP_6:62;
take ki ; :: thesis:
x in product F ;
then x . i in F . i by Th5;
hence x . i = ki . (y . i) by A18, A19, A20, FUNCT_2:26; :: thesis:

end;

end;

end;