let X be set ; :: thesis: for f, g being Function st dom f = X & dom g = X & ( for x being set st x in X holds
f . x,g . x are_equipotent ) holds
product f, product g are_equipotent
let f, g be Function; :: thesis: ( dom f = X & dom g = X & ( for x being set st x in X holds
f . x,g . x are_equipotent ) implies product f, product g are_equipotent )
assume A1: ( dom f = X & dom g = X & ( for x being set st x in X holds
f . x,g . x are_equipotent ) ) ; :: thesis: product f, product g are_equipotent
defpred S₁[ set , set ] means ex f1 being Function st
( $2 = f1 & f1 is one-to-one & dom f1 = f . $1 & rng f1 = g . $1 );
A2: for x being set st x in X holds
ex y being set st S₁[x,y]

proof

let x be set ; :: thesis: ( x in X implies ex y being set st S₁[x,y] )
assume x in X ; :: thesis: ex y being set st S₁[x,y]
then f . x,g . x are_equipotent by A1;
then ex h being Function st
( h is one-to-one & dom h = f . x & rng h = g . x ) by WELLORD2:def 4;
hence ex y being set st S₁[x,y] ; :: thesis: verum

end;

consider h being Function such that
A3: ( dom h = X & ( for x being set st x in X holds
S₁[x,h . x] ) ) from CLASSES1:sch 1(A2);

now

let x be set ; :: thesis: ( x in rng h implies x is Function )
assume x in rng h ; :: thesis: x is Function
then consider a being set such that
A4: ( a in X & x = h . a ) by A3, FUNCT_1:def 5;
ex f1 being Function st
( x = f1 & f1 is one-to-one & dom f1 = f . a & rng f1 = g . a ) by A3, A4;
hence x is Function ; :: thesis: verum

end;

then SubFuncs (rng h) = rng h by Lm1;
then h " (SubFuncs (rng h)) = X by A3, RELAT_1:169;
then A5: ( dom (doms h) = X & dom (rngs h) = X ) by Def2, Def3;

now

let x be set ; :: thesis: ( x in X implies (doms h) . x = f . x )
assume A6: x in X ; :: thesis: (doms h) . x = f . x
then ex f1 being Function st
( h . x = f1 & f1 is one-to-one & dom f1 = f . x & rng f1 = g . x ) by A3;
hence (doms h) . x = f . x by A3, A6, Th31; :: thesis: verum

end;

then A7: doms h = f by A1, A5, FUNCT_1:9;

now

let x be set ; :: thesis: ( x in X implies (rngs h) . x = g . x )
assume A8: x in X ; :: thesis: (rngs h) . x = g . x
then ex f1 being Function st
( h . x = f1 & f1 is one-to-one & dom f1 = f . x & rng f1 = g . x ) by A3;
hence (rngs h) . x = g . x by A3, A8, Th31; :: thesis: verum

end;

then A9: rngs h = g by A1, A5, FUNCT_1:9;

now

per cases ( {} in rng h or not {} in rng h ) ;

suppose {} in rng h ; :: thesis: product f, product g are_equipotent

then consider x being set such that
A10: ( x in X & {} = h . x ) by A3, FUNCT_1:def 5;
ex f1 being Function st
( {} = f1 & f1 is one-to-one & dom f1 = f . x & rng f1 = g . x ) by A3, A10;
then ( {} in rng f & {} in rng g ) by A1, A10, FUNCT_1:def 5, RELAT_1:60;
then ( product f = {} & product g = {} ) by CARD_3:37;
hence product f, product g are_equipotent ; :: thesis: verum

end;

suppose A11: not {} in rng h ; :: thesis: product f, product g are_equipotent

A12: now

let f1 be Function; :: thesis: ( f1 in rng h implies f1 is one-to-one )
assume f1 in rng h ; :: thesis: f1 is one-to-one
then consider x being set such that
A13: ( x in X & f1 = h . x ) by A3, FUNCT_1:def 5;
ex f1 being Function st
( h . x = f1 & f1 is one-to-one & dom f1 = f . x & rng f1 = g . x ) by A3, A13;
hence f1 is one-to-one by A13; :: thesis: verum

end;

thus product f, product g are_equipotent :: thesis: verum

proof

take Frege h ; :: according to WELLORD2:def 4 :: thesis: ( Frege h is one-to-one & proj1 (Frege h) = product f & proj2 (Frege h) = product g )
thus ( Frege h is one-to-one & proj1 (Frege h) = product f & proj2 (Frege h) = product g ) by A7, A9, A11, A12, Def7, Th58, Th59; :: thesis: verum

end;

end;

end;

end;

hence product f, product g are_equipotent ; :: thesis: verum