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 that
A1: dom f = X and
A2: dom g = X and
A3: 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 );
A4: 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 A3;
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
A5: ( dom h = X & ( for x being set st x in X holds
S₁[x,h . x] ) ) from CLASSES1:sch 1(A4);

A6: now

let x be set ; :: thesis: ( x in X implies (rngs h) . x = g . x )
assume A7: 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 A5;
hence (rngs h) . x = g . x by A5, A7, Th31; :: thesis: verum

end;

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
A8: ( a in X & x = h . a ) by A5, FUNCT_1:def 3;
ex f1 being Function st
( x = f1 & f1 is one-to-one & dom f1 = f . a & rng f1 = g . a ) by A5, A8;
hence x is Function ; :: thesis: verum

end;

then SubFuncs (rng h) = rng h by Lm1;
then A9: h " (SubFuncs (rng h)) = X by A5, RELAT_1:134;
then dom (rngs h) = X by Def3;
then A10: rngs h = g by A2, A6, FUNCT_1:2;

A11: now

let x be set ; :: thesis: ( x in X implies (doms h) . x = f . x )
assume A12: 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 A5;
hence (doms h) . x = f . x by A5, A12, Th31; :: thesis: verum

end;

dom (doms h) = X by A9, Def2;
then A13: doms h = f by A1, A11, FUNCT_1:2;

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
A14: x in X and
A15: {} = h . x by A5, FUNCT_1:def 3;
A16: ex f1 being Function st
( {} = f1 & f1 is one-to-one & dom f1 = f . x & rng f1 = g . x ) by A5, A14, A15;
then {} in rng f by A1, A14, FUNCT_1:def 3, RELAT_1:38;
then A17: product f = {} by CARD_3:26;
{} in rng g by A2, A14, A16, FUNCT_1:def 3, RELAT_1:38;
hence product f, product g are_equipotent by A17, CARD_3:26; :: thesis: verum

end;

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

A19: 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
A20: x in X and
A21: f1 = h . x by A5, FUNCT_1:def 3;
ex f1 being Function st
( h . x = f1 & f1 is one-to-one & dom f1 = f . x & rng f1 = g . x ) by A5, A20;
hence f1 is one-to-one by A21; :: 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 A13, A10, A18, A19, Def7, Th58, Th59; :: thesis: verum

end;

end;

end;

end;

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