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 that
A1: dom F = dom G and
A2: 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
A3: ( 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
A4: x in dom f and
A5: {} = f . x by FUNCT_1:def 5;
reconsider Fx = F . x, Gx = G . x as Cardinal by A1, A3, A4, Def1;
A6: Fx in Gx by A2, A3, A4;
not Fx in Fx ;
then Fx in Gx \ Fx by A6, XBOOLE_0:def 5;
hence contradiction by A3, A4, A5; :: thesis: verum
end;
then A7: product f <> {} by Th37;
consider a being Element of product f;
consider h being Function such that
a = h and
dom h = dom f and
A8: for x being set st x in dom f holds
h . x in f . x by A7, 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 proj1 f1 or not b1 in proj1 f1 or not f1 . x = f1 . b1 or x = b1 )
let y be set ; :: thesis: ( not x in proj1 f1 or not y in proj1 f1 or not f1 . x = f1 . y or x = y )
assume that
A13: x in dom f1 and
A14: y in dom f1 and
A15: f1 . x = f1 . y and
A16: x <> y ; :: thesis: contradiction
consider g1 being Function such that
A17: f1 . x = g1 and
A18: S2[x,g1] by A11, A13;
consider g2 being Function such that
A19: f1 . y = g2 and
A20: S2[y,g2] by A11, A14;
A21: x `2 in dom F by A11, A13, Th33;
A22: y `2 in dom F by A11, A14, Th33;
A23: y `1 in F . (y `2 ) by A11, A14, Th33;
A24: ex x1, x2 being set st x = [x1,x2] by A11, A13, Th32;
A25: ex x1, x2 being set st y = [x1,x2] by A11, A14, Th32;
A26: x = [(x `1 ),(x `2 )] by A24, MCART_1:8;
A27: y = [(y `1 ),(y `2 )] by A25, MCART_1:8;
A28: now
assume A29: x `1 = y `1 ; :: thesis: contradiction
A30: g2 . (y `2 ) = y `1 by A20, A22;
A31: g1 . (y `2 ) = h . (y `2 ) by A16, A18, A22, A26, A27, A29;
A32: f . (y `2 ) = (G . (y `2 )) \ (F . (y `2 )) by A3, A22;
h . (y `2 ) in f . (y `2 ) by A3, A8, A22;
hence contradiction by A15, A17, A19, A23, A30, A31, A32, XBOOLE_0:def 5; :: thesis: verum
end;
A33: ( x `2 = y `2 implies ( g1 . (x `2 ) = x `1 & g2 . (x `2 ) = y `1 ) ) by A18, A20, A21;
A34: g1 . (y `2 ) = y `1 by A15, A17, A19, A20, A22;
A35: g1 . (y `2 ) = h . (y `2 ) by A15, A17, A18, A19, A22, A28, A33;
A36: f . (y `2 ) = (G . (y `2 )) \ (F . (y `2 )) by A3, A22;
h . (y `2 ) in f . (y `2 ) by A3, A8, A22;
hence contradiction by A23, A34, A35, A36, 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
A37: y in dom f1 and
A38: x = f1 . y by FUNCT_1:def 5;
consider g being Function such that
A39: f1 . y = g and
A40: S2[y,g] by A11, A37;
now
let x be set ; :: thesis: ( x in dom G implies g . x in G . x )
assume A41: x in dom G ; :: thesis: g . x in G . x
then reconsider Gx = G . x, Fx = F . x as Cardinal by A1, Def1;
A42: Fx in Gx by A1, A2, A41;
A43: ( y `2 = x implies g . x = y `1 ) by A1, A40, A41;
A44: ( y `2 <> x implies g . x = h . x ) by A1, A40, A41;
A45: h . x in f . x by A1, A3, A8, A41;
A46: f . x = Gx \ Fx by A1, A3, A41;
A47: y `1 in F . (y `2 ) by A11, A37, Th33;
Fx c= Gx by A42, CARD_1:13;
hence g . x in G . x by A43, A44, A45, A46, A47; :: thesis: verum
end;
hence x in product G by A1, A38, A39, A40, Def5; :: thesis: verum
end;
then A48: 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
f is one-to-one and
A49: dom f = Union (disjoin F) and
A50: 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
A51: ( 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
A52: x in dom F and
A53: {} = K . x by A51, FUNCT_1:def 5;
A54: K . x = (G . x) \ (pi (f .: ((disjoin F) . x)),x) by A51, A52;
reconsider Fx = F . x, Gx = G . x as Cardinal by A1, A52, Def1;
A55: card (pi (f .: ((disjoin F) . x)),x) c= card (f .: ((disjoin F) . x)) by Th31;
A56: card (f .: ((disjoin F) . x)) c= card ((disjoin F) . x) by CARD_2:3;
card ((disjoin F) . x) = Fx by A52, Th40;
then A57: card (pi (f .: ((disjoin F) . x)),x) c= Fx by A55, A56, XBOOLE_1:1;
A58: Fx in Gx by A2, A52;
card Gx = Gx by CARD_1:def 5;
hence contradiction by A53, A54, A57, A58, CARD_2:4, ORDINAL1:22; :: thesis: verum
end;
then A59: product K <> {} by Th37;
consider t being Element of product K;
consider g being Function such that
A60: t = g and
dom g = dom K and
A61: for x being set st x in dom K holds
g . x in K . x by A59, 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) by A51;
hence K . x c= G . x ; :: thesis: verum
end;
then product K c= product G by A1, A51, Th38;
then t in product G by A59, TARSKI:def 3;
then consider y being set such that
A62: y in dom f and
A63: t = f . y by A50, FUNCT_1:def 5;
consider X being set such that
A64: y in X and
A65: X in rng (disjoin F) by A49, A62, TARSKI:def 4;
consider x being set such that
A66: x in dom (disjoin F) and
A67: X = (disjoin F) . x by A65, FUNCT_1:def 5;
g in f .: X by A60, A62, A63, A64, FUNCT_1:def 12;
then A68: g . x in pi (f .: ((disjoin F) . x)),x by A67, Def6;
A69: x in dom F by A66, Def3;
A70: not g . x in (G . x) \ (pi (f .: ((disjoin F) . x)),x) by A68, XBOOLE_0:def 5;
g . x in K . x by A51, A61, A69;
hence contradiction by A51, A69, A70; :: thesis: verum
end;
hence Sum F in Product G by A48, CARD_1:13; :: thesis: verum