let f, g, h be Function; :: thesis: ( dom f = dom h & dom g = rng h & h is one-to-one & ( for x being object st x in dom h holds
f . x,g . (h . x) are_equipotent ) implies product f, product g are_equipotent )
set X = dom f;
assume that
A1: dom f = dom h and
A2: dom g = rng h and
A3: h is one-to-one and
A4: for x being object st x in dom h holds
f . x,g . (h . x) are_equipotent ; :: thesis: product f, product g are_equipotent
A5: h * (h ") = id (dom g) by A2, A3, FUNCT_1:39;
A6: dom (g * h) = dom f by A1, A2, RELAT_1:27;

now :: thesis: for x being object st x in dom f holds
f . x,(g * h) . x are_equipotent

let x be object ; :: thesis: ( x in dom f implies f . x,(g * h) . x are_equipotent )
assume A7: x in dom f ; :: thesis: f . x,(g * h) . x are_equipotent
then f . x,g . (h . x) are_equipotent by A1, A4;
hence f . x,(g * h) . x are_equipotent by A6, A7, FUNCT_1:12; :: thesis: verum

end;

then A8: product f, product (g * h) are_equipotent by A6, Th38;
defpred S₁[ object , object ] means ex f1 being Function st
( $1 = f1 & $2 = f1 * (h ") );
A9: for x being object st x in product (g * h) holds
ex y being object st S₁[x,y]

proof

let x be object ; :: thesis: ( x in product (g * h) implies ex y being object st S₁[x,y] )
assume x in product (g * h) ; :: thesis: ex y being object st S₁[x,y]
then ex f1 being Function st
( x = f1 & dom f1 = dom (g * h) & ( for y being object st y in dom (g * h) holds
f1 . y in (g * h) . y ) ) by CARD_3:def 5;
then consider f1 being Function such that
A10: x = f1 ;
f1 * (h ") = f1 * (h ") ;
hence ex y being object st S₁[x,y] by A10; :: thesis: verum

end;

consider F being Function such that
A11: ( dom F = product (g * h) & ( for x being object st x in product (g * h) holds
S₁[x,F . x] ) ) from CLASSES1:sch 1(A9);
A12: rng (h ") = dom f by A1, A3, FUNCT_1:33;
A13: F is one-to-one

proof

let x, y be object ; :: according to FUNCT_1:def 4 :: thesis: ( not x in dom F or not y in dom F or not F . x = F . y or x = y )
assume that
A14: x in dom F and
A15: y in dom F and
A16: F . x = F . y ; :: thesis: x = y
consider g2 being Function such that
A17: y = g2 and
A18: F . y = g2 * (h ") by A11, A15;
A19: dom g2 = dom f by A6, A11, A15, A17, CARD_3:9;
consider g1 being Function such that
A20: x = g1 and
A21: F . x = g1 * (h ") by A11, A14;
dom g1 = dom f by A6, A11, A14, A20, CARD_3:9;
hence x = y by A12, A16, A20, A21, A17, A18, A19, FUNCT_1:86; :: thesis: verum

end;

A22: ( (g * h) * (h ") = g * (h * (h ")) & g * (id (dom g)) = g ) by RELAT_1:36, RELAT_1:52;
A23: product g c= rng F

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in product g or x in rng F )
assume x in product g ; :: thesis: x in rng F
then consider f1 being Function such that
A24: x = f1 and
A25: dom f1 = dom g and
A26: for z being object st z in dom g holds
f1 . z in g . z by CARD_3:def 5;
A27: dom (f1 * h) = dom f by A1, A2, A25, RELAT_1:27;

now :: thesis: for z being object st z in dom f holds
(f1 * h) . z in (g * h) . z

let z be object ; :: thesis: ( z in dom f implies (f1 * h) . z in (g * h) . z )
assume A28: z in dom f ; :: thesis: (f1 * h) . z in (g * h) . z
then A29: h . z in dom g by A1, A2, FUNCT_1:def 3;
A30: (h ") . (h . z) = z by A1, A3, A28, FUNCT_1:34;
(f1 * h) . z = f1 . (h . z) by A27, A28, FUNCT_1:12;
then (f1 * h) . z in ((g * h) * (h ")) . (h . z) by A5, A22, A26, A29;
hence (f1 * h) . z in (g * h) . z by A5, A22, A29, A30, FUNCT_1:12; :: thesis: verum

end;

then A31: f1 * h in product (g * h) by A6, A27, CARD_3:def 5;
then ex f2 being Function st
( f1 * h = f2 & F . (f1 * h) = f2 * (h ") ) by A11;
then F . (f1 * h) = f1 * (id (dom g)) by A5, RELAT_1:36
.= x by A24, A25, RELAT_1:51 ;
hence x in rng F by A11, A31, FUNCT_1:def 3; :: thesis: verum

end;

A32: dom (h ") = rng h by A3, FUNCT_1:33;
rng F c= product g

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rng F or x in product g )
assume x in rng F ; :: thesis: x in product g
then consider y being object such that
A33: y in dom F and
A34: x = F . y by FUNCT_1:def 3;
consider f1 being Function such that
A35: y = f1 and
A36: dom f1 = dom f and
A37: for z being object st z in dom f holds
f1 . z in (g * h) . z by A6, A11, A33, CARD_3:def 5;
A38: dom (f1 * (h ")) = dom g by A2, A12, A32, A36, RELAT_1:27;

A39: now :: thesis: for z being object st z in dom g holds
(f1 * (h ")) . z in g . z

let z be object ; :: thesis: ( z in dom g implies (f1 * (h ")) . z in g . z )
assume A40: z in dom g ; :: thesis: (f1 * (h ")) . z in g . z
then A41: (h ") . z in dom f by A2, A12, A32, FUNCT_1:def 3;
( g . z = (g * h) . ((h ") . z) & (f1 * (h ")) . z = f1 . ((h ") . z) ) by A5, A22, A38, A40, FUNCT_1:12;
hence (f1 * (h ")) . z in g . z by A37, A41; :: thesis: verum

end;

ex f1 being Function st
( y = f1 & F . y = f1 * (h ") ) by A11, A33;
hence x in product g by A34, A35, A38, A39, CARD_3:def 5; :: thesis: verum

end;

then rng F = product g by A23;
then product (g * h), product g are_equipotent by A11, A13;
hence product f, product g are_equipotent by A8, WELLORD2:15; :: thesis: verum