let f, h, g be Function; :: thesis: ( dom f = dom h & dom g = rng h & h is one-to-one & ( for x being set 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 & dom g = rng h & h is one-to-one ) and
A2: for x being set st x in dom h holds
f . x,g . (h . x) are_equipotent ; :: thesis: product f, product g are_equipotent
A3: dom (g * h) = dom f by A1, RELAT_1:46;

now

let x be set ; :: thesis: ( x in dom f implies f . x,(g * h) . x are_equipotent )
assume x in dom f ; :: thesis: f . x,(g * h) . x are_equipotent
then ( f . x,g . (h . x) are_equipotent & g . (h . x) = (g * h) . x ) by A1, A2, A3, FUNCT_1:22;
hence f . x,(g * h) . x are_equipotent ; :: thesis: verum

end;

then A4: product f, product (g * h) are_equipotent by A3, Th69;
defpred S₁[ set , set ] means ex f1 being Function st
( $1 = f1 & $2 = f1 * (h " ) );
A5: for x being set st x in product (g * h) holds
ex y being set st S₁[x,y]

proof

let x be set ; :: thesis: ( x in product (g * h) implies ex y being set st S₁[x,y] )
assume x in product (g * h) ; :: thesis: ex y being set st S₁[x,y]
then ex f1 being Function st
( x = f1 & dom f1 = dom (g * h) & ( for y being set 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
A6: x = f1 ;
f1 * (h " ) = f1 * (h " ) ;
hence ex y being set st S₁[x,y] by A6; :: thesis: verum

end;

consider F being Function such that
A7: ( dom F = product (g * h) & ( for x being set st x in product (g * h) holds
S₁[x,F . x] ) ) from CLASSES1:sch 1(A5);
A8: ( rng (h " ) = dom f & (h " ) " = h & dom (h " ) = rng h & h " is one-to-one & (g * h) * (h " ) = g * (h * (h " )) & h * (h " ) = id (dom g) & g * (id (dom g)) = g ) by A1, FUNCT_1:55, FUNCT_1:61, FUNCT_1:65, RELAT_1:55, RELAT_1:78;
A9: F is one-to-one

proof

let x be set ; :: according to FUNCT_1:def 8 :: thesis: for b₁ being set holds
( not x in proj1 F or not b₁ in proj1 F or not F . x = F . b₁ or x = b₁ )
let y be set ; :: thesis: ( not x in proj1 F or not y in proj1 F or not F . x = F . y or x = y )
assume A10: ( x in dom F & y in dom F & F . x = F . y ) ; :: thesis: x = y
then consider g1 being Function such that
A11: ( x = g1 & F . x = g1 * (h " ) ) by A7;
consider g2 being Function such that
A12: ( y = g2 & F . y = g2 * (h " ) ) by A7, A10;
( dom g1 = dom f & dom g2 = dom f ) by A3, A7, A10, A11, A12, CARD_3:18;
hence x = y by A8, A10, A11, A12, FUNCT_1:156; :: thesis: verum

end;

A13: rng F c= product g

proof

let x be set ; :: 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 set such that
A14: ( y in dom F & x = F . y ) by FUNCT_1:def 5;
consider f1 being Function such that
A15: ( y = f1 & dom f1 = dom f & ( for z being set st z in dom f holds
f1 . z in (g * h) . z ) ) by A3, A7, A14, CARD_3:def 5;
ex f1 being Function st
( y = f1 & F . y = f1 * (h " ) ) by A7, A14;
then A16: ( x = f1 * (h " ) & dom (f1 * (h " )) = dom g & dom ((g * h) * (h " )) = dom g ) by A1, A8, A14, A15, RELAT_1:46;

now

let z be set ; :: thesis: ( z in dom g implies (f1 * (h " )) . z in g . z )
assume z in dom g ; :: thesis: (f1 * (h " )) . z in g . z
then ( g . z = (g * h) . ((h " ) . z) & (f1 * (h " )) . z = f1 . ((h " ) . z) & (h " ) . z in dom f ) by A1, A8, A16, FUNCT_1:22, FUNCT_1:def 5;
hence (f1 * (h " )) . z in g . z by A15; :: thesis: verum

end;

hence x in product g by A16, CARD_3:def 5; :: thesis: verum

end;

product g c= rng F

proof

let x be set ; :: 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
A17: ( x = f1 & dom f1 = dom g & ( for z being set st z in dom g holds
f1 . z in g . z ) ) by CARD_3:def 5;
A18: dom (f1 * h) = dom f by A1, A17, RELAT_1:46;

now

let z be set ; :: thesis: ( z in dom f implies (f1 * h) . z in (g * h) . z )
assume z in dom f ; :: thesis: (f1 * h) . z in (g * h) . z
then ( (f1 * h) . z = f1 . (h . z) & h . z in dom g & (h " ) . (h . z) = z ) by A1, A18, FUNCT_1:22, FUNCT_1:56, FUNCT_1:def 5;
then ( (f1 * h) . z in ((g * h) * (h " )) . (h . z) & ((g * h) * (h " )) . (h . z) = (g * h) . z ) by A8, A17, FUNCT_1:22;
hence (f1 * h) . z in (g * h) . z ; :: thesis: verum

end;

then A19: f1 * h in product (g * h) by A3, A18, CARD_3:def 5;
then ex f2 being Function st
( f1 * h = f2 & F . (f1 * h) = f2 * (h " ) ) by A7;
then F . (f1 * h) = f1 * (id (dom g)) by A8, RELAT_1:55
.= x by A17, RELAT_1:77 ;
hence x in rng F by A7, A19, FUNCT_1:def 5; :: thesis: verum

end;

then rng F = product g by A13, XBOOLE_0:def 10;
then product (g * h), product g are_equipotent by A7, A9, WELLORD2:def 4;
hence product f, product g are_equipotent by A4, WELLORD2:22; :: thesis: verum