let F, G be Cardinal-Function; :: thesis: ( dom F = dom G & ( for x being object 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 object st x in dom F holds
F . x in G . x ; :: thesis: Sum F in Product G
deffunc H₁( object ) -> Element of bool (G . $1) = (G . $1) \ (F . $1);
consider f being Function such that
A3: ( dom f = dom F & ( for x being object st x in dom F holds
f . x = H₁(x) ) ) from FUNCT_1:sch 3();

now :: thesis: not {} in rng f

assume {} in rng f ; :: thesis: contradiction
then consider x being object such that
A4: x in dom f and
A5: {} = f . x by FUNCT_1:def 3;
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 Th26;
set a = the Element of product f;
consider h being Function such that
the Element of product f = h and
dom h = dom f and
A8: for x being object st x in dom f holds
h . x in f . x by A7, Def5;
defpred S₂[ object , Function] means ( dom $2 = dom F & ( for x being object st x in dom F holds
( ( $1 `2 = x implies $2 . x = $1 `1 ) & ( $1 `2 <> x implies $2 . x = h . x ) ) ) );
defpred S₃[ object , object ] means ex g being Function st
( $2 = g & S₂[$1,g] );
A9: for x being object st x in Union (disjoin F) holds
ex y being object st S₃[x,y]

proof

let x be object ; :: thesis: ( x in Union (disjoin F) implies ex y being object st S₃[x,y] )
assume x in Union (disjoin F) ; :: thesis: ex y being object st S₃[x,y]
deffunc H₂( object ) -> object = x `1 ;
deffunc H<sub>3</sub>( object ) -> set = h . $1;
defpred S<sub>4</sub>[ object ] means $1 = x `2 ;
consider g being Function such that
A10: ( dom g = dom F & ( for u being object st u in dom F holds
( ( S₄[u] implies g . u = H₂(u) ) & ( not S₄[u] implies g . u = H₃(u) ) ) ) ) from PARTFUN1:sch 1();
reconsider y = g as object ;
take y ; :: thesis: S₃[x,y]
take g ; :: thesis: ( y = g & S₂[x,g] )
thus ( y = g & S₂[x,g] ) by A10; :: thesis: verum

end;

consider f1 being Function such that
A11: ( dom f1 = Union (disjoin F) & ( for x being object st x in Union (disjoin F) holds
S₃[x,f1 . x] ) ) from CLASSES1:sch 1(A9);
A12: f1 is one-to-one

proof

let x, y be object ; :: according to FUNCT_1:def 4 :: 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: S₂[x,g1] by A11, A13;
consider g2 being Function such that
A19: f1 . y = g2 and
A20: S₂[y,g2] by A11, A14;
A21: x `2 in dom F by A11, A13, Th22;
A22: y `2 in dom F by A11, A14, Th22;
A23: y `1 in F . (y `2) by A11, A14, Th22;
A24: ex x1, x2 being object st x = [x1,x2] by A11, A13, Th21;
A25: ex x1, x2 being object st y = [x1,x2] by A11, A14, Th21;
A26: x = [(x `1),(x `2)] by A24;
A27: y = [(y `1),(y `2)] by A25;

A28: now :: thesis: not x `1 = y `1

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 object ; :: 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 object such that
A37: y in dom f1 and
A38: x = f1 . y by FUNCT_1:def 3;
consider g being Function such that
A39: f1 . y = g and
A40: S₂[y,g] by A11, A37;

now :: thesis: for x being object st x in dom G holds
g . x in G . x

let x be object ; :: 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, Th22;
Fx c= Gx by A42, CARD_1:3;
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:10;

now :: thesis: not Sum F = Product G

assume Sum F = Product G ; :: thesis: contradiction
then Union (disjoin F), product G are_equipotent by CARD_1:5;
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 ;
deffunc H₂( object ) -> 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 object st x in dom F holds
K . x = H₂(x) ) ) from FUNCT_1:sch 3();

now :: thesis: not {} in rng K

assume {} in rng K ; :: thesis: contradiction
then consider x being object such that
A52: x in dom F and
A53: {} = K . x by A51, FUNCT_1:def 3;
reconsider x = x as set by TARSKI:1;
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 Th20;
A56: card (f .: ((disjoin F) . x)) c= card ((disjoin F) . x) by CARD_1:67;
card ((disjoin F) . x) = Fx by A52, Th29;
then A57: card (pi ((f .: ((disjoin F) . x)),x)) c= Fx by A55, A56;
A58: Fx in Gx by A2, A52;
card Gx = Gx ;
hence contradiction by A53, A54, A57, A58, CARD_1:68, ORDINAL1:12; :: thesis: verum

end;

then A59: product K <> {} by Th26;
set t = the Element of product K;
consider g being Function such that
A60: the Element of product K = g and
dom g = dom K and
A61: for x being object st x in dom K holds
g . x in K . x by A59, Def5;

now :: thesis: for x being object st x in dom K holds
K . x c= G . x

let x be object ; :: 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, Th27;
then the Element of product K in product G by A59;
then consider y being object such that
A62: y in dom f and
A63: the Element of product K = f . y by A50, FUNCT_1:def 3;
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 object such that
A66: x in dom (disjoin F) and
A67: X = (disjoin F) . x by A65, FUNCT_1:def 3;
reconsider x = x as set by TARSKI:1;
g in f .: X by A60, A62, A63, A64, FUNCT_1:def 6;
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:3; :: thesis: verum