let I be non empty set ; :: thesis: for F, G being Group-Family of I
for h being non empty Function st I = dom h & ( for i being Element of I ex hi being Homomorphism of (F . i),(G . i) st
( hi = h . i & hi is bijective ) ) holds
ProductMap (F,G,h) is bijective
let F, G be Group-Family of I; :: thesis: for h being non empty Function st I = dom h & ( for i being Element of I ex hi being Homomorphism of (F . i),(G . i) st
( hi = h . i & hi is bijective ) ) holds
ProductMap (F,G,h) is bijective
let h be non empty Function; :: thesis: ( I = dom h & ( for i being Element of I ex hi being Homomorphism of (F . i),(G . i) st
( hi = h . i & hi is bijective ) ) implies ProductMap (F,G,h) is bijective )
assume A1: ( I = dom h & ( for i being Element of I ex hi being Homomorphism of (F . i),(G . i) st
( hi = h . i & hi is bijective ) ) ) ; :: thesis: ProductMap (F,G,h) is bijective
set p = ProductMap ((Carrier F),(Carrier G),h);
A3: ( dom (Carrier F) = I & dom (Carrier G) = I ) by PARTFUN1:def 2;
for i being object st i in I holds
ex hi being Function of ((Carrier F) . i),((Carrier G) . i) st
( hi = h . i & hi is bijective )

proof

let i be object ; :: thesis: ( i in I implies ex hi being Function of ((Carrier F) . i),((Carrier G) . i) st
( hi = h . i & hi is bijective ) )
assume i in I ; :: thesis: ex hi being Function of ((Carrier F) . i),((Carrier G) . i) st
( hi = h . i & hi is bijective )
then reconsider j = i as Element of I ;
consider hi being Homomorphism of (F . j),(G . j) such that
A5: ( hi = h . j & hi is bijective ) by A1;
A6: (Carrier F) . j = [#] (F . j) by PENCIL_3:7;
A7: (Carrier G) . j = [#] (G . j) by PENCIL_3:7;
then reconsider hi = hi as Function of ((Carrier F) . i),((Carrier G) . i) by A6;
take hi ; :: thesis: ( hi = h . i & hi is bijective )
thus ( hi = h . i & hi is bijective ) by A5, A7; :: thesis: verum

end;

then A8: ProductMap ((Carrier F),(Carrier G),h) is bijective by A1, A3, Th37;
A9: [#] (product F) = product (Carrier F) by GROUP_7:def 2;
A10: [#] (product G) = product (Carrier G) by GROUP_7:def 2;
reconsider p = ProductMap ((Carrier F),(Carrier G),h) as Function of (product F),(product G) by A9, GROUP_7:def 2;
for i being Element of I holds h . i is Homomorphism of (F . i),(G . i)

proof

let i be Element of I; :: thesis: h . i is Homomorphism of (F . i),(G . i)
ex hi being Homomorphism of (F . i),(G . i) st
( hi = h . i & hi is bijective ) by A1;
hence h . i is Homomorphism of (F . i),(G . i) ; :: thesis: verum

end;

then p = ProductMap (F,G,h) by A1, Def6;
hence ProductMap (F,G,h) is bijective by A8, A10; :: thesis: verum