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 one-to-one ) ) holds
ProductMap (F,G,h) is one-to-one
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 one-to-one ) ) implies ProductMap (F,G,h) is one-to-one )
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 one-to-one ) ; :: thesis: ProductMap (F,G,h) is one-to-one
set p = ProductMap (F,G,h);
A4: for i being object st i in dom h holds
h . i is Function of (F . i),(G . i)

proof

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

end;

for x1, x2 being object st x1 in product F & x2 in product F & (ProductMap (F,G,h)) . x1 = (ProductMap (F,G,h)) . x2 holds
x1 = x2

proof

let x1, x2 be object ; :: thesis: ( x1 in product F & x2 in product F & (ProductMap (F,G,h)) . x1 = (ProductMap (F,G,h)) . x2 implies x1 = x2 )
assume A5: ( x1 in product F & x2 in product F & (ProductMap (F,G,h)) . x1 = (ProductMap (F,G,h)) . x2 ) ; :: thesis: x1 = x2
thus x1 = x2 :: thesis: verum

proof

reconsider x1 = x1, x2 = x2 as Element of product F by A5;
A7: dom x2 = dom F by CARD_3:9;
for i being object st i in dom x1 holds
x1 . i = x2 . i

proof

let i be object ; :: thesis: ( i in dom x1 implies x1 . i = x2 . i )
assume i in dom x1 ; :: thesis: x1 . i = x2 . i
then reconsider i = i as Element of dom h by A1, CARD_3:9;
consider hi1 being Function of (F . i),(G . i) such that
A9: ( hi1 = h . i & ((ProductMap (F,G,h)) . x1) . i = hi1 . (x1 . i) ) by A1, A4, Def5;
consider hi2 being Function of (F . i),(G . i) such that
A10: ( hi2 = h . i & ((ProductMap (F,G,h)) . x2) . i = hi2 . (x2 . i) ) by A1, A4, Def5;
A14: ex hi being Function of (F . i),(G . i) st
( hi = h . i & hi is one-to-one ) by A2;
A15: x1 . i in F . i by A1, CARD_3:9;
x2 . i in F . i by A1, CARD_3:9;
hence x1 . i = x2 . i by A1, A5, A9, A10, A14, A15, FUNCT_2:19; :: thesis: verum

end;

hence x1 = x2 by A7, CARD_3:9, FUNCT_1:2; :: thesis: verum

end;

end;

hence ProductMap (F,G,h) is one-to-one by FUNCT_2:19; :: thesis: verum