:: deftheorem Def5 defines ProductMap GROUP_19:def 5 :
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
h . i is Function of (F . i),(G . i) ) holds
for b₄ being Function of (product F),(product G) holds
( b₄ = ProductMap (F,G,h) iff for x being Element of product F
for i being object st i in dom h holds
ex hi being Function of (F . i),(G . i) st
( hi = h . i & (b₄ . x) . i = hi . (x . i) ) );