let F, G be non-empty non empty Function; :: thesis: 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
let h be non empty Function; :: thesis: ( 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 ) ) implies ProductMap (F,G,h) is bijective )
assume that
A1: ( dom F = dom G & dom G = dom h ) and
A2: 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 ) ; :: thesis: ProductMap (F,G,h) is bijective
set p = ProductMap (F,G,h);

now :: thesis: 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 onto )

let i be object ; :: thesis: ( i in dom h implies ex hi being Function of (F . i),(G . i) st
( hi = h . i & hi is onto ) )
assume i in dom h ; :: thesis: ex hi being Function of (F . i),(G . i) st
( hi = h . i & hi is onto )
then ex hi being Function of (F . i),(G . i) st
( hi = h . i & hi is bijective ) by A2;
hence ex hi being Function of (F . i),(G . i) st
( hi = h . i & hi is onto ) ; :: thesis: verum

end;

then A3: ProductMap (F,G,h) is onto by A1, Th35;

now :: thesis: 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 one-to-one )

let i be object ; :: thesis: ( i in dom h implies ex hi being Function of (F . i),(G . i) st
( hi = h . i & hi is one-to-one ) )
assume i in dom h ; :: thesis: ex hi being Function of (F . i),(G . i) st
( hi = h . i & hi is one-to-one )
then ex hi being Function of (F . i),(G . i) st
( hi = h . i & hi is bijective ) by A2;
hence ex hi being Function of (F . i),(G . i) st
( hi = h . i & hi is one-to-one ) ; :: thesis: verum

end;

then ProductMap (F,G,h) is one-to-one by A1, Th36;
hence ProductMap (F,G,h) is bijective by A3; :: thesis: verum