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 object st i in I holds
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 object st i in I holds
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 object st i in I holds
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 object st i in I holds
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 dom h 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 dom h implies ex hi being Function of ((Carrier F) . i),((Carrier G) . i) st
( hi = h . i & hi is bijective ) )
assume A4: i in dom h ; :: thesis: ex hi being Function of ((Carrier F) . i),((Carrier G) . i) st
( hi = h . i & hi is bijective )
then consider hi being Homomorphism of (F . i),(G . i) such that
A5: ( hi = h . i & hi is bijective ) by A1;
A6: (Carrier F) . i = [#] (F . i) by A1, A4, Th4;
A7: (Carrier G) . i = [#] (G . i) by A1, A4, Th4;
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 object st i in I holds
h . i is Homomorphism of (F . i),(G . i)

proof

let i be object ; :: thesis: ( i in I implies h . i is Homomorphism of (F . i),(G . i) )
assume i in I ; :: thesis: h . i is Homomorphism of (F . i),(G . i)
then consider hi being Homomorphism of (F . i),(G . i) such that
A11: ( hi = h . i & hi is bijective ) by A1;
thus h . i is Homomorphism of (F . i),(G . i) by A11; :: thesis: verum

end;

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