for F, G being non-empty non empty Function
for h being non empty Function st dom F = dom G & dom G = dom h & ( for i being object st i in dom h holds
ex hi being Function of (F . i),(G . i) st
( hi = h . i & hi is bijective ) ) holds
ProductMap (F,G,h) is bijective