let F, G be Cardinal-Function; :: thesis: ( dom F = dom G & ( for x being set st x in dom F holds
F . x in G . x ) implies Sum F in Product G )
assume A1: ( dom F = dom G & ( for x being set st x in dom F holds
F . x in G . x ) ) ; :: thesis: Sum F in Product G
deffunc H1( set ) -> Element of bool (G . $1) = (G . $1) \ (F . $1);
consider f being Function such that
A2: ( dom f = dom F & ( for x being set st x in dom F holds
f . x = H1(x) ) ) from FUNCT_1:sch 3();
now
assume {} in rng f ; :: thesis: contradiction
then consider x being set such that
A3: ( x in dom f & {} = f . x ) by FUNCT_1:def 5;
reconsider Fx = F . x, Gx = G . x as Cardinal by A1, A2, A3, Def1;
( Fx in Gx & not Fx in Fx ) by A1, A2, A3;
then ( Fx in Gx \ Fx & {} = Gx \ Fx ) by A2, A3, XBOOLE_0:def 5;
hence contradiction ; :: thesis: verum
end;
then A4: product f <> {} by Th37;
consider a being Element of product f;
consider h being Function such that
A5: ( a = h & dom h = dom f & ( for x being set st x in dom f holds
h . x in f . x ) ) by A4, Def5;
defpred S2[ set , Function] means ( dom $2 = dom F & ( for x being set st x in dom F holds
( ( $1 `2 = x implies $2 . x = $1 `1 ) & ( $1 `2 <> x implies $2 . x = h . x ) ) ) );
defpred S3[ set , set ] means ex g being Function st
( $2 = g & S2[$1,g] );
A9: for x being set st x in Union (disjoin F) holds
ex y being set st S3[x,y]
proof
let x be set ; :: thesis: ( x in Union (disjoin F) implies ex y being set st S3[x,y] )
assume x in Union (disjoin F) ; :: thesis: ex y being set st S3[x,y]
deffunc H2( set ) -> set = x `1 ;
deffunc H3( set ) -> set = h . $1;
defpred S4[ set ] means $1 = x `2 ;
consider g being Function such that
A10: ( dom g = dom F & ( for u being set st u in dom F holds
( ( S4[u] implies g . u = H2(u) ) & ( not S4[u] implies g . u = H3(u) ) ) ) ) from PARTFUN1:sch 1();
 reconsider y = g as set ;
take y ; :: thesis: S3[x,y]
take g ; :: thesis: ( y = g & S2[x,g] )
thus ( y = g & S2[x,g] ) by A10; :: thesis: verum
end;
consider f1 being Function such that
A11: ( dom f1 = Union (disjoin F) & ( for x being set st x in Union (disjoin F) holds
S3[x,f1 . x] ) ) from CLASSES1:sch 1(A9);
 A12: f1 is one-to-one
proof
let x be set ; :: according to FUNCT_1:def 8 :: thesis: for b1 being set holds
( not x in dom f1 or not b1 in dom f1 or not f1 . x = f1 . b1 or x = b1 )
let y be set ; :: thesis: ( not x in dom f1 or not y in dom f1 or not f1 . x = f1 . y or x = y )
assume A13: ( x in dom f1 & y in dom f1 & f1 . x = f1 . y & x <> y ) ; :: thesis: contradiction
then consider g1 being Function such that
A14: ( f1 . x = g1 & S2[x,g1] ) by A11;
consider g2 being Function such that
A15: ( f1 . y = g2 & S2[y,g2] ) by A11, A13;
A16: ( x `2 in dom F & x `1 in F . (x `2 ) & y `2 in dom F & y `1 in F . (y `2 ) ) by A11, A13, Th33;
( ex x1, x2 being set st x = [x1,x2] & ex x1, x2 being set st y = [x1,x2] ) by A11, A13, Th32;
then A17: ( x = [(x `1 ),(x `2 )] & y = [(y `1 ),(y `2 )] ) by MCART_1:8;
A18: now
assume x `1 = y `1 ; :: thesis: contradiction
then ( g1 . (x `2 ) = x `1 & g2 . (x `2 ) = h . (x `2 ) & g2 . (y `2 ) = y `1 & g1 . (y `2 ) = h . (y `2 ) & f . (y `2 ) = (G . (y `2 )) \ (F . (y `2 )) & h . (y `2 ) in f . (y `2 ) & f . (y `2 ) = f . (y `2 ) ) by A2, A5, A13, A14, A15, A16, A17;
hence contradiction by A13, A14, A15, A16, XBOOLE_0:def 5; :: thesis: verum
end;
( x `2 = y `2 implies ( g1 . (x `2 ) = x `1 & g2 . (x `2 ) = y `1 ) ) by A14, A15, A16;
then ( g1 . (y `2 ) = y `1 & g1 . (y `2 ) = h . (y `2 ) & f . (y `2 ) = (G . (y `2 )) \ (F . (y `2 )) & h . (y `2 ) in f . (y `2 ) & f . (y `2 ) = f . (y `2 ) ) by A2, A5, A13, A14, A15, A16, A18;
hence contradiction by A16, XBOOLE_0:def 5; :: thesis: verum
end;
rng f1 c= product G
proof
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in rng f1 or x in product G )
assume x in rng f1 ; :: thesis: x in product G
then consider y being set such that
A19: ( y in dom f1 & x = f1 . y ) by FUNCT_1:def 5;
consider g being Function such that
A20: ( f1 . y = g & S2[y,g] ) by A11, A19;
now
let x be set ; :: thesis: ( x in dom G implies g . x in G . x )
assume A21: x in dom G ; :: thesis: g . x in G . x
then reconsider Gx = G . x, Fx = F . x as Cardinal by A1, Def1;
Fx in Gx by A1, A21;
then ( ( y `2 = x implies g . x = y `1 ) & ( y `2 <> x implies g . x = h . x ) & h . x in f . x & f . x = Gx \ Fx & f . x = f . x & y `1 in F . (y `2 ) & Fx c= Gx & Fx = Fx ) by A1, A2, A5, A11, A19, A20, A21, Th33, CARD_1:13;
hence g . x in G . x ; :: thesis: verum
end;
hence x in product G by A1, A19, A20, Def5; :: thesis: verum
end;
then A22: Sum F c= Product G by A11, A12, CARD_1:26;
now
assume Sum F = Product G ; :: thesis: contradiction
then Union (disjoin F), product G are_equipotent by CARD_1:21;
then consider f being Function such that
A23: ( f is one-to-one & dom f = Union (disjoin F) & rng f = product G ) by WELLORD2:def 4;
deffunc H2( set ) -> Element of bool (G . $1) = (G . $1) \ (pi (f .: ((disjoin F) . $1)),$1);
consider K being Function such that
A24: ( dom K = dom F & ( for x being set st x in dom F holds
K . x = H2(x) ) ) from FUNCT_1:sch 3();
now
assume {} in rng K ; :: thesis: contradiction
then consider x being set such that
A25: ( x in dom F & {} = K . x ) by A24, FUNCT_1:def 5;
A26: K . x = (G . x) \ (pi (f .: ((disjoin F) . x)),x) by A24, A25;
reconsider Fx = F . x, Gx = G . x as Cardinal by A1, A25, Def1;
A27: ( card (pi (f .: ((disjoin F) . x)),x) c= card (f .: ((disjoin F) . x)) & card (f .: ((disjoin F) . x)) c= card ((disjoin F) . x) ) by Th31, CARD_2:3;
( card ((disjoin F) . x) = Fx & Fx in Gx ) by A1, A25, Th40;
then ( card (pi (f .: ((disjoin F) . x)),x) c= Fx & Fx in Gx & card Gx = Gx ) by A27, CARD_1:def 5, XBOOLE_1:1;
hence contradiction by A25, A26, CARD_2:4, ORDINAL1:22; :: thesis: verum
end;
then A28: product K <> {} by Th37;
consider t being Element of product K;
consider g being Function such that
A29: ( t = g & dom g = dom K & ( for x being set st x in dom K holds
g . x in K . x ) ) by A28, Def5;
now
let x be set ; :: thesis: ( x in dom K implies K . x c= G . x )
assume x in dom K ; :: thesis: K . x c= G . x
then ( K . x = (G . x) \ (pi (f .: ((disjoin F) . x)),x) & K . x = K . x & G . x = G . x ) by A24;
hence K . x c= G . x ; :: thesis: verum
end;
then product K c= product G by A1, A24, Th38;
then t in product G by A28, TARSKI:def 3;
then consider y being set such that
A30: ( y in dom f & t = f . y ) by A23, FUNCT_1:def 5;
consider X being set such that
A31: ( y in X & X in rng (disjoin F) ) by A23, A30, TARSKI:def 4;
consider x being set such that
A32: ( x in dom (disjoin F) & X = (disjoin F) . x ) by A31, FUNCT_1:def 5;
g in f .: X by A29, A30, A31, FUNCT_1:def 12;
then ( g . x in pi (f .: ((disjoin F) . x)),x & x in dom F ) by A32, Def3, Def6;
then ( not g . x in (G . x) \ (pi (f .: ((disjoin F) . x)),x) & g . x in K . x & (G . x) \ (pi (f .: ((disjoin F) . x)),x) = K . x ) by A24, A29, XBOOLE_0:def 5;
hence contradiction ; :: thesis: verum
end;
hence Sum F in Product G by A22, CARD_1:13; :: thesis: verum