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 onto ) ) holds
ProductMap (F,G,h) is onto
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 onto ) ) implies ProductMap (F,G,h) is onto )
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 onto ) ; :: thesis: ProductMap (F,G,h) is onto
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 onto ) by A2;
hence h . i is Function of (F . i),(G . i) ; :: thesis: verum

end;

for y being object st y in product G holds
ex x being object st
( x in product F & y = (ProductMap (F,G,h)) . x )

proof

let y be object ; :: thesis: ( y in product G implies ex x being object st
( x in product F & y = (ProductMap (F,G,h)) . x ) )
assume A5: y in product G ; :: thesis: ex x being object st
( x in product F & y = (ProductMap (F,G,h)) . x )
then reconsider y = y as Function ;
A6: ( dom y = dom G & ( for x being object st x in dom G holds
y . x in G . x ) ) by A5, CARD_3:9;
defpred S₁[ object , object ] means ex i being Element of dom h ex hi being Function of (F . i),(G . i) st
( $1 = i & hi = h . i & $2 in F . i & y . i = hi . $2 );
A7: for i being object st i in dom F holds
ex x being object st S₁[i,x]

proof

let i be object ; :: thesis: ( i in dom F implies ex x being object st S₁[i,x] )
assume i in dom F ; :: thesis: ex x being object st S₁[i,x]
then reconsider i = i as Element of dom h by A1;
consider hi being Function of (F . i),(G . i) such that
A9: ( hi = h . i & hi is onto ) by A2;
rng hi = G . i by A9, FUNCT_2:def 3;
then consider x being object such that
A11: ( x in F . i & y . i = hi . x ) by A1, A5, CARD_3:9, FUNCT_2:11;
take x ; :: thesis: S₁[i,x]
thus S₁[i,x] by A9, A11; :: thesis: verum

end;

consider x being Function such that
A12: ( dom x = dom F & ( for i being object st i in dom F holds
S₁[i,x . i] ) ) from CLASSES1:sch 1(A7);

now :: thesis: for i being object st i in dom F holds
x . i in F . i

let i be object ; :: thesis: ( i in dom F implies x . i in F . i )
assume i in dom F ; :: thesis: x . i in F . i
then ex i0 being Element of dom h ex hi being Function of (F . i0),(G . i0) st
( i = i0 & hi = h . i0 & x . i in F . i0 & y . i0 = hi . (x . i) ) by A12;
hence x . i in F . i ; :: thesis: verum

end;

then reconsider x = x as Element of product F by A12, CARD_3:9;
take x ; :: thesis: ( x in product F & y = (ProductMap (F,G,h)) . x )
A14: dom y = dom ((ProductMap (F,G,h)) . x) by A6, CARD_3:9;

now :: thesis: for i being object st i in dom y holds
y . i = ((ProductMap (F,G,h)) . x) . i

let i be object ; :: thesis: ( i in dom y implies y . i = ((ProductMap (F,G,h)) . x) . i )
assume i in dom y ; :: thesis: y . i = ((ProductMap (F,G,h)) . x) . i
then i in dom F by A1, A5, CARD_3:9;
then consider i0 being Element of dom h, hi being Function of (F . i0),(G . i0) such that
A16: ( i = i0 & hi = h . i0 & x . i in F . i0 & y . i0 = hi . (x . i) ) by A12;
ex hi being Function of (F . i0),(G . i0) st
( hi = h . i0 & ((ProductMap (F,G,h)) . x) . i0 = hi . (x . i0) ) by A1, A4, Def5;
hence y . i = ((ProductMap (F,G,h)) . x) . i by A16; :: thesis: verum

end;

hence ( x in product F & y = (ProductMap (F,G,h)) . x ) by A14, FUNCT_1:2; :: thesis: verum

end;

then rng (ProductMap (F,G,h)) = product G by FUNCT_2:10;
hence ProductMap (F,G,h) is onto by FUNCT_2:def 3; :: thesis: verum