:: CARD_3 semantic presentation

begin


definition
let IT be Function;
attrIT is Cardinal-yielding  means :Def1: :: CARD_3:def 1
 for x being set st x in dom IT holds
IT . x is Cardinal;
end;

:: deftheorem Def1 defines Cardinal-yielding CARD_3:def_1_:_
 for IT being Function holds
( IT is Cardinal-yielding iff for x being set st x in dom IT holds
IT . x is Cardinal );

registration
cluster empty Relation-like Function-like  ->  Cardinal-yielding for set ;
coherence
 for b1 being Function st b1 is empty holds
b1 is Cardinal-yielding
proof
let f be Function; ::_thesis: ( f is empty implies f is Cardinal-yielding )
assume A1: f is empty ; ::_thesis: f is Cardinal-yielding
let x be set ; :: according to CARD_3:def_1 ::_thesis: ( x in dom f implies f . x is Cardinal )
thus  ( x in dom f implies f . x is Cardinal ) by A1; ::_thesis: verum
end;
end;

registration
cluster Relation-like Function-like Cardinal-yielding for set ;
existence
 ex b1 being Function st b1 is Cardinal-yielding
proof
take  {} ; ::_thesis: {} is Cardinal-yielding
thus  {} is Cardinal-yielding ; ::_thesis: verum
end;
end;

definition
mode Cardinal-Function is Cardinal-yielding Function;
end;

registration
let ff be Cardinal-Function;
let X be set ;
clusterff | X ->  Cardinal-yielding ;
coherence
 ff | X is Cardinal-yielding
proof
 ff | X is Cardinal-yielding
proof
let x be set ; :: according to CARD_3:def_1 ::_thesis: ( x in dom (ff | X) implies (ff | X) . x is Cardinal )
assume A1: x in dom (ff | X) ; ::_thesis: (ff | X) . x is Cardinal
then A2: (ff | X) . x = ff . x by FUNCT_1:47;
 dom (ff | X) = (dom ff) /\ X by RELAT_1:61;
then  x in dom ff by A1, XBOOLE_0:def_4;
hence  (ff | X) . x is Cardinal by A2, Def1; ::_thesis: verum
end;
hence  ff | X is Cardinal-yielding ; ::_thesis: verum
end;
end;

registration
let X be set ;
let K be Cardinal;
clusterX --> K ->  Cardinal-yielding ;
coherence
 X --> K is Cardinal-yielding
proof
let x be set ; :: according to CARD_3:def_1 ::_thesis: ( x in dom (X --> K) implies (X --> K) . x is Cardinal )
assume  x in dom (X --> K) ; ::_thesis: (X --> K) . x is Cardinal
hence  (X --> K) . x is Cardinal by FUNCOP_1:7; ::_thesis: verum
end;
end;

registration
let X be set ;
let K be Cardinal;
clusterX .--> K ->  Cardinal-yielding ;
coherence
 X .--> K is Cardinal-yielding ;
end;

scheme :: CARD_3:sch 1
CFLambda{ F1() ->  set , F2( set ) ->  Cardinal } :
 ex ff being Cardinal-Function st
( dom ff = F1() & ( for x being set st x in F1() holds
ff . x = F2(x) ) )
proof
consider f being Function such that
A1: ( dom f = F1() & ( for x being set st x in F1() holds
f . x = F2(x) ) ) from FUNCT_1:sch_3();
 f is Cardinal-yielding
proof
let x be set ; :: according to CARD_3:def_1 ::_thesis: ( x in dom f implies f . x is Cardinal )
assume  x in dom f ; ::_thesis: f . x is Cardinal
then  f . x = F2(x) by A1;
hence  f . x is Cardinal ; ::_thesis: verum
end;
then reconsider f = f as Cardinal-Function ;
take  f ; ::_thesis: ( dom f = F1() & ( for x being set st x in F1() holds
f . x = F2(x) ) )
thus  ( dom f = F1() & ( for x being set st x in F1() holds
f . x = F2(x) ) ) by A1; ::_thesis: verum
end;

definition
let f be Function;
func Card f ->  Cardinal-Function means :Def2: :: CARD_3:def 2
( dom it = dom f & ( for x being set st x in dom f holds
it . x = card (f . x) ) );
existence
 ex b1 being Cardinal-Function st
( dom b1 = dom f & ( for x being set st x in dom f holds
b1 . x = card (f . x) ) )
proof
deffunc H1( set ) ->  set = card (f . $1);
thus  ex g being Cardinal-Function st
( dom g = dom f & ( for x being set st x in dom f holds
g . x = H1(x) ) ) from CARD_3:sch_1(); ::_thesis: verum
end;
uniqueness
 for b1, b2 being Cardinal-Function st dom b1 = dom f & ( for x being set st x in dom f holds
b1 . x = card (f . x) ) & dom b2 = dom f & ( for x being set st x in dom f holds
b2 . x = card (f . x) ) holds
b1 = b2
proof
let a1, a2 be Cardinal-Function; ::_thesis: ( dom a1 = dom f & ( for x being set st x in dom f holds
a1 . x = card (f . x) ) & dom a2 = dom f & ( for x being set st x in dom f holds
a2 . x = card (f . x) ) implies a1 = a2 )
assume that
A1: dom a1 = dom f and
A2: for x being set st x in dom f holds
a1 . x = card (f . x) and
A3: dom a2 = dom f and
A4: for x being set st x in dom f holds
a2 . x = card (f . x) ; ::_thesis: a1 = a2
now__::_thesis:_for_x_being_set_st_x_in_dom_f_holds_
a1_._x_=_a2_._x
let x be set ; ::_thesis: ( x in dom f implies a1 . x = a2 . x )
assume A5: x in dom f ; ::_thesis: a1 . x = a2 . x
then  a1 . x = card (f . x) by A2;
hence  a1 . x = a2 . x by A4, A5; ::_thesis: verum
end;
hence  a1 = a2 by A1, A3, FUNCT_1:2; ::_thesis: verum
end;
func disjoin f ->  Function means :Def3: :: CARD_3:def 3
( dom it = dom f & ( for x being set st x in dom f holds
it . x = [:(f . x),{x}:] ) );
existence
 ex b1 being Function st
( dom b1 = dom f & ( for x being set st x in dom f holds
b1 . x = [:(f . x),{x}:] ) )
proof
deffunc H1( set ) ->  set = [:(f . $1),{$1}:];
thus  ex g being Function st
( dom g = dom f & ( for x being set st x in dom f holds
g . x = H1(x) ) ) from FUNCT_1:sch_3(); ::_thesis: verum
end;
uniqueness
 for b1, b2 being Function st dom b1 = dom f & ( for x being set st x in dom f holds
b1 . x = [:(f . x),{x}:] ) & dom b2 = dom f & ( for x being set st x in dom f holds
b2 . x = [:(f . x),{x}:] ) holds
b1 = b2
proof
let a1, a2 be Function; ::_thesis: ( dom a1 = dom f & ( for x being set st x in dom f holds
a1 . x = [:(f . x),{x}:] ) & dom a2 = dom f & ( for x being set st x in dom f holds
a2 . x = [:(f . x),{x}:] ) implies a1 = a2 )
assume that
A6: dom a1 = dom f and
A7: for x being set st x in dom f holds
a1 . x = [:(f . x),{x}:] and
A8: dom a2 = dom f and
A9: for x being set st x in dom f holds
a2 . x = [:(f . x),{x}:] ; ::_thesis: a1 = a2
now__::_thesis:_for_x_being_set_st_x_in_dom_f_holds_
a1_._x_=_a2_._x
let x be set ; ::_thesis: ( x in dom f implies a1 . x = a2 . x )
assume A10: x in dom f ; ::_thesis: a1 . x = a2 . x
then  a1 . x = [:(f . x),{x}:] by A7;
hence  a1 . x = a2 . x by A9, A10; ::_thesis: verum
end;
hence  a1 = a2 by A6, A8, FUNCT_1:2; ::_thesis: verum
end;
func Union f ->  set  equals :: CARD_3:def 4
 union (rng f);
correctness
coherence
union (rng f) is set ;
;
defpred S1[ set ] means  ex g being Function st
( $1 = g & dom g = dom f & ( for x being set st x in dom f holds
g . x in f . x ) );
func product f ->  set  means :Def5: :: CARD_3:def 5
 for x being set holds
( x in it iff ex g being Function st
( x = g & dom g = dom f & ( for y being set st y in dom f holds
g . y in f . y ) ) );
existence
 ex b1 being set st
for x being set holds
( x in b1 iff ex g being Function st
( x = g & dom g = dom f & ( for y being set st y in dom f holds
g . y in f . y ) ) )
proof
consider X being set  such that
A11: for x being set holds
( x in X iff ( x in Funcs ((dom f),(union (rng f))) & S1[x] ) ) from XBOOLE_0:sch_1();
take  X ; ::_thesis: for x being set holds
( x in X iff ex g being Function st
( x = g & dom g = dom f & ( for y being set st y in dom f holds
g . y in f . y ) ) )
let x be set ; ::_thesis: ( x in X iff ex g being Function st
( x = g & dom g = dom f & ( for y being set st y in dom f holds
g . y in f . y ) ) )
thus  ( x in X implies ex g being Function st
( x = g & dom g = dom f & ( for x being set st x in dom f holds
g . x in f . x ) ) ) by A11; ::_thesis: ( ex g being Function st
( x = g & dom g = dom f & ( for y being set st y in dom f holds
g . y in f . y ) ) implies x in X )
given g being Function such that A12: x = g and
A13: dom g = dom f and
A14: for x being set st x in dom f holds
g . x in f . x ; ::_thesis: x in X
 rng g c= union (rng f)
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng g or y in union (rng f) )
assume  y in rng g ; ::_thesis: y in union (rng f)
then consider z being set  such that
A15: z in dom g and
A16: y = g . z by FUNCT_1:def_3;
A17: y in f . z by A13, A14, A15, A16;
 f . z in rng f by A13, A15, FUNCT_1:def_3;
hence  y in union (rng f) by A17, TARSKI:def_4; ::_thesis: verum
end;
then  x in Funcs ((dom f),(union (rng f))) by A12, A13, FUNCT_2:def_2;
hence  x in X by A11, A12, A13, A14; ::_thesis: verum
end;
uniqueness
 for b1, b2 being set st ( for x being set holds
( x in b1 iff ex g being Function st
( x = g & dom g = dom f & ( for y being set st y in dom f holds
g . y in f . y ) ) ) ) & ( for x being set holds
( x in b2 iff ex g being Function st
( x = g & dom g = dom f & ( for y being set st y in dom f holds
g . y in f . y ) ) ) ) holds
b1 = b2
proof
let X1, X2 be set ; ::_thesis: ( ( for x being set holds
( x in X1 iff ex g being Function st
( x = g & dom g = dom f & ( for y being set st y in dom f holds
g . y in f . y ) ) ) ) & ( for x being set holds
( x in X2 iff ex g being Function st
( x = g & dom g = dom f & ( for y being set st y in dom f holds
g . y in f . y ) ) ) ) implies X1 = X2 )
assume that
A18: for x being set holds
( x in X1 iff S1[x] ) and
A19: for x being set holds
( x in X2 iff S1[x] ) ; ::_thesis: X1 = X2
thus  X1 = X2 from XBOOLE_0:sch_2(A18, A19); ::_thesis: verum
end;
end;

:: deftheorem Def2 defines Card CARD_3:def_2_:_
 for f being Function
for b2 being Cardinal-Function holds
( b2 = Card f iff ( dom b2 = dom f & ( for x being set st x in dom f holds
b2 . x = card (f . x) ) ) );

:: deftheorem Def3 defines disjoin CARD_3:def_3_:_
 for f, b2 being Function holds
( b2 = disjoin f iff ( dom b2 = dom f & ( for x being set st x in dom f holds
b2 . x = [:(f . x),{x}:] ) ) );

:: deftheorem  defines Union CARD_3:def_4_:_
 for f being Function holds Union f = union (rng f);

:: deftheorem Def5 defines product CARD_3:def_5_:_
 for f being Function
for b2 being set holds
( b2 = product f iff for x being set holds
( x in b2 iff ex g being Function st
( x = g & dom g = dom f & ( for y being set st y in dom f holds
g . y in f . y ) ) ) );

theorem Th1: :: CARD_3:1
for ff being Cardinal-Function holds Card ff = ff
proof
let ff be Cardinal-Function; ::_thesis: Card ff = ff
now__::_thesis:_for_x_being_set_st_x_in_dom_ff_holds_
ff_._x_=_card_(ff_._x)
let x be set ; ::_thesis: ( x in dom ff implies ff . x = card (ff . x) )
assume  x in dom ff ; ::_thesis: ff . x = card (ff . x)
then reconsider M = ff . x as Cardinal by Def1;
 card M = M by CARD_1:def_2;
hence  ff . x = card (ff . x) ; ::_thesis: verum
end;
hence  Card ff = ff by Def2; ::_thesis: verum
end;

theorem :: CARD_3:2
for X, Y being set holds Card (X --> Y) = X --> (card Y)
proof
let X, Y be set ; ::_thesis: Card (X --> Y) = X --> (card Y)
A1: dom (Card (X --> Y)) = dom (X --> Y) by Def2;
then A2: dom (Card (X --> Y)) = X by FUNCOP_1:13;
A3: dom (X --> (card Y)) = X by FUNCOP_1:13;
now__::_thesis:_for_x_being_set_st_x_in_X_holds_
(Card_(X_-->_Y))_._x_=_(X_-->_(card_Y))_._x
let x be set ; ::_thesis: ( x in X implies (Card (X --> Y)) . x = (X --> (card Y)) . x )
assume A4: x in X ; ::_thesis: (Card (X --> Y)) . x = (X --> (card Y)) . x
then A5: (Card (X --> Y)) . x = card ((X --> Y) . x) by A1, A2, Def2;
 (X --> (card Y)) . x = card Y by A4, FUNCOP_1:7;
hence  (Card (X --> Y)) . x = (X --> (card Y)) . x by A4, A5, FUNCOP_1:7; ::_thesis: verum
end;
hence  Card (X --> Y) = X --> (card Y) by A2, A3, FUNCT_1:2; ::_thesis: verum
end;

theorem :: CARD_3:3
disjoin {} = {}
proof
 dom (disjoin {}) = {} by Def3, RELAT_1:38;
hence  disjoin {} = {} ; ::_thesis: verum
end;

theorem Th4: :: CARD_3:4
for x, X being set holds disjoin (x .--> X) = x .--> [:X,{x}:]
proof
let x, X be set ; ::_thesis: disjoin (x .--> X) = x .--> [:X,{x}:]
A1: dom (disjoin ({x} --> X)) = dom ({x} --> X) by Def3;
A2: dom ({x} --> X) = {x} by FUNCOP_1:13;
A3: dom ({x} --> [:X,{x}:]) = {x} by FUNCOP_1:13;
now__::_thesis:_for_y_being_set_st_y_in_{x}_holds_
(disjoin_({x}_-->_X))_._y_=_({x}_-->_[:X,{x}:])_._y
let y be set ; ::_thesis: ( y in {x} implies (disjoin ({x} --> X)) . y = ({x} --> [:X,{x}:]) . y )
assume A4: y in {x} ; ::_thesis: (disjoin ({x} --> X)) . y = ({x} --> [:X,{x}:]) . y
then A5: (disjoin ({x} --> X)) . y = [:(({x} --> X) . y),{y}:] by A2, Def3;
A6: ({x} --> X) . y = X by A4, FUNCOP_1:7;
 ({x} --> [:X,{x}:]) . y = [:X,{x}:] by A4, FUNCOP_1:7;
hence  (disjoin ({x} --> X)) . y = ({x} --> [:X,{x}:]) . y by A4, A5, A6, TARSKI:def_1; ::_thesis: verum
end;
hence  disjoin (x .--> X) = x .--> [:X,{x}:] by A1, A2, A3, FUNCT_1:2; ::_thesis: verum
end;

theorem :: CARD_3:5
for x, y being set
for f being Function st x in dom f & y in dom f & x <> y holds
(disjoin f) . x misses (disjoin f) . y
proof
let x, y be set ; ::_thesis: for f being Function st x in dom f & y in dom f & x <> y holds
(disjoin f) . x misses (disjoin f) . y
let f be Function; ::_thesis: ( x in dom f & y in dom f & x <> y implies (disjoin f) . x misses (disjoin f) . y )
assume that
A1: x in dom f and
A2: y in dom f and
A3: x <> y ; ::_thesis: (disjoin f) . x misses (disjoin f) . y
set z = the Element of ((disjoin f) . x) /\ ((disjoin f) . y);
assume A4: ((disjoin f) . x) /\ ((disjoin f) . y) <> {} ; :: according to XBOOLE_0:def_7 ::_thesis: contradiction
A5: (disjoin f) . x = [:(f . x),{x}:] by A1, Def3;
A6: (disjoin f) . y = [:(f . y),{y}:] by A2, Def3;
A7: the Element of ((disjoin f) . x) /\ ((disjoin f) . y) in (disjoin f) . x by A4, XBOOLE_0:def_4;
A8: the Element of ((disjoin f) . x) /\ ((disjoin f) . y) in (disjoin f) . y by A4, XBOOLE_0:def_4;
A9: the Element of ((disjoin f) . x) /\ ((disjoin f) . y) `2 in {x} by A5, A7, MCART_1:10;
A10: the Element of ((disjoin f) . x) /\ ((disjoin f) . y) `2 in {y} by A6, A8, MCART_1:10;
 the Element of ((disjoin f) . x) /\ ((disjoin f) . y) `2 = x by A9, TARSKI:def_1;
hence  contradiction by A3, A10, TARSKI:def_1; ::_thesis: verum
end;

theorem Th6: :: CARD_3:6
for X, Y being set holds Union (X --> Y) c= Y
proof
let X, Y be set ; ::_thesis: Union (X --> Y) c= Y
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Union (X --> Y) or x in Y )
assume  x in Union (X --> Y) ; ::_thesis: x in Y
then consider Z being set  such that
A1: x in Z and
A2: Z in rng (X --> Y) by TARSKI:def_4;
 ex z being set st
( z in dom (X --> Y) & Z = (X --> Y) . z ) by A2, FUNCT_1:def_3;
hence  x in Y by A1, FUNCOP_1:7; ::_thesis: verum
end;

theorem Th7: :: CARD_3:7
for X, Y being set st X <> {} holds
Union (X --> Y) = Y
proof
let X, Y be set ; ::_thesis: ( X <> {} implies Union (X --> Y) = Y )
assume A1: X <> {} ; ::_thesis: Union (X --> Y) = Y
set x = the Element of X;
thus  Union (X --> Y) c= Y by Th6; :: according to XBOOLE_0:def_10 ::_thesis: Y c= Union (X --> Y)
A2: dom (X --> Y) = X by FUNCOP_1:13;
 (X --> Y) . the Element of X = Y by A1, FUNCOP_1:7;
then  Y in rng (X --> Y) by A1, A2, FUNCT_1:def_3;
hence  Y c= Union (X --> Y) by ZFMISC_1:74; ::_thesis: verum
end;

theorem :: CARD_3:8
for x, Y being set holds Union (x .--> Y) = Y by Th7;

theorem Th9: :: CARD_3:9
for g, f being Function holds
( g in product f iff ( dom g = dom f & ( for x being set st x in dom f holds
g . x in f . x ) ) )
proof
let g, f be Function; ::_thesis: ( g in product f iff ( dom g = dom f & ( for x being set st x in dom f holds
g . x in f . x ) ) )
thus  ( g in product f implies ( dom g = dom f & ( for x being set st x in dom f holds
g . x in f . x ) ) ) ::_thesis: ( dom g = dom f & ( for x being set st x in dom f holds
g . x in f . x ) implies g in product f )
proof
assume  g in product f ; ::_thesis: ( dom g = dom f & ( for x being set st x in dom f holds
g . x in f . x ) )
then  ex h being Function st
( g = h & dom h = dom f & ( for x being set st x in dom f holds
h . x in f . x ) ) by Def5;
hence  ( dom g = dom f & ( for x being set st x in dom f holds
g . x in f . x ) ) ; ::_thesis: verum
end;
thus  ( dom g = dom f & ( for x being set st x in dom f holds
g . x in f . x ) implies g in product f ) by Def5; ::_thesis: verum
end;

theorem Th10: :: CARD_3:10
product {} = {{}}
proof
thus  product {} c= {{}} :: according to XBOOLE_0:def_10 ::_thesis: {{}} c= product {}
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in product {} or x in {{}} )
assume  x in product {} ; ::_thesis: x in {{}}
then  ex g being Function st
( x = g & dom g = dom {} & ( for y being set st y in dom {} holds
g . y in {} . y ) ) by Def5;
then  x = {} ;
hence  x in {{}} by TARSKI:def_1; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {{}} or x in product {} )
assume  x in {{}} ; ::_thesis: x in product {}
then A1: x = {} by TARSKI:def_1;
 for y being set st y in dom {} holds
{} . y in {} . y ;
hence  x in product {} by A1, Th9; ::_thesis: verum
end;

theorem Th11: :: CARD_3:11
for X, Y being set holds Funcs (X,Y) = product (X --> Y)
proof
let X, Y be set ; ::_thesis: Funcs (X,Y) = product (X --> Y)
set f = X --> Y;
A1: dom (X --> Y) = X by FUNCOP_1:13;
thus  Funcs (X,Y) c= product (X --> Y) :: according to XBOOLE_0:def_10 ::_thesis: product (X --> Y) c= Funcs (X,Y)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Funcs (X,Y) or x in product (X --> Y) )
assume  x in Funcs (X,Y) ; ::_thesis: x in product (X --> Y)
then consider g being Function such that
A2: x = g and
A3: dom g = X and
A4: rng g c= Y by FUNCT_2:def_2;
now__::_thesis:_for_y_being_set_st_y_in_dom_(X_-->_Y)_holds_
g_._y_in_(X_-->_Y)_._y
let y be set ; ::_thesis: ( y in dom (X --> Y) implies g . y in (X --> Y) . y )
assume A5: y in dom (X --> Y) ; ::_thesis: g . y in (X --> Y) . y
then A6: (X --> Y) . y = Y by FUNCOP_1:7;
 g . y in rng g by A3, A5, FUNCT_1:def_3;
hence  g . y in (X --> Y) . y by A4, A6; ::_thesis: verum
end;
hence  x in product (X --> Y) by A1, A2, A3, Def5; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in product (X --> Y) or x in Funcs (X,Y) )
assume  x in product (X --> Y) ; ::_thesis: x in Funcs (X,Y)
then consider g being Function such that
A7: x = g and
A8: dom g = dom (X --> Y) and
A9: for x being set st x in dom (X --> Y) holds
g . x in (X --> Y) . x by Def5;
 rng g c= Y
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng g or y in Y )
assume  y in rng g ; ::_thesis: y in Y
then consider z being set  such that
A10: z in dom g and
A11: y = g . z by FUNCT_1:def_3;
 y in (X --> Y) . z by A8, A9, A10, A11;
hence  y in Y by A8, A10, FUNCOP_1:7; ::_thesis: verum
end;
hence  x in Funcs (X,Y) by A1, A7, A8, FUNCT_2:def_2; ::_thesis: verum
end;

defpred S1[ set ] means $1 is Function;

definition
let x, X be set ;
defpred S2[ set , set ] means  ex g being Function st
( $1 = g & $2 = g . x );
func pi (X,x) ->  set  means :Def6: :: CARD_3:def 6
 for y being set holds
( y in it iff ex f being Function st
( f in X & y = f . x ) );
existence
 ex b1 being set st
for y being set holds
( y in b1 iff ex f being Function st
( f in X & y = f . x ) )
proof
consider Y being set  such that
A1: for y being set holds
( y in Y iff ( y in X & S1[y] ) ) from XBOOLE_0:sch_1();
A2: for y being set st y in Y holds
ex z being set st S2[y,z]
proof
let y be set ; ::_thesis: ( y in Y implies ex z being set st S2[y,z] )
assume  y in Y ; ::_thesis: ex z being set st S2[y,z]
then reconsider y = y as Function by A1;
take  y . x ; ::_thesis: S2[y,y . x]
take  y ; ::_thesis: ( y = y & y . x = y . x )
thus  ( y = y & y . x = y . x ) ; ::_thesis: verum
end;
consider f being Function such that
A3: ( dom f = Y & ( for y being set st y in Y holds
S2[y,f . y] ) ) from CLASSES1:sch_1(A2);
take  rng f ; ::_thesis: for y being set holds
( y in rng f iff ex f being Function st
( f in X & y = f . x ) )
let y be set ; ::_thesis: ( y in rng f iff ex f being Function st
( f in X & y = f . x ) )
thus  ( y in rng f implies ex f being Function st
( f in X & y = f . x ) ) ::_thesis: ( ex f being Function st
( f in X & y = f . x ) implies y in rng f )
proof
assume  y in rng f ; ::_thesis: ex f being Function st
( f in X & y = f . x )
then consider z being set  such that
A4: z in dom f and
A5: y = f . z by FUNCT_1:def_3;
consider g being Function such that
A6: z = g and
A7: f . z = g . x by A3, A4;
take  g ; ::_thesis: ( g in X & y = g . x )
thus  ( g in X & y = g . x ) by A1, A3, A4, A5, A6, A7; ::_thesis: verum
end;
given g being Function such that A8: g in X and
A9: y = g . x ; ::_thesis: y in rng f
A10: g in Y by A1, A8;
then  ex f1 being Function st
( g = f1 & f . g = f1 . x ) by A3;
hence  y in rng f by A3, A9, A10, FUNCT_1:def_3; ::_thesis: verum
end;
uniqueness
 for b1, b2 being set st ( for y being set holds
( y in b1 iff ex f being Function st
( f in X & y = f . x ) ) ) & ( for y being set holds
( y in b2 iff ex f being Function st
( f in X & y = f . x ) ) ) holds
b1 = b2
proof
defpred S3[ set ] means  ex f being Function st
( f in X & $1 = f . x );
let X1, X2 be set ; ::_thesis: ( ( for y being set holds
( y in X1 iff ex f being Function st
( f in X & y = f . x ) ) ) & ( for y being set holds
( y in X2 iff ex f being Function st
( f in X & y = f . x ) ) ) implies X1 = X2 )
assume that
A11: for y being set holds
( y in X1 iff S3[y] ) and
A12: for y being set holds
( y in X2 iff S3[y] ) ; ::_thesis: X1 = X2
thus  X1 = X2 from XBOOLE_0:sch_2(A11, A12); ::_thesis: verum
end;
end;

:: deftheorem Def6 defines pi CARD_3:def_6_:_
 for x, X, b3 being set holds
( b3 = pi (X,x) iff for y being set holds
( y in b3 iff ex f being Function st
( f in X & y = f . x ) ) );

theorem :: CARD_3:12
for x being set
for f being Function st x in dom f & product f <> {} holds
pi ((product f),x) = f . x
proof
let x be set ; ::_thesis: for f being Function st x in dom f & product f <> {} holds
pi ((product f),x) = f . x
let f be Function; ::_thesis: ( x in dom f & product f <> {} implies pi ((product f),x) = f . x )
assume that
A1: x in dom f and
A2: product f <> {} ; ::_thesis: pi ((product f),x) = f . x
A3: pi ((product f),x) c= f . x
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in pi ((product f),x) or y in f . x )
assume  y in pi ((product f),x) ; ::_thesis: y in f . x
then  ex g being Function st
( g in product f & y = g . x ) by Def6;
hence  y in f . x by A1, Th9; ::_thesis: verum
end;
 f . x c= pi ((product f),x)
proof
set z = the Element of product f;
consider g being Function such that
 the Element of product f = g and
A4: dom g = dom f and
A5: for x being set st x in dom f holds
g . x in f . x by A2, Def5;
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in f . x or y in pi ((product f),x) )
deffunc H1( set ) ->  set = y;
deffunc H2( set ) ->  set = g . $1;
defpred S2[ set ] means x = $1;
consider h being Function such that
A6: ( dom h = dom g & ( for z being set st z in dom g holds
( ( S2[z] implies h . z = H1(z) ) & ( not S2[z] implies h . z = H2(z) ) ) ) ) from PARTFUN1:sch_1();
assume A7: y in f . x ; ::_thesis: y in pi ((product f),x)
now__::_thesis:_for_z_being_set_st_z_in_dom_f_holds_
h_._z_in_f_._z
let z be set ; ::_thesis: ( z in dom f implies h . z in f . z )
assume A8: z in dom f ; ::_thesis: h . z in f . z
then  ( x <> z implies g . z = h . z ) by A4, A6;
hence  h . z in f . z by A4, A5, A6, A7, A8; ::_thesis: verum
end;
then A9: h in product f by A4, A6, Th9;
 h . x = y by A1, A4, A6;
hence  y in pi ((product f),x) by A9, Def6; ::_thesis: verum
end;
hence  pi ((product f),x) = f . x by A3, XBOOLE_0:def_10; ::_thesis: verum
end;

theorem :: CARD_3:13
for x being set holds pi ({},x) = {}
proof
let x be set ; ::_thesis: pi ({},x) = {}
set y = the Element of pi ({},x);
assume  not pi ({},x) = {} ; ::_thesis: contradiction
then  ex f being Function st
( f in {} & the Element of pi ({},x) = f . x ) by Def6;
hence  contradiction ; ::_thesis: verum
end;

theorem :: CARD_3:14
for x being set
for g being Function holds pi ({g},x) = {(g . x)}
proof
let x be set ; ::_thesis: for g being Function holds pi ({g},x) = {(g . x)}
let g be Function; ::_thesis: pi ({g},x) = {(g . x)}
thus  pi ({g},x) c= {(g . x)} :: according to XBOOLE_0:def_10 ::_thesis: {(g . x)} c= pi ({g},x)
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in pi ({g},x) or y in {(g . x)} )
assume  y in pi ({g},x) ; ::_thesis: y in {(g . x)}
then consider f being Function such that
A1: f in {g} and
A2: y = f . x by Def6;
 f = g by A1, TARSKI:def_1;
hence  y in {(g . x)} by A2, TARSKI:def_1; ::_thesis: verum
end;
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in {(g . x)} or y in pi ({g},x) )
assume A3: y in {(g . x)} ; ::_thesis: y in pi ({g},x)
A4: g in {g} by TARSKI:def_1;
 y = g . x by A3, TARSKI:def_1;
hence  y in pi ({g},x) by A4, Def6; ::_thesis: verum
end;

theorem :: CARD_3:15
for x being set
for f, g being Function holds pi ({f,g},x) = {(f . x),(g . x)}
proof
let x be set ; ::_thesis: for f, g being Function holds pi ({f,g},x) = {(f . x),(g . x)}
let f, g be Function; ::_thesis: pi ({f,g},x) = {(f . x),(g . x)}
thus  pi ({f,g},x) c= {(f . x),(g . x)} :: according to XBOOLE_0:def_10 ::_thesis: {(f . x),(g . x)} c= pi ({f,g},x)
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in pi ({f,g},x) or y in {(f . x),(g . x)} )
assume  y in pi ({f,g},x) ; ::_thesis: y in {(f . x),(g . x)}
then consider f1 being Function such that
A1: f1 in {f,g} and
A2: y = f1 . x by Def6;
 ( f1 = f or f1 = g ) by A1, TARSKI:def_2;
hence  y in {(f . x),(g . x)} by A2, TARSKI:def_2; ::_thesis: verum
end;
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in {(f . x),(g . x)} or y in pi ({f,g},x) )
assume A3: y in {(f . x),(g . x)} ; ::_thesis: y in pi ({f,g},x)
A4: f in {f,g} by TARSKI:def_2;
A5: g in {f,g} by TARSKI:def_2;
 ( y = g . x or y = f . x ) by A3, TARSKI:def_2;
hence  y in pi ({f,g},x) by A4, A5, Def6; ::_thesis: verum
end;

theorem Th16: :: CARD_3:16
for X, Y, x being set holds pi ((X \/ Y),x) = (pi (X,x)) \/ (pi (Y,x))
proof
let X, Y, x be set ; ::_thesis: pi ((X \/ Y),x) = (pi (X,x)) \/ (pi (Y,x))
thus  pi ((X \/ Y),x) c= (pi (X,x)) \/ (pi (Y,x)) :: according to XBOOLE_0:def_10 ::_thesis: (pi (X,x)) \/ (pi (Y,x)) c= pi ((X \/ Y),x)
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in pi ((X \/ Y),x) or y in (pi (X,x)) \/ (pi (Y,x)) )
assume  y in pi ((X \/ Y),x) ; ::_thesis: y in (pi (X,x)) \/ (pi (Y,x))
then consider f being Function such that
A1: f in X \/ Y and
A2: y = f . x by Def6;
 ( f in X or f in Y ) by A1, XBOOLE_0:def_3;
then  ( y in pi (X,x) or y in pi (Y,x) ) by A2, Def6;
hence  y in (pi (X,x)) \/ (pi (Y,x)) by XBOOLE_0:def_3; ::_thesis: verum
end;
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in (pi (X,x)) \/ (pi (Y,x)) or y in pi ((X \/ Y),x) )
assume  y in (pi (X,x)) \/ (pi (Y,x)) ; ::_thesis: y in pi ((X \/ Y),x)
then A3: ( y in pi (X,x) or y in pi (Y,x) ) by XBOOLE_0:def_3;
A4: now__::_thesis:_(_y_in_pi_(X,x)_implies_y_in_pi_((X_\/_Y),x)_)
assume  y in pi (X,x) ; ::_thesis: y in pi ((X \/ Y),x)
then consider f being Function such that
A5: f in X and
A6: y = f . x by Def6;
 f in X \/ Y by A5, XBOOLE_0:def_3;
hence  y in pi ((X \/ Y),x) by A6, Def6; ::_thesis: verum
end;
now__::_thesis:_(_not_y_in_pi_(X,x)_implies_y_in_pi_((X_\/_Y),x)_)
assume  not y in pi (X,x) ; ::_thesis: y in pi ((X \/ Y),x)
then consider f being Function such that
A7: f in Y and
A8: y = f . x by A3, Def6;
 f in X \/ Y by A7, XBOOLE_0:def_3;
hence  y in pi ((X \/ Y),x) by A8, Def6; ::_thesis: verum
end;
hence  y in pi ((X \/ Y),x) by A4; ::_thesis: verum
end;

theorem :: CARD_3:17
for X, Y, x being set holds pi ((X /\ Y),x) c= (pi (X,x)) /\ (pi (Y,x))
proof
let X, Y, x be set ; ::_thesis: pi ((X /\ Y),x) c= (pi (X,x)) /\ (pi (Y,x))
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in pi ((X /\ Y),x) or y in (pi (X,x)) /\ (pi (Y,x)) )
assume  y in pi ((X /\ Y),x) ; ::_thesis: y in (pi (X,x)) /\ (pi (Y,x))
then consider f being Function such that
A1: f in X /\ Y and
A2: y = f . x by Def6;
A3: f in X by A1, XBOOLE_0:def_4;
A4: f in Y by A1, XBOOLE_0:def_4;
A5: y in pi (X,x) by A2, A3, Def6;
 y in pi (Y,x) by A2, A4, Def6;
hence  y in (pi (X,x)) /\ (pi (Y,x)) by A5, XBOOLE_0:def_4; ::_thesis: verum
end;

theorem Th18: :: CARD_3:18
for X, x, Y being set holds (pi (X,x)) \ (pi (Y,x)) c= pi ((X \ Y),x)
proof
let X, x, Y be set ; ::_thesis: (pi (X,x)) \ (pi (Y,x)) c= pi ((X \ Y),x)
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in (pi (X,x)) \ (pi (Y,x)) or y in pi ((X \ Y),x) )
assume A1: y in (pi (X,x)) \ (pi (Y,x)) ; ::_thesis: y in pi ((X \ Y),x)
then consider f being Function such that
A2: f in X and
A3: y = f . x by Def6;
 not y in pi (Y,x) by A1, XBOOLE_0:def_5;
then  not f in Y by A3, Def6;
then  f in X \ Y by A2, XBOOLE_0:def_5;
hence  y in pi ((X \ Y),x) by A3, Def6; ::_thesis: verum
end;

theorem :: CARD_3:19
for X, x, Y being set holds (pi (X,x)) \+\ (pi (Y,x)) c= pi ((X \+\ Y),x)
proof
let X, x, Y be set ; ::_thesis: (pi (X,x)) \+\ (pi (Y,x)) c= pi ((X \+\ Y),x)
A1: (pi (X,x)) \ (pi (Y,x)) c= pi ((X \ Y),x) by Th18;
A2: (pi (Y,x)) \ (pi (X,x)) c= pi ((Y \ X),x) by Th18;
 (pi ((X \ Y),x)) \/ (pi ((Y \ X),x)) = pi (((X \ Y) \/ (Y \ X)),x) by Th16;
hence  (pi (X,x)) \+\ (pi (Y,x)) c= pi ((X \+\ Y),x) by A1, A2, XBOOLE_1:13; ::_thesis: verum
end;

theorem Th20: :: CARD_3:20
for X, x being set holds card (pi (X,x)) c= card X
proof
let X, x be set ; ::_thesis: card (pi (X,x)) c= card X
consider Y being set  such that
A1: for y being set holds
( y in Y iff ( y in X & S1[y] ) ) from XBOOLE_0:sch_1();
defpred S2[ set , set ] means  ex g being Function st
( $1 = g & $2 = g . x );
A2: for y being set st y in Y holds
ex z being set st S2[y,z]
proof
let y be set ; ::_thesis: ( y in Y implies ex z being set st S2[y,z] )
assume  y in Y ; ::_thesis: ex z being set st S2[y,z]
then reconsider y = y as Function by A1;
take  y . x ; ::_thesis: S2[y,y . x]
take  y ; ::_thesis: ( y = y & y . x = y . x )
thus  ( y = y & y . x = y . x ) ; ::_thesis: verum
end;
consider f being Function such that
A3: ( dom f = Y & ( for y being set st y in Y holds
S2[y,f . y] ) ) from CLASSES1:sch_1(A2);
now__::_thesis:_for_y_being_set_holds_
(_(_y_in_rng_f_implies_ex_f_being_Function_st_
(_f_in_X_&_y_=_f_._x_)_)_&_(_ex_g_being_Function_st_
(_g_in_X_&_y_=_g_._x_)_implies_y_in_rng_f_)_)
let y be set ; ::_thesis: ( ( y in rng f implies ex f being Function st
( f in X & y = f . x ) ) & ( ex g being Function st
( g in X & y = g . x ) implies y in rng f ) )
thus  ( y in rng f implies ex f being Function st
( f in X & y = f . x ) ) ::_thesis: ( ex g being Function st
( g in X & y = g . x ) implies y in rng f )
proof
assume  y in rng f ; ::_thesis: ex f being Function st
( f in X & y = f . x )
then consider z being set  such that
A4: z in dom f and
A5: y = f . z by FUNCT_1:def_3;
consider g being Function such that
A6: z = g and
A7: f . z = g . x by A3, A4;
take  g ; ::_thesis: ( g in X & y = g . x )
thus  ( g in X & y = g . x ) by A1, A3, A4, A5, A6, A7; ::_thesis: verum
end;
given g being Function such that A8: g in X and
A9: y = g . x ; ::_thesis: y in rng f
A10: g in Y by A1, A8;
then  ex f1 being Function st
( g = f1 & f . g = f1 . x ) by A3;
hence  y in rng f by A3, A9, A10, FUNCT_1:def_3; ::_thesis: verum
end;
then  rng f = pi (X,x) by Def6;
then A11: card (pi (X,x)) c= card Y by A3, CARD_1:12;
 Y c= X
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Y or x in X )
thus  ( not x in Y or x in X ) by A1; ::_thesis: verum
end;
then  card Y c= card X by CARD_1:11;
hence  card (pi (X,x)) c= card X by A11, XBOOLE_1:1; ::_thesis: verum
end;

theorem Th21: :: CARD_3:21
for x being set
for f being Function st x in Union (disjoin f) holds
ex y, z being set st x = [y,z]
proof
let x be set ; ::_thesis: for f being Function st x in Union (disjoin f) holds
ex y, z being set st x = [y,z]
let f be Function; ::_thesis: ( x in Union (disjoin f) implies ex y, z being set st x = [y,z] )
assume  x in Union (disjoin f) ; ::_thesis: ex y, z being set st x = [y,z]
then consider X being set  such that
A1: x in X and
A2: X in rng (disjoin f) by TARSKI:def_4;
consider y being set  such that
A3: y in dom (disjoin f) and
A4: X = (disjoin f) . y by A2, FUNCT_1:def_3;
 y in dom f by A3, Def3;
then  X = [:(f . y),{y}:] by A4, Def3;
hence  ex y, z being set st x = [y,z] by A1, RELAT_1:def_1; ::_thesis: verum
end;

theorem Th22: :: CARD_3:22
for x being set
for f being Function holds
( x in Union (disjoin f) iff ( x `2 in dom f & x `1 in f . (x `2) & x = [(x `1),(x `2)] ) )
proof
let x be set ; ::_thesis: for f being Function holds
( x in Union (disjoin f) iff ( x `2 in dom f & x `1 in f . (x `2) & x = [(x `1),(x `2)] ) )
let f be Function; ::_thesis: ( x in Union (disjoin f) iff ( x `2 in dom f & x `1 in f . (x `2) & x = [(x `1),(x `2)] ) )
thus  ( x in Union (disjoin f) implies ( x `2 in dom f & x `1 in f . (x `2) & x = [(x `1),(x `2)] ) ) ::_thesis: ( x `2 in dom f & x `1 in f . (x `2) & x = [(x `1),(x `2)] implies x in Union (disjoin f) )
proof
assume  x in Union (disjoin f) ; ::_thesis: ( x `2 in dom f & x `1 in f . (x `2) & x = [(x `1),(x `2)] )
then consider X being set  such that
A1: x in X and
A2: X in rng (disjoin f) by TARSKI:def_4;
consider y being set  such that
A3: y in dom (disjoin f) and
A4: X = (disjoin f) . y by A2, FUNCT_1:def_3;
A5: y in dom f by A3, Def3;
then A6: X = [:(f . y),{y}:] by A4, Def3;
then A7: x `1 in f . y by A1, MCART_1:10;
 x `2 in {y} by A1, A6, MCART_1:10;
hence  ( x `2 in dom f & x `1 in f . (x `2) & x = [(x `1),(x `2)] ) by A1, A5, A6, A7, MCART_1:21, TARSKI:def_1; ::_thesis: verum
end;
assume that
A8: x `2 in dom f and
A9: x `1 in f . (x `2) and
A10: x = [(x `1),(x `2)] ; ::_thesis: x in Union (disjoin f)
A11: (disjoin f) . (x `2) = [:(f . (x `2)),{(x `2)}:] by A8, Def3;
A12: dom f = dom (disjoin f) by Def3;
 x `2 in {(x `2)} by TARSKI:def_1;
then A13: x in [:(f . (x `2)),{(x `2)}:] by A9, A10, ZFMISC_1:87;
 [:(f . (x `2)),{(x `2)}:] in rng (disjoin f) by A8, A11, A12, FUNCT_1:def_3;
hence  x in Union (disjoin f) by A13, TARSKI:def_4; ::_thesis: verum
end;

theorem Th23: :: CARD_3:23
for f, g being Function st f c= g holds
disjoin f c= disjoin g
proof
let f, g be Function; ::_thesis: ( f c= g implies disjoin f c= disjoin g )
assume A1: f c= g ; ::_thesis: disjoin f c= disjoin g
then A2: dom f c= dom g by GRFUNC_1:2;
A3: dom (disjoin f) = dom f by Def3;
A4: dom (disjoin g) = dom g by Def3;
now__::_thesis:_for_x_being_set_st_x_in_dom_(disjoin_f)_holds_
(disjoin_f)_._x_=_(disjoin_g)_._x
let x be set ; ::_thesis: ( x in dom (disjoin f) implies (disjoin f) . x = (disjoin g) . x )
assume A5: x in dom (disjoin f) ; ::_thesis: (disjoin f) . x = (disjoin g) . x
then A6: (disjoin f) . x = [:(f . x),{x}:] by A3, Def3;
 f . x = g . x by A1, A3, A5, GRFUNC_1:2;
hence  (disjoin f) . x = (disjoin g) . x by A2, A3, A5, A6, Def3; ::_thesis: verum
end;
hence  disjoin f c= disjoin g by A2, A3, A4, GRFUNC_1:2; ::_thesis: verum
end;

theorem Th24: :: CARD_3:24
for f, g being Function st f c= g holds
Union f c= Union g
proof
let f, g be Function; ::_thesis: ( f c= g implies Union f c= Union g )
assume A1: f c= g ; ::_thesis: Union f c= Union g
then A2: dom f c= dom g by GRFUNC_1:2;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Union f or x in Union g )
assume  x in Union f ; ::_thesis: x in Union g
then consider X being set  such that
A3: x in X and
A4: X in rng f by TARSKI:def_4;
consider y being set  such that
A5: y in dom f and
A6: X = f . y by A4, FUNCT_1:def_3;
 f . y = g . y by A1, A5, GRFUNC_1:2;
then  X in rng g by A2, A5, A6, FUNCT_1:def_3;
hence  x in Union g by A3, TARSKI:def_4; ::_thesis: verum
end;

theorem :: CARD_3:25
for Y, X being set holds Union (disjoin (Y --> X)) = [:X,Y:]
proof
let Y, X be set ; ::_thesis: Union (disjoin (Y --> X)) = [:X,Y:]
set f = Y --> X;
A1: dom (Y --> X) = Y by FUNCOP_1:13;
thus  Union (disjoin (Y --> X)) c= [:X,Y:] :: according to XBOOLE_0:def_10 ::_thesis: [:X,Y:] c= Union (disjoin (Y --> X))
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Union (disjoin (Y --> X)) or x in [:X,Y:] )
assume  x in Union (disjoin (Y --> X)) ; ::_thesis: x in [:X,Y:]
then consider Z being set  such that
A2: x in Z and
A3: Z in rng (disjoin (Y --> X)) by TARSKI:def_4;
consider y being set  such that
A4: y in dom (disjoin (Y --> X)) and
A5: Z = (disjoin (Y --> X)) . y by A3, FUNCT_1:def_3;
A6: y in Y by A1, A4, Def3;
then A7: Z = [:((Y --> X) . y),{y}:] by A1, A5, Def3;
A8: (Y --> X) . y = X by A6, FUNCOP_1:7;
 {y} c= Y by A6, ZFMISC_1:31;
then  Z c= [:X,Y:] by A7, A8, ZFMISC_1:95;
hence  x in [:X,Y:] by A2; ::_thesis: verum
end;
let x1, x2 be set ; :: according to RELAT_1:def_3 ::_thesis: ( not [x1,x2] in [:X,Y:] or [x1,x2] in Union (disjoin (Y --> X)) )
assume A9: [x1,x2] in [:X,Y:] ; ::_thesis: [x1,x2] in Union (disjoin (Y --> X))
then A10: x1 in X by ZFMISC_1:87;
A11: x2 in Y by A9, ZFMISC_1:87;
then A12: (Y --> X) . x2 = X by FUNCOP_1:7;
A13: (disjoin (Y --> X)) . x2 = [:((Y --> X) . x2),{x2}:] by A1, A11, Def3;
A14: x2 in dom (disjoin (Y --> X)) by A1, A11, Def3;
 x2 in {x2} by TARSKI:def_1;
then A15: [x1,x2] in [:((Y --> X) . x2),{x2}:] by A10, A12, ZFMISC_1:87;
 [:((Y --> X) . x2),{x2}:] in rng (disjoin (Y --> X)) by A13, A14, FUNCT_1:def_3;
hence  [x1,x2] in Union (disjoin (Y --> X)) by A15, TARSKI:def_4; ::_thesis: verum
end;

theorem Th26: :: CARD_3:26
for f being Function holds
( product f = {} iff {} in rng f )
proof
let f be Function; ::_thesis: ( product f = {} iff {} in rng f )
thus  ( product f = {} implies {} in rng f ) ::_thesis: ( {} in rng f implies product f = {} )
proof
assume that
A1: product f = {} and
A2: not {} in rng f ; ::_thesis: contradiction
A3: now__::_thesis:_not_dom_f_=_{}
assume  dom f = {} ; ::_thesis: contradiction
then  for x being set st x in dom f holds
f . x in f . x ;
hence  contradiction by A1, Def5; ::_thesis: verum
end;
now__::_thesis:_not_dom_f_<>_{}
assume  dom f <> {} ; ::_thesis: contradiction
then reconsider M = rng f as non empty set by RELAT_1:42;
 for X being set st X in M holds
X <> {} by A2;
then consider f1 being Function such that
 dom f1 = M and
A4: for X being set st X in M holds
f1 . X in X by FUNCT_1:111;
deffunc H1( set ) ->  set = f1 . (f . $1);
consider g being Function such that
A5: ( dom g = dom f & ( for x being set st x in dom f holds
g . x = H1(x) ) ) from FUNCT_1:sch_3();
now__::_thesis:_for_x_being_set_st_x_in_dom_f_holds_
g_._x_in_f_._x
let x be set ; ::_thesis: ( x in dom f implies g . x in f . x )
assume A6: x in dom f ; ::_thesis: g . x in f . x
then A7: f . x in M by FUNCT_1:def_3;
 g . x = f1 . (f . x) by A5, A6;
hence  g . x in f . x by A4, A7; ::_thesis: verum
end;
hence  contradiction by A1, A5, Def5; ::_thesis: verum
end;
hence  contradiction by A3; ::_thesis: verum
end;
assume  {} in rng f ; ::_thesis: product f = {}
then A8: ex x being set st
( x in dom f & {} = f . x ) by FUNCT_1:def_3;
assume A9: product f <> {} ; ::_thesis: contradiction
set y = the Element of product f;
 ex g being Function st
( the Element of product f = g & dom g = dom f & ( for x being set st x in dom f holds
g . x in f . x ) ) by A9, Def5;
hence  contradiction by A8; ::_thesis: verum
end;

theorem Th27: :: CARD_3:27
for f, g being Function st dom f = dom g & ( for x being set st x in dom f holds
f . x c= g . x ) holds
product f c= product g
proof
let f, g be Function; ::_thesis: ( dom f = dom g & ( for x being set st x in dom f holds
f . x c= g . x ) implies product f c= product g )
assume that
A1: dom f = dom g and
A2: for x being set st x in dom f holds
f . x c= g . x ; ::_thesis: product f c= product g
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in product f or x in product g )
assume  x in product f ; ::_thesis: x in product g
then consider f1 being Function such that
A3: x = f1 and
A4: dom f1 = dom f and
A5: for x being set st x in dom f holds
f1 . x in f . x by Def5;
now__::_thesis:_for_x_being_set_st_x_in_dom_g_holds_
f1_._x_in_g_._x
let x be set ; ::_thesis: ( x in dom g implies f1 . x in g . x )
assume A6: x in dom g ; ::_thesis: f1 . x in g . x
then A7: f1 . x in f . x by A1, A5;
 f . x c= g . x by A1, A2, A6;
hence  f1 . x in g . x by A7; ::_thesis: verum
end;
hence  x in product g by A1, A3, A4, Def5; ::_thesis: verum
end;


theorem :: CARD_3:28
for F being Cardinal-Function
for x being set st x in dom F holds
card (F . x) = F . x
proof
let F be Cardinal-Function; ::_thesis: for x being set st x in dom F holds
card (F . x) = F . x
let x be set ; ::_thesis: ( x in dom F implies card (F . x) = F . x )
assume  x in dom F ; ::_thesis: card (F . x) = F . x
then reconsider M = F . x as Cardinal by Def1;
 card M = M by CARD_1:def_2;
hence  card (F . x) = F . x ; ::_thesis: verum
end;

theorem Th29: :: CARD_3:29
for F being Cardinal-Function
for x being set st x in dom F holds
card ((disjoin F) . x) = F . x
proof
let F be Cardinal-Function; ::_thesis: for x being set st x in dom F holds
card ((disjoin F) . x) = F . x
let x be set ; ::_thesis: ( x in dom F implies card ((disjoin F) . x) = F . x )
assume A1: x in dom F ; ::_thesis: card ((disjoin F) . x) = F . x
then reconsider M = F . x as Cardinal by Def1;
 M,[:M,{x}:] are_equipotent by CARD_1:69;
then  M = card [:M,{x}:] by CARD_1:def_2;
hence  card ((disjoin F) . x) = F . x by A1, Def3; ::_thesis: verum
end;

definition
let F be Cardinal-Function;
func Sum F ->  Cardinal equals :: CARD_3:def 7
 card (Union (disjoin F));
correctness
coherence
card (Union (disjoin F)) is Cardinal;
;
func Product F ->  Cardinal equals :: CARD_3:def 8
 card (product F);
correctness
coherence
card (product F) is Cardinal;
;
end;

:: deftheorem  defines Sum CARD_3:def_7_:_
 for F being Cardinal-Function holds Sum F = card (Union (disjoin F));

:: deftheorem  defines Product CARD_3:def_8_:_
 for F being Cardinal-Function holds Product F = card (product F);

theorem :: CARD_3:30
for F, G being Cardinal-Function st dom F = dom G & ( for x being set st x in dom F holds
F . x c= G . x ) holds
Sum F c= Sum G
proof
let F, G be Cardinal-Function; ::_thesis: ( dom F = dom G & ( for x being set st x in dom F holds
F . x c= G . x ) implies Sum F c= Sum G )
assume that
A1: dom F = dom G and
A2: for x being set st x in dom F holds
F . x c= G . x ; ::_thesis: Sum F c= Sum G
 Union (disjoin F) c= Union (disjoin G)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Union (disjoin F) or x in Union (disjoin G) )
assume  x in Union (disjoin F) ; ::_thesis: x in Union (disjoin G)
then consider X being set  such that
A3: x in X and
A4: X in rng (disjoin F) by TARSKI:def_4;
consider y being set  such that
A5: y in dom (disjoin F) and
A6: X = (disjoin F) . y by A4, FUNCT_1:def_3;
A7: y in dom F by A5, Def3;
then A8: F . y c= G . y by A2;
A9: X = [:(F . y),{y}:] by A6, A7, Def3;
A10: (disjoin G) . y = [:(G . y),{y}:] by A1, A7, Def3;
A11: y in dom (disjoin G) by A1, A7, Def3;
A12: X c= [:(G . y),{y}:] by A8, A9, ZFMISC_1:95;
 [:(G . y),{y}:] in rng (disjoin G) by A10, A11, FUNCT_1:def_3;
hence  x in Union (disjoin G) by A3, A12, TARSKI:def_4; ::_thesis: verum
end;
hence  Sum F c= Sum G by CARD_1:11; ::_thesis: verum
end;

theorem :: CARD_3:31
for F being Cardinal-Function holds
( {} in rng F iff Product F = 0 )
proof
let F be Cardinal-Function; ::_thesis: ( {} in rng F iff Product F = 0 )
thus  ( {} in rng F implies Product F = 0 ) by Th26, CARD_1:27; ::_thesis: ( Product F = 0 implies {} in rng F )
assume  Product F = 0 ; ::_thesis: {} in rng F
then  product F = {} ;
hence  {} in rng F by Th26; ::_thesis: verum
end;

theorem :: CARD_3:32
for F, G being Cardinal-Function st dom F = dom G & ( for x being set st x in dom F holds
F . x c= G . x ) holds
Product F c= Product G by Th27, CARD_1:11;

theorem :: CARD_3:33
for F, G being Cardinal-Function st F c= G holds
Sum F c= Sum G
proof
let F, G be Cardinal-Function; ::_thesis: ( F c= G implies Sum F c= Sum G )
assume  F c= G ; ::_thesis: Sum F c= Sum G
then  disjoin F c= disjoin G by Th23;
hence  Sum F c= Sum G by Th24, CARD_1:11; ::_thesis: verum
end;

theorem :: CARD_3:34
for F, G being Cardinal-Function st F c= G & not 0 in rng G holds
Product F c= Product G
proof
let F, G be Cardinal-Function; ::_thesis: ( F c= G & not 0 in rng G implies Product F c= Product G )
assume A1: F c= G ; ::_thesis: ( 0 in rng G or Product F c= Product G )
then A2: dom F c= dom G by GRFUNC_1:2;
assume A3: not 0 in rng G ; ::_thesis: Product F c= Product G
deffunc H1( Function) ->  set = $1 | (dom F);
consider f being Function such that
A4: ( dom f = product G & ( for g being Function st g in product G holds
f . g = H1(g) ) ) from FUNCT_5:sch_1();
 product F c= rng f
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in product F or x in rng f )
assume  x in product F ; ::_thesis: x in rng f
then consider g being Function such that
A5: x = g and
A6: dom g = dom F and
A7: for x being set st x in dom F holds
g . x in F . x by Def5;
A8: product G <> {} by A3, Th26;
set y = the Element of product G;
consider h being Function such that
 the Element of product G = h and
 dom h = dom G and
A9: for x being set st x in dom G holds
h . x in G . x by A8, Def5;
deffunc H2( set ) ->  set = g . $1;
deffunc H3( set ) ->  set = h . $1;
defpred S2[ set ] means $1 in dom F;
consider f1 being Function such that
A10: ( dom f1 = dom G & ( for x being set st x in dom G holds
( ( S2[x] implies f1 . x = H2(x) ) & ( not S2[x] implies f1 . x = H3(x) ) ) ) ) from PARTFUN1:sch_1();
now__::_thesis:_for_z_being_set_st_z_in_dom_G_holds_
f1_._z_in_G_._z
let z be set ; ::_thesis: ( z in dom G implies f1 . z in G . z )
assume A11: z in dom G ; ::_thesis: f1 . z in G . z
A12: now__::_thesis:_(_z_in_dom_F_implies_f1_._z_in_G_._z_)
assume A13: z in dom F ; ::_thesis: f1 . z in G . z
then A14: f1 . z = g . z by A10, A11;
 g . z in F . z by A7, A13;
hence  f1 . z in G . z by A1, A13, A14, GRFUNC_1:2; ::_thesis: verum
end;
 ( not z in dom F implies f1 . z = h . z ) by A10, A11;
hence  f1 . z in G . z by A9, A11, A12; ::_thesis: verum
end;
then A15: f1 in product G by A10, Def5;
then A16: f . f1 = f1 | (dom F) by A4;
A17: dom (f1 | (dom F)) = dom F by A2, A10, RELAT_1:62;
now__::_thesis:_for_z_being_set_st_z_in_dom_F_holds_
(f1_|_(dom_F))_._z_=_g_._z
let z be set ; ::_thesis: ( z in dom F implies (f1 | (dom F)) . z = g . z )
assume A18: z in dom F ; ::_thesis: (f1 | (dom F)) . z = g . z
then  (f1 | (dom F)) . z = f1 . z by A17, FUNCT_1:47;
hence  (f1 | (dom F)) . z = g . z by A2, A10, A18; ::_thesis: verum
end;
then  f . f1 = g by A6, A16, A17, FUNCT_1:2;
hence  x in rng f by A4, A5, A15, FUNCT_1:def_3; ::_thesis: verum
end;
hence  Product F c= Product G by A4, CARD_1:12; ::_thesis: verum
end;

theorem :: CARD_3:35
for K being Cardinal holds Sum ({} --> K) = 0
proof
let K be Cardinal; ::_thesis: Sum ({} --> K) = 0
 dom ({} --> K) = {} ;
then  dom (disjoin ({} --> K)) = {} by Def3;
hence  Sum ({} --> K) = 0 by CARD_1:27, RELAT_1:42, ZFMISC_1:2; ::_thesis: verum
end;

theorem :: CARD_3:36
for K being Cardinal holds Product ({} --> K) = 1 by Th10, CARD_1:30;

theorem :: CARD_3:37
for K being Cardinal
for x being set holds Sum (x .--> K) = K
proof
let K be Cardinal; ::_thesis: for x being set holds Sum (x .--> K) = K
let x be set ; ::_thesis: Sum (x .--> K) = K
thus  Sum (x .--> K) = card (Union (x .--> [:K,{x}:])) by Th4
.= card [:K,{x}:] by Th7
.= card K by CARD_1:69
.= K by CARD_1:def_2 ; ::_thesis: verum
end;

theorem :: CARD_3:38
for K being Cardinal
for x being set holds Product (x .--> K) = K
proof
let K be Cardinal; ::_thesis: for x being set holds Product (x .--> K) = K
let x be set ; ::_thesis: Product (x .--> K) = K
thus  Product (x .--> K) = card (Funcs ({x},K)) by Th11
.= card K by FUNCT_5:58
.= K by CARD_1:def_2 ; ::_thesis: verum
end;

theorem Th39: :: CARD_3:39
for f being Function holds card (Union f) c= Sum (Card f)
proof
let f be Function; ::_thesis: card (Union f) c= Sum (Card f)
A1: now__::_thesis:_(_dom_f_=_{}_implies_card_(Union_f)_c=_Sum_(Card_f)_)
assume  dom f = {} ; ::_thesis: card (Union f) c= Sum (Card f)
then  {} = Union f by RELAT_1:42, ZFMISC_1:2;
hence  card (Union f) c= Sum (Card f) ; ::_thesis: verum
end;
now__::_thesis:_(_dom_f_<>_{}_implies_card_(Union_f)_c=_Sum_(Card_f)_)
assume A2: dom f <> {} ; ::_thesis: card (Union f) c= Sum (Card f)
defpred S2[ set , set ] means  for x being set holds
( x in $2 iff ( x in Funcs ((card $1),$1) & ex g being Function st
( x = g & rng g = $1 ) ) );
defpred S3[ set , set ] means S2[f . $1,$2];
A3: for x being set st x in dom f holds
ex y being set st S3[x,y]
proof
let x be set ; ::_thesis: ( x in dom f implies ex y being set st S3[x,y] )
assume  x in dom f ; ::_thesis: ex y being set st S3[x,y]
defpred S4[ set ] means  ex g being Function st
( $1 = g & rng g = f . x );
consider Y being set  such that
A4: for z being set holds
( z in Y iff ( z in Funcs ((card (f . x)),(f . x)) & S4[z] ) ) from XBOOLE_0:sch_1();
take  Y ; ::_thesis: S3[x,Y]
thus  S3[x,Y] by A4; ::_thesis: verum
end;
consider k being Function such that
A5: ( dom k = dom f & ( for x being set st x in dom f holds
S3[x,k . x] ) ) from CLASSES1:sch_1(A3);
reconsider M = rng k as non empty set by A2, A5, RELAT_1:42;
now__::_thesis:_for_X_being_set_st_X_in_M_holds_
X_<>_{}
let X be set ; ::_thesis: ( X in M implies X <> {} )
assume  X in M ; ::_thesis: X <> {}
then consider x being set  such that
A6: x in dom k and
A7: X = k . x by FUNCT_1:def_3;
 card (f . x),f . x are_equipotent by CARD_1:def_2;
then consider g being Function such that
 g is one-to-one and
A8: dom g = card (f . x) and
A9: rng g = f . x by WELLORD2:def_4;
 g in Funcs ((card (f . x)),(f . x)) by A8, A9, FUNCT_2:def_2;
hence  X <> {} by A5, A6, A7, A9; ::_thesis: verum
end;
then consider FF being Function such that
 dom FF = M and
A10: for X being set st X in M holds
FF . X in X by FUNCT_1:111;
set DD = union (rng (disjoin (Card f)));
defpred S4[ set , set ] means  ex g being Function st
( g = FF . (k . ($1 `2)) & $2 = g . ($1 `1) );
A11: for x being set st x in union (rng (disjoin (Card f))) holds
ex y being set st S4[x,y]
proof
let x be set ; ::_thesis: ( x in union (rng (disjoin (Card f))) implies ex y being set st S4[x,y] )
assume  x in union (rng (disjoin (Card f))) ; ::_thesis: ex y being set st S4[x,y]
then consider X being set  such that
A12: x in X and
A13: X in rng (disjoin (Card f)) by TARSKI:def_4;
consider y being set  such that
A14: y in dom (disjoin (Card f)) and
A15: X = (disjoin (Card f)) . y by A13, FUNCT_1:def_3;
A16: dom (disjoin (Card f)) = dom (Card f) by Def3;
A17: dom (Card f) = dom f by Def2;
 X = [:((Card f) . y),{y}:] by A14, A15, A16, Def3;
then  x `2 in {y} by A12, MCART_1:10;
then A18: x `2 in dom f by A14, A16, A17, TARSKI:def_1;
then  k . (x `2) in M by A5, FUNCT_1:def_3;
then  FF . (k . (x `2)) in k . (x `2) by A10;
then  FF . (k . (x `2)) in Funcs ((card (f . (x `2))),(f . (x `2))) by A5, A18;
then consider g being Function such that
A19: FF . (k . (x `2)) = g and
 dom g = card (f . (x `2)) and
 rng g c= f . (x `2) by FUNCT_2:def_2;
take  g . (x `1) ; ::_thesis: S4[x,g . (x `1)]
take  g ; ::_thesis: ( g = FF . (k . (x `2)) & g . (x `1) = g . (x `1) )
thus  ( g = FF . (k . (x `2)) & g . (x `1) = g . (x `1) ) by A19; ::_thesis: verum
end;
consider t being Function such that
A20: ( dom t = union (rng (disjoin (Card f))) & ( for x being set st x in union (rng (disjoin (Card f))) holds
S4[x,t . x] ) ) from CLASSES1:sch_1(A11);
 union (rng f) c= rng t
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in union (rng f) or x in rng t )
assume  x in union (rng f) ; ::_thesis: x in rng t
then consider X being set  such that
A21: x in X and
A22: X in rng f by TARSKI:def_4;
consider y being set  such that
A23: y in dom f and
A24: X = f . y by A22, FUNCT_1:def_3;
 k . y in M by A5, A23, FUNCT_1:def_3;
then A25: FF . (k . y) in k . y by A10;
then  FF . (k . y) in Funcs ((card (f . y)),(f . y)) by A5, A23;
then consider g being Function such that
A26: FF . (k . y) = g and
A27: dom g = card (f . y) and
 rng g c= f . y by FUNCT_2:def_2;
 ex g being Function st
( FF . (k . y) = g & rng g = f . y ) by A5, A23, A25;
then consider z being set  such that
A28: z in dom g and
A29: x = g . z by A21, A24, A26, FUNCT_1:def_3;
A30: (Card f) . y = card (f . y) by A23, Def2;
A31: dom (Card f) = dom f by Def2;
then A32: (disjoin (Card f)) . y = [:(dom g),{y}:] by A23, A27, A30, Def3;
A33: y in {y} by TARSKI:def_1;
A34: dom (disjoin (Card f)) = dom f by A31, Def3;
A35: [z,y] in [:(dom g),{y}:] by A28, A33, ZFMISC_1:87;
 [:(dom g),{y}:] in rng (disjoin (Card f)) by A23, A32, A34, FUNCT_1:def_3;
then A36: [z,y] in union (rng (disjoin (Card f))) by A35, TARSKI:def_4;
A37: [z,y] `1 = z ;
 [z,y] `2 = y ;
then  ex g being Function st
( g = FF . (k . y) & t . [z,y] = g . z ) by A20, A36, A37;
hence  x in rng t by A20, A26, A29, A36, FUNCT_1:def_3; ::_thesis: verum
end;
hence  card (Union f) c= Sum (Card f) by A20, CARD_1:12; ::_thesis: verum
end;
hence  card (Union f) c= Sum (Card f) by A1; ::_thesis: verum
end;

theorem :: CARD_3:40
for F being Cardinal-Function holds card (Union F) c= Sum F
proof
let F be Cardinal-Function; ::_thesis: card (Union F) c= Sum F
 Card F = F by Th1;
hence  card (Union F) c= Sum F by Th39; ::_thesis: verum
end;

theorem :: CARD_3:41
for F, G being Cardinal-Function st dom F = dom G & ( for x being set st x in dom F holds
F . x in G . x ) holds
Sum F in Product G
proof
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__::_thesis:_not_{}_in_rng_f
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_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 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_4 ::_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, 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 set st x = [x1,x2] by A11, A13, Th21;
A25: ex x1, x2 being set st y = [x1,x2] by A11, A14, Th21;
A26: x = [(x `1),(x `2)] by A24, MCART_1:8;
A27: y = [(y `1),(y `2)] by A25, MCART_1:8;
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 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_3;
consider g being Function such that
A39: f1 . y = g and
A40: S2[y,g] by A11, A37;
now__::_thesis:_for_x_being_set_st_x_in_dom_G_holds_
g_._x_in_G_._x
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, 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 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__::_thesis:_not_{}_in_rng_K
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_3;
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, XBOOLE_1:1;
A58: Fx in Gx by A2, A52;
 card Gx = Gx by CARD_1:def_2;
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 set st x in dom K holds
g . x in K . x by A59, Def5;
now__::_thesis:_for_x_being_set_st_x_in_dom_K_holds_
K_._x_c=_G_._x
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, Th27;
then  the Element of product K in product G by A59, TARSKI:def_3;
then consider y being set  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 set  such that
A66: x in dom (disjoin F) and
A67: X = (disjoin F) . x by A65, FUNCT_1:def_3;
 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
end;

scheme :: CARD_3:sch 2
FuncSeparation{ F1() ->  set , F2( set ) ->  set , P1[ set , set ] } :
 ex f being Function st
( dom f = F1() & ( for x being set st x in F1() holds
for y being set holds
( y in f . x iff ( y in F2(x) & P1[x,y] ) ) ) )
proof
defpred S2[ set , set ] means  for y being set holds
( y in $2 iff ( y in F2($1) & P1[$1,y] ) );
A1: for x being set st x in F1() holds
ex y being set st S2[x,y]
proof
let x be set ; ::_thesis: ( x in F1() implies ex y being set st S2[x,y] )
assume  x in F1() ; ::_thesis: ex y being set st S2[x,y]
defpred S3[ set ] means P1[x,$1];
consider Y being set  such that
A2: for y being set holds
( y in Y iff ( y in F2(x) & S3[y] ) ) from XBOOLE_0:sch_1();
take  Y ; ::_thesis: S2[x,Y]
thus  S2[x,Y] by A2; ::_thesis: verum
end;
thus  ex f being Function st
( dom f = F1() & ( for x being set st x in F1() holds
S2[x,f . x] ) ) from CLASSES1:sch_1(A1); ::_thesis: verum
end;

Lm1:  for x being set
for R being Relation st x in field R holds
ex y being set st
( [x,y] in R or [y,x] in R )
proof
let x be set ; ::_thesis: for R being Relation st x in field R holds
ex y being set st
( [x,y] in R or [y,x] in R )
let R be Relation; ::_thesis: ( x in field R implies ex y being set st
( [x,y] in R or [y,x] in R ) )
assume  x in field R ; ::_thesis: ex y being set st
( [x,y] in R or [y,x] in R )
then  ( x in dom R or x in rng R ) by XBOOLE_0:def_3;
hence  ex y being set st
( [x,y] in R or [y,x] in R ) by XTUPLE_0:def_12, XTUPLE_0:def_13; ::_thesis: verum
end;

theorem Th42: :: CARD_3:42
for X being set st X is finite holds
card X in card omega
proof
let X be set ; ::_thesis: ( X is finite implies card X in card omega )
assume  X is finite ; ::_thesis: card X in card omega
then  ex n being Nat st card X = card n by CARD_1:48;
hence  card X in card omega by CARD_1:47; ::_thesis: verum
end;

theorem Th43: :: CARD_3:43
for A, B being Ordinal st card A in card B holds
A in B
proof
let A, B be Ordinal; ::_thesis: ( card A in card B implies A in B )
assume that
A1: card A in card B and
A2: not A in B ; ::_thesis: contradiction
 not card B c= card A by A1, CARD_1:4;
hence  contradiction by A2, CARD_1:11, ORDINAL1:16; ::_thesis: verum
end;

theorem Th44: :: CARD_3:44
for A being Ordinal
for M being Cardinal st card A in M holds
A in M
proof
let A be Ordinal; ::_thesis: for M being Cardinal st card A in M holds
A in M
let M be Cardinal; ::_thesis: ( card A in M implies A in M )
 card M = M by CARD_1:def_2;
hence  ( card A in M implies A in M ) by Th43; ::_thesis: verum
end;

theorem Th45: :: CARD_3:45
for X being set st X is c=-linear holds
ex Y being set st
( Y c= X & union Y = union X & ( for Z being set st Z c= Y & Z <> {} holds
ex Z1 being set st
( Z1 in Z & ( for Z2 being set st Z2 in Z holds
Z1 c= Z2 ) ) ) )
proof
let X be set ; ::_thesis: ( X is c=-linear implies ex Y being set st
( Y c= X & union Y = union X & ( for Z being set st Z c= Y & Z <> {} holds
ex Z1 being set st
( Z1 in Z & ( for Z2 being set st Z2 in Z holds
Z1 c= Z2 ) ) ) ) )
assume A1: X is c=-linear ; ::_thesis: ex Y being set st
( Y c= X & union Y = union X & ( for Z being set st Z c= Y & Z <> {} holds
ex Z1 being set st
( Z1 in Z & ( for Z2 being set st Z2 in Z holds
Z1 c= Z2 ) ) ) )
consider R being Relation such that
A2: R well_orders X by WELLORD2:17;
A3: R |_2 X is well-ordering by A2, WELLORD2:16;
A4: field (R |_2 X) = X by A2, WELLORD2:16;
 R |_2 X, RelIncl (order_type_of (R |_2 X)) are_isomorphic by A3, WELLORD2:def_2;
then  RelIncl (order_type_of (R |_2 X)),R |_2 X are_isomorphic by WELLORD1:40;
then consider f being Function such that
A5: f is_isomorphism_of RelIncl (order_type_of (R |_2 X)),R |_2 X by WELLORD1:def_8;
 field (RelIncl (order_type_of (R |_2 X))) = order_type_of (R |_2 X) by WELLORD2:def_1;
then A6: dom f = order_type_of (R |_2 X) by A5, WELLORD1:def_7;
A7: rng f = X by A4, A5, WELLORD1:def_7;
defpred S2[ set ] means  for A, B being Ordinal st B in A & $1 = A holds
f . B c= f . A;
consider Y being set  such that
A8: for x being set holds
( x in Y iff ( x in dom f & S2[x] ) ) from XBOOLE_0:sch_1();
take Z = f .: Y; ::_thesis: ( Z c= X & union Z = union X & ( for Z being set st Z c= Z & Z <> {} holds
ex Z1 being set st
( Z1 in Z & ( for Z2 being set st Z2 in Z holds
Z1 c= Z2 ) ) ) )
thus  Z c= X by A7, RELAT_1:111; ::_thesis: ( union Z = union X & ( for Z being set st Z c= Z & Z <> {} holds
ex Z1 being set st
( Z1 in Z & ( for Z2 being set st Z2 in Z holds
Z1 c= Z2 ) ) ) )
thus  union Z c= union X by A7, RELAT_1:111, ZFMISC_1:77; :: according to XBOOLE_0:def_10 ::_thesis: ( union X c= union Z & ( for Z being set st Z c= Z & Z <> {} holds
ex Z1 being set st
( Z1 in Z & ( for Z2 being set st Z2 in Z holds
Z1 c= Z2 ) ) ) )
thus  union X c= union Z ::_thesis: for Z being set st Z c= Z & Z <> {} holds
ex Z1 being set st
( Z1 in Z & ( for Z2 being set st Z2 in Z holds
Z1 c= Z2 ) )
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in union X or x in union Z )
assume  x in union X ; ::_thesis: x in union Z
then consider Z1 being set  such that
A9: x in Z1 and
A10: Z1 in X by TARSKI:def_4;
consider y being set  such that
A11: y in dom f and
A12: Z1 = f . y by A7, A10, FUNCT_1:def_3;
reconsider y = y as Ordinal by A6, A11;
defpred S3[ Ordinal] means ( $1 c= y & x in f . $1 );
A13: ex A being Ordinal st S3[A] by A9, A12;
consider A being Ordinal such that
A14: ( S3[A] & ( for B being Ordinal st S3[B] holds
A c= B ) ) from ORDINAL1:sch_1(A13);
A15: A in dom f by A6, A11, A14, ORDINAL1:12;
now__::_thesis:_for_B,_C_being_Ordinal_st_C_in_B_&_A_=_B_holds_
f_._C_c=_f_._B
let B, C be Ordinal; ::_thesis: ( C in B & A = B implies f . C c= f . B )
assume that
A16: C in B and
A17: A = B ; ::_thesis: f . C c= f . B
A18: C in dom f by A6, A11, A14, A16, A17, ORDINAL1:10;
A19: ( not C c= y or not x in f . C ) by A14, A16, A17, ORDINAL1:5;
A20: f . A in X by A7, A15, FUNCT_1:def_3;
 f . C in X by A7, A18, FUNCT_1:def_3;
then  f . C,f . A are_c=-comparable by A1, A20, ORDINAL1:def_8;
then  ( f . C c= f . A or f . A c= f . C ) by XBOOLE_0:def_9;
hence  f . C c= f . B by A14, A16, A17, A19, ORDINAL1:def_2; ::_thesis: verum
end;
then  A in Y by A8, A15;
then  f . A in Z by A15, FUNCT_1:def_6;
hence  x in union Z by A14, TARSKI:def_4; ::_thesis: verum
end;
let V be set ; ::_thesis: ( V c= Z & V <> {} implies ex Z1 being set st
( Z1 in V & ( for Z2 being set st Z2 in V holds
Z1 c= Z2 ) ) )
assume that
A21: V c= Z and
A22: V <> {} ; ::_thesis: ex Z1 being set st
( Z1 in V & ( for Z2 being set st Z2 in V holds
Z1 c= Z2 ) )
set x = the Element of V;
 the Element of V in Z by A21, A22, TARSKI:def_3;
then consider y being set  such that
A23: y in dom f and
A24: y in Y and
A25: the Element of V = f . y by FUNCT_1:def_6;
reconsider y = y as Ordinal by A6, A23;
defpred S3[ Ordinal] means ( $1 in Y & f . $1 in V );
 y = y ;
then A26: ex A being Ordinal st S3[A] by A22, A24, A25;
consider A being Ordinal such that
A27: ( S3[A] & ( for B being Ordinal st S3[B] holds
A c= B ) ) from ORDINAL1:sch_1(A26);
take Z1 = f . A; ::_thesis: ( Z1 in V & ( for Z2 being set st Z2 in V holds
Z1 c= Z2 ) )
thus  Z1 in V by A27; ::_thesis: for Z2 being set st Z2 in V holds
Z1 c= Z2
let Z2 be set ; ::_thesis: ( Z2 in V implies Z1 c= Z2 )
assume A28: Z2 in V ; ::_thesis: Z1 c= Z2
then consider y being set  such that
A29: y in dom f and
A30: y in Y and
A31: Z2 = f . y by A21, FUNCT_1:def_6;
reconsider y = y as Ordinal by A6, A29;
 ( A c< y iff ( A c= y & A <> y ) ) by XBOOLE_0:def_8;
then  ( A = y or A in y ) by A27, A28, A30, A31, ORDINAL1:11;
hence  Z1 c= Z2 by A8, A30, A31; ::_thesis: verum
end;

theorem :: CARD_3:46
for M being Cardinal
for X being set st ( for Z being set st Z in X holds
card Z in M ) & X is c=-linear holds
card (union X) c= M
proof
let M be Cardinal; ::_thesis: for X being set st ( for Z being set st Z in X holds
card Z in M ) & X is c=-linear holds
card (union X) c= M
let X be set ; ::_thesis: ( ( for Z being set st Z in X holds
card Z in M ) & X is c=-linear implies card (union X) c= M )
assume that
A1: for Z being set st Z in X holds
card Z in M and
A2: X is c=-linear ; ::_thesis: card (union X) c= M
consider XX being set  such that
A3: XX c= X and
A4: union XX = union X and
A5: for Z being set st Z c= XX & Z <> {} holds
ex Z1 being set st
( Z1 in Z & ( for Z2 being set st Z2 in Z holds
Z1 c= Z2 ) ) by A2, Th45;
A6: now__::_thesis:_for_Z1,_Z2_being_set_st_Z1_in_XX_&_Z2_in_XX_&_not_Z1_c=_Z2_holds_
Z2_c=_Z1
let Z1, Z2 be set ; ::_thesis: ( Z1 in XX & Z2 in XX & not Z1 c= Z2 implies Z2 c= Z1 )
assume that
A7: Z1 in XX and
A8: Z2 in XX ; ::_thesis: ( Z1 c= Z2 or Z2 c= Z1 )
 Z1,Z2 are_c=-comparable by A2, A3, A7, A8, ORDINAL1:def_8;
hence  ( Z1 c= Z2 or Z2 c= Z1 ) by XBOOLE_0:def_9; ::_thesis: verum
end;
consider R being Relation such that
A9: R well_orders union X by WELLORD2:17;
A10: R is_reflexive_in union X by A9, WELLORD1:def_5;
A11: R is_transitive_in union X by A9, WELLORD1:def_5;
A12: R is_antisymmetric_in union X by A9, WELLORD1:def_5;
A13: R is_connected_in union X by A9, WELLORD1:def_5;
defpred S2[ set , set ] means ( ex Z1 being set st
( Z1 in XX & $1 in Z1 & not $2 in Z1 ) or ( ( for Z1 being set st Z1 in XX holds
( $1 in Z1 iff $2 in Z1 ) ) & [$1,$2] in R ) );
consider Q being Relation such that
A14: for x, y being set holds
( [x,y] in Q iff ( x in union X & y in union X & S2[x,y] ) ) from RELAT_1:sch_1();
A15: field Q = union X
proof
thus  field Q c= union X :: according to XBOOLE_0:def_10 ::_thesis: union X c= field Q
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in field Q or x in union X )
assume  x in field Q ; ::_thesis: x in union X
then  ex y being set st
( [x,y] in Q or [y,x] in Q ) by Lm1;
hence  x in union X by A14; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in union X or x in field Q )
assume A16: x in union X ; ::_thesis: x in field Q
then A17: [x,x] in R by A10, RELAT_2:def_1;
 for Z1 being set st Z1 in XX holds
( x in Z1 iff x in Z1 ) ;
then  [x,x] in Q by A14, A16, A17;
hence  x in field Q by RELAT_1:15; ::_thesis: verum
end;
A18: Q is reflexive
proof
let x be set ; :: according to RELAT_2:def_1,RELAT_2:def_9 ::_thesis: ( not x in field Q or [x,x] in Q )
assume A19: x in field Q ; ::_thesis: [x,x] in Q
then A20: [x,x] in R by A10, A15, RELAT_2:def_1;
 for Z1 being set st Z1 in XX holds
( x in Z1 iff x in Z1 ) ;
hence  [x,x] in Q by A14, A15, A19, A20; ::_thesis: verum
end;
A21: Q is transitive
proof
let x be set ; :: according to RELAT_2:def_8,RELAT_2:def_16 ::_thesis: for b1, b2 being set holds
( not x in field Q or not b1 in field Q or not b2 in field Q or not [x,b1] in Q or not [b1,b2] in Q or [x,b2] in Q )
let y, z be set ; ::_thesis: ( not x in field Q or not y in field Q or not z in field Q or not [x,y] in Q or not [y,z] in Q or [x,z] in Q )
assume that
A22: x in field Q and
A23: y in field Q and
A24: z in field Q and
A25: [x,y] in Q and
A26: [y,z] in Q ; ::_thesis: [x,z] in Q
A27: now__::_thesis:_(_ex_Z1_being_set_st_
(_Z1_in_XX_&_x_in_Z1_&_not_y_in_Z1_)_&_ex_Z2_being_set_st_
(_Z2_in_XX_&_y_in_Z2_&_not_z_in_Z2_)_implies_[x,z]_in_Q_)
given Z1 being set  such that A28: Z1 in XX and
A29: x in Z1 and
A30: not y in Z1 ; ::_thesis: ( ex Z2 being set st
( Z2 in XX & y in Z2 & not z in Z2 ) implies [x,z] in Q )
given Z2 being set  such that A31: Z2 in XX and
A32: y in Z2 and
A33: not z in Z2 ; ::_thesis: [x,z] in Q
 ( Z1 c= Z2 or Z2 c= Z1 ) by A6, A28, A31;
hence  [x,z] in Q by A14, A15, A22, A24, A29, A30, A31, A32, A33; ::_thesis: verum
end;
A34: now__::_thesis:_(_ex_Z1_being_set_st_
(_Z1_in_XX_&_x_in_Z1_&_not_y_in_Z1_)_&_(_for_Z1_being_set_st_Z1_in_XX_holds_
(_y_in_Z1_iff_z_in_Z1_)_)_&_[y,z]_in_R_implies_[x,z]_in_Q_)
given Z1 being set  such that A35: Z1 in XX and
A36: x in Z1 and
A37: not y in Z1 ; ::_thesis: ( ( for Z1 being set st Z1 in XX holds
( y in Z1 iff z in Z1 ) ) & [y,z] in R implies [x,z] in Q )
assume that
A38: for Z1 being set st Z1 in XX holds
( y in Z1 iff z in Z1 ) and
 [y,z] in R ; ::_thesis: [x,z] in Q
 not z in Z1 by A35, A37, A38;
hence  [x,z] in Q by A14, A15, A22, A24, A35, A36; ::_thesis: verum
end;
A39: now__::_thesis:_(_ex_Z1_being_set_st_
(_Z1_in_XX_&_y_in_Z1_&_not_z_in_Z1_)_&_(_for_Z1_being_set_st_Z1_in_XX_holds_
(_x_in_Z1_iff_y_in_Z1_)_)_&_[x,y]_in_R_implies_[x,z]_in_Q_)
given Z1 being set  such that A40: Z1 in XX and
A41: y in Z1 and
A42: not z in Z1 ; ::_thesis: ( ( for Z1 being set st Z1 in XX holds
( x in Z1 iff y in Z1 ) ) & [x,y] in R implies [x,z] in Q )
assume that
A43: for Z1 being set st Z1 in XX holds
( x in Z1 iff y in Z1 ) and
 [x,y] in R ; ::_thesis: [x,z] in Q
 x in Z1 by A40, A41, A43;
hence  [x,z] in Q by A14, A15, A22, A24, A40, A42; ::_thesis: verum
end;
now__::_thesis:_(_(_for_Z1_being_set_st_Z1_in_XX_holds_
(_x_in_Z1_iff_y_in_Z1_)_)_&_[x,y]_in_R_&_(_for_Z1_being_set_st_Z1_in_XX_holds_
(_y_in_Z1_iff_z_in_Z1_)_)_&_[y,z]_in_R_implies_[x,z]_in_Q_)
assume that
A44: for Z1 being set st Z1 in XX holds
( x in Z1 iff y in Z1 ) and
A45: [x,y] in R and
A46: for Z1 being set st Z1 in XX holds
( y in Z1 iff z in Z1 ) and
A47: [y,z] in R ; ::_thesis: [x,z] in Q
A48: [x,z] in R by A11, A15, A22, A23, A24, A45, A47, RELAT_2:def_8;
now__::_thesis:_for_Z_being_set_st_Z_in_XX_holds_
(_x_in_Z_iff_z_in_Z_)
let Z be set ; ::_thesis: ( Z in XX implies ( x in Z iff z in Z ) )
assume A49: Z in XX ; ::_thesis: ( x in Z iff z in Z )
then  ( x in Z iff y in Z ) by A44;
hence  ( x in Z iff z in Z ) by A46, A49; ::_thesis: verum
end;
hence  [x,z] in Q by A14, A15, A22, A24, A48; ::_thesis: verum
end;
hence  [x,z] in Q by A14, A25, A26, A27, A34, A39; ::_thesis: verum
end;
A50: Q is antisymmetric
proof
let x be set ; :: according to RELAT_2:def_4,RELAT_2:def_12 ::_thesis: for b1 being set holds
( not x in field Q or not b1 in field Q or not [x,b1] in Q or not [b1,x] in Q or x = b1 )
let y be set ; ::_thesis: ( not x in field Q or not y in field Q or not [x,y] in Q or not [y,x] in Q or x = y )
assume that
A51: x in field Q and
A52: y in field Q and
A53: [x,y] in Q and
A54: [y,x] in Q ; ::_thesis: x = y
A55: ( ex Z1 being set st
( Z1 in XX & x in Z1 & not y in Z1 ) or ( ( for Z1 being set st Z1 in XX holds
( x in Z1 iff y in Z1 ) ) & [x,y] in R ) ) by A14, A53;
A56: ( ex Z1 being set st
( Z1 in XX & y in Z1 & not x in Z1 ) or ( ( for Z1 being set st Z1 in XX holds
( y in Z1 iff x in Z1 ) ) & [y,x] in R ) ) by A14, A54;
now__::_thesis:_(_ex_Z1_being_set_st_
(_Z1_in_XX_&_x_in_Z1_&_not_y_in_Z1_)_&_ex_Z2_being_set_st_
(_Z2_in_XX_&_y_in_Z2_&_not_x_in_Z2_)_implies_x_=_y_)
given Z1 being set  such that A57: Z1 in XX and
A58: x in Z1 and
A59: not y in Z1 ; ::_thesis: ( ex Z2 being set st
( Z2 in XX & y in Z2 & not x in Z2 ) implies x = y )
given Z2 being set  such that A60: Z2 in XX and
A61: y in Z2 and
A62: not x in Z2 ; ::_thesis: x = y
 ( Z1 c= Z2 or Z2 c= Z1 ) by A6, A57, A60;
hence  x = y by A58, A59, A61, A62; ::_thesis: verum
end;
hence  x = y by A12, A15, A51, A52, A55, A56, RELAT_2:def_4; ::_thesis: verum
end;
A63: Q is connected
proof
let x be set ; :: according to RELAT_2:def_6,RELAT_2:def_14 ::_thesis: for b1 being set holds
( not x in field Q or not b1 in field Q or x = b1 or [x,b1] in Q or [b1,x] in Q )
let y be set ; ::_thesis: ( not x in field Q or not y in field Q or x = y or [x,y] in Q or [y,x] in Q )
assume that
A64: x in field Q and
A65: y in field Q and
A66: x <> y ; ::_thesis: ( [x,y] in Q or [y,x] in Q )
now__::_thesis:_(_(_for_Z_being_set_st_Z_in_XX_holds_
(_x_in_Z_iff_y_in_Z_)_)_&_not_[x,y]_in_Q_implies_[y,x]_in_Q_)
assume A67: for Z being set st Z in XX holds
( x in Z iff y in Z ) ; ::_thesis: ( [x,y] in Q or [y,x] in Q )
A68: ( [x,y] in R or [y,x] in R ) by A13, A15, A64, A65, A66, RELAT_2:def_6;
 for Z being set st Z in XX holds
( y in Z iff x in Z ) by A67;
hence  ( [x,y] in Q or [y,x] in Q ) by A14, A15, A64, A65, A67, A68; ::_thesis: verum
end;
hence  ( [x,y] in Q or [y,x] in Q ) by A14, A15, A64, A65; ::_thesis: verum
end;
 Q is well_founded
proof
let Y be set ; :: according to WELLORD1:def_2 ::_thesis: ( not Y c= field Q or Y = {} or ex b1 being set st
( b1 in Y & Q -Seg b1 misses Y ) )
assume that
A69: Y c= field Q and
A70: Y <> {} ; ::_thesis: ex b1 being set st
( b1 in Y & Q -Seg b1 misses Y )
defpred S3[ set ] means $1 /\ Y <> {} ;
consider Z being set  such that
A71: for x being set holds
( x in Z iff ( x in XX & S3[x] ) ) from XBOOLE_0:sch_1();
A72: Z c= XX
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Z or x in XX )
thus  ( not x in Z or x in XX ) by A71; ::_thesis: verum
end;
set x = the Element of Y;
 the Element of Y in union XX by A4, A15, A69, A70, TARSKI:def_3;
then consider Z1 being set  such that
A73: the Element of Y in Z1 and
A74: Z1 in XX by TARSKI:def_4;
 Z1 /\ Y <> {} by A70, A73, XBOOLE_0:def_4;
then  Z <> {} by A71, A74;
then consider Z1 being set  such that
A75: Z1 in Z and
A76: for Z2 being set st Z2 in Z holds
Z1 c= Z2 by A5, A72;
A77: Z1 in XX by A71, A75;
A78: Z1 /\ Y c= Z1 by XBOOLE_1:17;
A79: Z1 c= union X by A3, A77, ZFMISC_1:74;
 Z1 /\ Y <> {} by A71, A75;
then consider x being set  such that
A80: x in Z1 /\ Y and
A81: for y being set st y in Z1 /\ Y holds
[x,y] in R by A9, A78, A79, WELLORD1:5, XBOOLE_1:1;
take  x ; ::_thesis: ( x in Y & Q -Seg x misses Y )
thus  x in Y by A80, XBOOLE_0:def_4; ::_thesis: Q -Seg x misses Y
assume A82: (Q -Seg x) /\ Y <> {} ; :: according to XBOOLE_0:def_7 ::_thesis: contradiction
set y = the Element of (Q -Seg x) /\ Y;
A83: x in Z1 by A80, XBOOLE_0:def_4;
A84: the Element of (Q -Seg x) /\ Y in Q -Seg x by A82, XBOOLE_0:def_4;
A85: the Element of (Q -Seg x) /\ Y in Y by A82, XBOOLE_0:def_4;
A86: the Element of (Q -Seg x) /\ Y <> x by A84, WELLORD1:1;
A87: [ the Element of (Q -Seg x) /\ Y,x] in Q by A84, WELLORD1:1;
A88: now__::_thesis:_for_Z2_being_set_holds_
(_not_Z2_in_XX_or_not_the_Element_of_(Q_-Seg_x)_/\_Y_in_Z2_or_x_in_Z2_)
given Z2 being set  such that A89: Z2 in XX and
A90: the Element of (Q -Seg x) /\ Y in Z2 and
A91: not x in Z2 ; ::_thesis: contradiction
 Z2 /\ Y <> {} by A85, A90, XBOOLE_0:def_4;
then  Z2 in Z by A71, A89;
then  Z1 c= Z2 by A76;
hence  contradiction by A83, A91; ::_thesis: verum
end;
then A92: the Element of (Q -Seg x) /\ Y in Z1 by A14, A77, A83, A87;
A93: [ the Element of (Q -Seg x) /\ Y,x] in R by A14, A87, A88;
 the Element of (Q -Seg x) /\ Y in Z1 /\ Y by A85, A92, XBOOLE_0:def_4;
then A94: [x, the Element of (Q -Seg x) /\ Y] in R by A81;
A95: x in union X by A14, A87;
 the Element of (Q -Seg x) /\ Y in union X by A14, A87;
hence  contradiction by A12, A86, A93, A94, A95, RELAT_2:def_4; ::_thesis: verum
end;
then  Q is well-ordering by A18, A21, A50, A63, WELLORD1:def_4;
then  Q, RelIncl (order_type_of Q) are_isomorphic by WELLORD2:def_2;
then  RelIncl (order_type_of Q),Q are_isomorphic by WELLORD1:40;
then consider g being Function such that
A96: g is_isomorphism_of RelIncl (order_type_of Q),Q by WELLORD1:def_8;
A97: field (RelIncl (order_type_of Q)) = order_type_of Q by WELLORD2:def_1;
then A98: dom g = order_type_of Q by A96, WELLORD1:def_7;
A99: rng g = union X by A15, A96, WELLORD1:def_7;
A100: g is one-to-one by A96, WELLORD1:def_7;
A101: for Z, x being set st Z in XX & x in Z holds
Q -Seg x c= Z
proof
let Z, x be set ; ::_thesis: ( Z in XX & x in Z implies Q -Seg x c= Z )
assume that
A102: Z in XX and
A103: x in Z ; ::_thesis: Q -Seg x c= Z
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in Q -Seg x or y in Z )
assume  y in Q -Seg x ; ::_thesis: y in Z
then A104: [y,x] in Q by WELLORD1:1;
now__::_thesis:_(_ex_Z1_being_set_st_
(_Z1_in_XX_&_y_in_Z1_&_not_x_in_Z1_)_implies_y_in_Z_)
given Z1 being set  such that A105: Z1 in XX and
A106: y in Z1 and
A107: not x in Z1 ; ::_thesis: y in Z
 ( Z1 c= Z or Z c= Z1 ) by A6, A102, A105;
hence  y in Z by A103, A106, A107; ::_thesis: verum
end;
hence  y in Z by A14, A102, A103, A104; ::_thesis: verum
end;
A108: for A being Ordinal st A in order_type_of Q holds
card A = card (Q -Seg (g . A))
proof
let A be Ordinal; ::_thesis: ( A in order_type_of Q implies card A = card (Q -Seg (g . A)) )
assume A109: A in order_type_of Q ; ::_thesis: card A = card (Q -Seg (g . A))
 A,Q -Seg (g . A) are_equipotent
proof
take f = g | A; :: according to WELLORD2:def_4 ::_thesis: ( f is one-to-one & proj1 f = A & proj2 f = Q -Seg (g . A) )
 A c= dom g by A98, A109, ORDINAL1:def_2;
hence A110: ( f is one-to-one & dom f = A ) by A100, FUNCT_1:52, RELAT_1:62; ::_thesis: proj2 f = Q -Seg (g . A)
thus  rng f c= Q -Seg (g . A) :: according to XBOOLE_0:def_10 ::_thesis: Q -Seg (g . A) c= proj2 f
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng f or x in Q -Seg (g . A) )
assume  x in rng f ; ::_thesis: x in Q -Seg (g . A)
then consider y being set  such that
A111: y in dom f and
A112: x = f . y by FUNCT_1:def_3;
reconsider B = y as Ordinal by A110, A111;
A113: B in order_type_of Q by A109, A110, A111, ORDINAL1:10;
 B c= A by A110, A111, ORDINAL1:def_2;
then A114: [B,A] in RelIncl (order_type_of Q) by A109, A113, WELLORD2:def_1;
A115: x = g . B by A111, A112, FUNCT_1:47;
A116: A <> B by A110, A111;
A117: [x,(g . A)] in Q by A96, A114, A115, WELLORD1:def_7;
 x <> g . A by A98, A100, A109, A113, A115, A116, FUNCT_1:def_4;
hence  x in Q -Seg (g . A) by A117, WELLORD1:1; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Q -Seg (g . A) or x in proj2 f )
assume A118: x in Q -Seg (g . A) ; ::_thesis: x in proj2 f
then A119: [x,(g . A)] in Q by WELLORD1:1;
then  x in union X by A14;
then consider y being set  such that
A120: y in dom g and
A121: x = g . y by A99, FUNCT_1:def_3;
reconsider B = y as Ordinal by A98, A120;
 [B,A] in RelIncl (order_type_of Q) by A96, A97, A98, A109, A119, A120, A121, WELLORD1:def_7;
then A122: B c= A by A98, A109, A120, WELLORD2:def_1;
 B <> A by A118, A121, WELLORD1:1;
then  B c< A by A122, XBOOLE_0:def_8;
hence  x in proj2 f by A120, A121, FUNCT_1:50, ORDINAL1:11; ::_thesis: verum
end;
hence  card A = card (Q -Seg (g . A)) by CARD_1:5; ::_thesis: verum
end;
A123: order_type_of Q c= M
proof
let x be Ordinal; :: according to ORDINAL1:def_5 ::_thesis: ( not x in order_type_of Q or x in M )
assume A124: x in order_type_of Q ; ::_thesis: x in M
reconsider A = x as Ordinal ;
 g . x in union X by A98, A99, A124, FUNCT_1:def_3;
then consider Z being set  such that
A125: g . x in Z and
A126: Z in XX by A4, TARSKI:def_4;
A127: card (Q -Seg (g . x)) c= card Z by A101, A125, A126, CARD_1:11;
A128: card (Q -Seg (g . x)) = card A by A108, A124;
 card (Q -Seg (g . x)) in M by A1, A3, A126, A127, ORDINAL1:12;
hence  x in M by A128, Th44; ::_thesis: verum
end;
 order_type_of Q, union X are_equipotent by A98, A99, A100, WELLORD2:def_4;
then A129: card (order_type_of Q) = card (union X) by CARD_1:5;
 card M = M by CARD_1:def_2;
hence  card (union X) c= M by A123, A129, CARD_1:11; ::_thesis: verum
end;

begin

registration
let f be Function;
cluster product f ->  functional ;
coherence
 product f is functional
proof
set d = product f;
let x be set ; :: according to FUNCT_1:def_13 ::_thesis: ( not x in product f or x is set )
assume  x in product f ; ::_thesis: x is set
then  ex g being Function st
( x = g & dom g = dom f & ( for x being set st x in dom f holds
g . x in f . x ) ) by Def5;
hence  x is set ; ::_thesis: verum
end;
end;

registration
let A be set ;
let B be with_non-empty_elements set ;
cluster Function-like quasi_total  ->  non-empty for Element of bool [:A,B:];
coherence
 for b1 being Function of A,B holds b1 is non-empty
proof
let f be Function of A,B; ::_thesis: f is non-empty
thus  not {} in rng f ; :: according to RELAT_1:def_9 ::_thesis: verum
end;
end;

registration
let f be non-empty Function;
cluster product f ->  non empty ;
coherence
 not product f is empty
proof
 not {} in rng f ;
hence  not product f is empty by Th26; ::_thesis: verum
end;
end;

theorem :: CARD_3:47
for a, b, c, d being set st a <> b holds
product ((a,b) --> ({c},{d})) = {((a,b) --> (c,d))}
proof
let a, b, c, d be set ; ::_thesis: ( a <> b implies product ((a,b) --> ({c},{d})) = {((a,b) --> (c,d))} )
assume A1: a <> b ; ::_thesis: product ((a,b) --> ({c},{d})) = {((a,b) --> (c,d))}
set X = {((a,b) --> (c,d))};
set f = (a,b) --> ({c},{d});
A2: dom ((a,b) --> ({c},{d})) = {a,b} by FUNCT_4:62;
now__::_thesis:_for_x_being_set_holds_
(_(_x_in_{((a,b)_-->_(c,d))}_implies_ex_g_being_Function_st_
(_x_=_g_&_dom_g_=_dom_((a,b)_-->_({c},{d}))_&_(_for_x_being_set_st_x_in_dom_((a,b)_-->_({c},{d}))_holds_
g_._x_in_((a,b)_-->_({c},{d}))_._x_)_)_)_&_(_ex_g_being_Function_st_
(_x_=_g_&_dom_g_=_dom_((a,b)_-->_({c},{d}))_&_(_for_x_being_set_st_x_in_dom_((a,b)_-->_({c},{d}))_holds_
g_._x_in_((a,b)_-->_({c},{d}))_._x_)_)_implies_x_in_{((a,b)_-->_(c,d))}_)_)
let x be set ; ::_thesis: ( ( x in {((a,b) --> (c,d))} implies ex g being Function st
( x = g & dom g = dom ((a,b) --> ({c},{d})) & ( for x being set st x in dom ((a,b) --> ({c},{d})) holds
g . x in ((a,b) --> ({c},{d})) . x ) ) ) & ( ex g being Function st
( x = g & dom g = dom ((a,b) --> ({c},{d})) & ( for x being set st x in dom ((a,b) --> ({c},{d})) holds
g . x in ((a,b) --> ({c},{d})) . x ) ) implies x in {((a,b) --> (c,d))} ) )
thus  ( x in {((a,b) --> (c,d))} implies ex g being Function st
( x = g & dom g = dom ((a,b) --> ({c},{d})) & ( for x being set st x in dom ((a,b) --> ({c},{d})) holds
g . x in ((a,b) --> ({c},{d})) . x ) ) ) ::_thesis: ( ex g being Function st
( x = g & dom g = dom ((a,b) --> ({c},{d})) & ( for x being set st x in dom ((a,b) --> ({c},{d})) holds
g . x in ((a,b) --> ({c},{d})) . x ) ) implies x in {((a,b) --> (c,d))} )
proof
assume A3: x in {((a,b) --> (c,d))} ; ::_thesis: ex g being Function st
( x = g & dom g = dom ((a,b) --> ({c},{d})) & ( for x being set st x in dom ((a,b) --> ({c},{d})) holds
g . x in ((a,b) --> ({c},{d})) . x ) )
take g = (a,b) --> (c,d); ::_thesis: ( x = g & dom g = dom ((a,b) --> ({c},{d})) & ( for x being set st x in dom ((a,b) --> ({c},{d})) holds
g . x in ((a,b) --> ({c},{d})) . x ) )
thus  x = g by A3, TARSKI:def_1; ::_thesis: ( dom g = dom ((a,b) --> ({c},{d})) & ( for x being set st x in dom ((a,b) --> ({c},{d})) holds
g . x in ((a,b) --> ({c},{d})) . x ) )
thus  dom g = dom ((a,b) --> ({c},{d})) by A2, FUNCT_4:62; ::_thesis: for x being set st x in dom ((a,b) --> ({c},{d})) holds
g . x in ((a,b) --> ({c},{d})) . x
let x be set ; ::_thesis: ( x in dom ((a,b) --> ({c},{d})) implies g . x in ((a,b) --> ({c},{d})) . x )
assume  x in dom ((a,b) --> ({c},{d})) ; ::_thesis: g . x in ((a,b) --> ({c},{d})) . x
then A4: ( x = a or x = b ) by A2, TARSKI:def_2;
A5: g . a = c by A1, FUNCT_4:63;
A6: ((a,b) --> ({c},{d})) . a = {c} by A1, FUNCT_4:63;
A7: g . b = d by FUNCT_4:63;
 ((a,b) --> ({c},{d})) . b = {d} by FUNCT_4:63;
hence  g . x in ((a,b) --> ({c},{d})) . x by A4, A5, A6, A7, TARSKI:def_1; ::_thesis: verum
end;
given g being Function such that A8: x = g and
A9: dom g = dom ((a,b) --> ({c},{d})) and
A10: for x being set st x in dom ((a,b) --> ({c},{d})) holds
g . x in ((a,b) --> ({c},{d})) . x ; ::_thesis: x in {((a,b) --> (c,d))}
A11: a in dom ((a,b) --> ({c},{d})) by A2, TARSKI:def_2;
A12: b in dom ((a,b) --> ({c},{d})) by A2, TARSKI:def_2;
A13: g . a in ((a,b) --> ({c},{d})) . a by A10, A11;
A14: g . b in ((a,b) --> ({c},{d})) . b by A10, A12;
A15: ((a,b) --> ({c},{d})) . a = {c} by A1, FUNCT_4:63;
A16: ((a,b) --> ({c},{d})) . b = {d} by FUNCT_4:63;
A17: g . a = c by A13, A15, TARSKI:def_1;
 g . b = d by A14, A16, TARSKI:def_1;
then  g = (a,b) --> (c,d) by A2, A9, A17, FUNCT_4:66;
hence  x in {((a,b) --> (c,d))} by A8, TARSKI:def_1; ::_thesis: verum
end;
hence  product ((a,b) --> ({c},{d})) = {((a,b) --> (c,d))} by Def5; ::_thesis: verum
end;

theorem :: CARD_3:48
for x being set
for f being Function st x in product f holds
x is Function ;

begin


definition
let f be Function;
func sproduct f ->  set  means :Def9: :: CARD_3:def 9
 for x being set holds
( x in it iff ex g being Function st
( x = g & dom g c= dom f & ( for x being set st x in dom g holds
g . x in f . x ) ) );
existence
 ex b1 being set st
for x being set holds
( x in b1 iff ex g being Function st
( x = g & dom g c= dom f & ( for x being set st x in dom g holds
g . x in f . x ) ) )
proof
defpred S2[ set ] means  ex g being Function st
( $1 = g & dom g c= dom f & ( for x being set st x in dom g holds
g . x in f . x ) );
consider A being set  such that
A1: for x being set holds
( x in A iff ( x in PFuncs ((dom f),(union (rng f))) & S2[x] ) ) from XBOOLE_0:sch_1();
now__::_thesis:_for_x_being_set_holds_
(_(_x_in_A_implies_ex_g_being_Function_st_
(_x_=_g_&_dom_g_c=_dom_f_&_(_for_x_being_set_st_x_in_dom_g_holds_
g_._x_in_f_._x_)_)_)_&_(_ex_g_being_Function_st_
(_x_=_g_&_dom_g_c=_dom_f_&_(_for_x_being_set_st_x_in_dom_g_holds_
g_._x_in_f_._x_)_)_implies_x_in_A_)_)
let x be set ; ::_thesis: ( ( x in A implies ex g being Function st
( x = g & dom g c= dom f & ( for x being set st x in dom g holds
g . x in f . x ) ) ) & ( ex g being Function st
( x = g & dom g c= dom f & ( for x being set st x in dom g holds
g . x in f . x ) ) implies x in A ) )
thus  ( x in A implies ex g being Function st
( x = g & dom g c= dom f & ( for x being set st x in dom g holds
g . x in f . x ) ) ) by A1; ::_thesis: ( ex g being Function st
( x = g & dom g c= dom f & ( for x being set st x in dom g holds
g . x in f . x ) ) implies x in A )
given g being Function such that A2: x = g and
A3: dom g c= dom f and
A4: for x being set st x in dom g holds
g . x in f . x ; ::_thesis: x in A
 rng g c= union (rng f)
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng g or y in union (rng f) )
assume  y in rng g ; ::_thesis: y in union (rng f)
then consider z being set  such that
A5: z in dom g and
A6: y = g . z by FUNCT_1:def_3;
A7: g . z in f . z by A4, A5;
 f . z in rng f by A3, A5, FUNCT_1:def_3;
hence  y in union (rng f) by A6, A7, TARSKI:def_4; ::_thesis: verum
end;
then  x in PFuncs ((dom f),(union (rng f))) by A2, A3, PARTFUN1:def_3;
hence  x in A by A1, A2, A3, A4; ::_thesis: verum
end;
hence  ex b1 being set st
for x being set holds
( x in b1 iff ex g being Function st
( x = g & dom g c= dom f & ( for x being set st x in dom g holds
g . x in f . x ) ) ) ; ::_thesis: verum
end;
uniqueness
 for b1, b2 being set st ( for x being set holds
( x in b1 iff ex g being Function st
( x = g & dom g c= dom f & ( for x being set st x in dom g holds
g . x in f . x ) ) ) ) & ( for x being set holds
( x in b2 iff ex g being Function st
( x = g & dom g c= dom f & ( for x being set st x in dom g holds
g . x in f . x ) ) ) ) holds
b1 = b2
proof
defpred S2[ set ] means  ex g being Function st
( $1 = g & dom g c= dom f & ( for x being set st x in dom g holds
g . x in f . x ) );
let A, B be set ; ::_thesis: ( ( for x being set holds
( x in A iff ex g being Function st
( x = g & dom g c= dom f & ( for x being set st x in dom g holds
g . x in f . x ) ) ) ) & ( for x being set holds
( x in B iff ex g being Function st
( x = g & dom g c= dom f & ( for x being set st x in dom g holds
g . x in f . x ) ) ) ) implies A = B )
assume that
A8: for x being set holds
( x in A iff S2[x] ) and
A9: for x being set holds
( x in B iff S2[x] ) ; ::_thesis: A = B
thus  A = B from XBOOLE_0:sch_2(A8, A9); ::_thesis: verum
end;
end;

:: deftheorem Def9 defines sproduct CARD_3:def_9_:_
 for f being Function
for b2 being set holds
( b2 = sproduct f iff for x being set holds
( x in b2 iff ex g being Function st
( x = g & dom g c= dom f & ( for x being set st x in dom g holds
g . x in f . x ) ) ) );

registration
let f be Function;
cluster sproduct f ->  non empty functional ;
coherence
 ( sproduct f is functional & not sproduct f is empty )
proof
defpred S2[ set ] means  ex g being Function st
( f = g & dom g c= dom f & ( for x being set st x in dom g holds
g . x in f . x ) );
consider A being set  such that
A1: for x being set holds
( x in A iff ( x in PFuncs ((dom f),(union (rng f))) & S2[x] ) ) from XBOOLE_0:sch_1();
 {} is PartFunc of (dom f),(union (rng f)) by RELSET_1:12;
then A2: {} in PFuncs ((dom f),(union (rng f))) by PARTFUN1:45;
A3: dom {} c= dom f by XBOOLE_1:2;
A4: for x being set st x in dom {} holds
{} . x in f . x ;
now__::_thesis:_for_x_being_set_st_x_in_A_holds_
x_is_Function
let x be set ; ::_thesis: ( x in A implies x is Function )
assume  x in A ; ::_thesis: x is Function
then  ex g being Function st
( x = g & dom g c= dom f & ( for x being set st x in dom g holds
g . x in f . x ) ) by A1;
hence  x is Function ; ::_thesis: verum
end;
then reconsider A = A as non empty functional set by A1, A2, A3, A4, FUNCT_1:def_13;
now__::_thesis:_for_x_being_set_holds_
(_(_x_in_A_implies_ex_g_being_Function_st_
(_x_=_g_&_dom_g_c=_dom_f_&_(_for_x_being_set_st_x_in_dom_g_holds_
g_._x_in_f_._x_)_)_)_&_(_ex_g_being_Function_st_
(_x_=_g_&_dom_g_c=_dom_f_&_(_for_x_being_set_st_x_in_dom_g_holds_
g_._x_in_f_._x_)_)_implies_x_in_A_)_)
let x be set ; ::_thesis: ( ( x in A implies ex g being Function st
( x = g & dom g c= dom f & ( for x being set st x in dom g holds
g . x in f . x ) ) ) & ( ex g being Function st
( x = g & dom g c= dom f & ( for x being set st x in dom g holds
g . x in f . x ) ) implies x in A ) )
thus  ( x in A implies ex g being Function st
( x = g & dom g c= dom f & ( for x being set st x in dom g holds
g . x in f . x ) ) ) by A1; ::_thesis: ( ex g being Function st
( x = g & dom g c= dom f & ( for x being set st x in dom g holds
g . x in f . x ) ) implies x in A )
given g being Function such that A5: x = g and
A6: dom g c= dom f and
A7: for x being set st x in dom g holds
g . x in f . x ; ::_thesis: x in A
 rng g c= union (rng f)
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng g or y in union (rng f) )
assume  y in rng g ; ::_thesis: y in union (rng f)
then consider z being set  such that
A8: z in dom g and
A9: y = g . z by FUNCT_1:def_3;
A10: g . z in f . z by A7, A8;
 f . z in rng f by A6, A8, FUNCT_1:def_3;
hence  y in union (rng f) by A9, A10, TARSKI:def_4; ::_thesis: verum
end;
then  x in PFuncs ((dom f),(union (rng f))) by A5, A6, PARTFUN1:def_3;
hence  x in A by A1, A5, A6, A7; ::_thesis: verum
end;
hence  ( sproduct f is functional & not sproduct f is empty ) by Def9; ::_thesis: verum
end;
end;

theorem Th49: :: CARD_3:49
for g, f being Function st g in sproduct f holds
( dom g c= dom f & ( for x being set st x in dom g holds
g . x in f . x ) )
proof
let g, f be Function; ::_thesis: ( g in sproduct f implies ( dom g c= dom f & ( for x being set st x in dom g holds
g . x in f . x ) ) )
assume  g in sproduct f ; ::_thesis: ( dom g c= dom f & ( for x being set st x in dom g holds
g . x in f . x ) )
then  ex h being Function st
( g = h & dom h c= dom f & ( for x being set st x in dom h holds
h . x in f . x ) ) by Def9;
hence  ( dom g c= dom f & ( for x being set st x in dom g holds
g . x in f . x ) ) ; ::_thesis: verum
end;

theorem Th50: :: CARD_3:50
for f being Function holds {} in sproduct f
proof
let f be Function; ::_thesis: {} in sproduct f
A1: dom {} c= dom f by XBOOLE_1:2;
 for x being set st x in dom {} holds
{} . x in f . x ;
hence  {} in sproduct f by A1, Def9; ::_thesis: verum
end;

registration
let f be Function;
cluster empty Relation-like Function-like for Element of sproduct f;
existence
 ex b1 being Element of sproduct f st b1 is empty
proof
 {} in sproduct f by Th50;
hence  ex b1 being Element of sproduct f st b1 is empty ; ::_thesis: verum
end;
end;

theorem Th51: :: CARD_3:51
for f being Function holds product f c= sproduct f
proof
let f be Function; ::_thesis: product f c= sproduct f
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in product f or x in sproduct f )
assume  x in product f ; ::_thesis: x in sproduct f
then  ex g being Function st
( x = g & dom g = dom f & ( for x being set st x in dom f holds
g . x in f . x ) ) by Def5;
hence  x in sproduct f by Def9; ::_thesis: verum
end;

theorem Th52: :: CARD_3:52
for x being set
for f being Function st x in sproduct f holds
x is PartFunc of (dom f),(union (rng f))
proof
let x be set ; ::_thesis: for f being Function st x in sproduct f holds
x is PartFunc of (dom f),(union (rng f))
let f be Function; ::_thesis: ( x in sproduct f implies x is PartFunc of (dom f),(union (rng f)) )
assume  x in sproduct f ; ::_thesis: x is PartFunc of (dom f),(union (rng f))
then consider g being Function such that
A1: x = g and
A2: dom g c= dom f and
A3: for x being set st x in dom g holds
g . x in f . x by Def9;
 rng g c= union (rng f)
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng g or y in union (rng f) )
assume  y in rng g ; ::_thesis: y in union (rng f)
then consider z being set  such that
A4: z in dom g and
A5: y = g . z by FUNCT_1:def_3;
A6: g . z in f . z by A3, A4;
 f . z in rng f by A2, A4, FUNCT_1:def_3;
hence  y in union (rng f) by A5, A6, TARSKI:def_4; ::_thesis: verum
end;
hence  x is PartFunc of (dom f),(union (rng f)) by A1, A2, RELSET_1:4; ::_thesis: verum
end;

theorem Th53: :: CARD_3:53
for g, f, h being Function st g in product f & h in sproduct f holds
g +* h in product f
proof
let g, f, h be Function; ::_thesis: ( g in product f & h in sproduct f implies g +* h in product f )
assume A1: g in product f ; ::_thesis: ( not h in sproduct f or g +* h in product f )
then A2: dom g = dom f by Th9;
assume A3: h in sproduct f ; ::_thesis: g +* h in product f
then A4: (dom g) \/ (dom h) = dom f by A2, Th49, XBOOLE_1:12;
then A5: dom (g +* h) = dom f by FUNCT_4:def_1;
now__::_thesis:_for_x_being_set_st_x_in_dom_f_holds_
(g_+*_h)_._x_in_f_._x
let x be set ; ::_thesis: ( x in dom f implies (g +* h) . x in f . x )
assume A6: x in dom f ; ::_thesis: (g +* h) . x in f . x
A7: ((dom g) \ (dom h)) \/ (dom h) = dom f by A4, XBOOLE_1:39;
now__::_thesis:_(_(_x_in_(dom_g)_\_(dom_h)_&_x_in_dom_f_&_(g_+*_h)_._x_=_g_._x_)_or_(_x_in_dom_h_&_(g_+*_h)_._x_=_h_._x_)_)
percases ( x in (dom g) \ (dom h) or x in dom h ) by A6, A7, XBOOLE_0:def_3;
caseA8: x in (dom g) \ (dom h) ; ::_thesis: ( x in dom f & (g +* h) . x = g . x )
then  not x in dom h by XBOOLE_0:def_5;
hence  ( x in dom f & (g +* h) . x = g . x ) by A2, A8, FUNCT_4:11; ::_thesis: verum
end;
case x in dom h ; ::_thesis: (g +* h) . x = h . x
hence  (g +* h) . x = h . x by FUNCT_4:13; ::_thesis: verum
end;
end;
end;
hence  (g +* h) . x in f . x by A1, A3, Th9, Th49; ::_thesis: verum
end;
hence  g +* h in product f by A5, Th9; ::_thesis: verum
end;

theorem :: CARD_3:54
for f, g being Function st product f <> {} holds
( g in sproduct f iff ex h being Function st
( h in product f & g c= h ) )
proof
let f, g be Function; ::_thesis: ( product f <> {} implies ( g in sproduct f iff ex h being Function st
( h in product f & g c= h ) ) )
assume A1: product f <> {} ; ::_thesis: ( g in sproduct f iff ex h being Function st
( h in product f & g c= h ) )
thus  ( g in sproduct f implies ex h being Function st
( h in product f & g c= h ) ) ::_thesis: ( ex h being Function st
( h in product f & g c= h ) implies g in sproduct f )
proof
assume A2: g in sproduct f ; ::_thesis: ex h being Function st
( h in product f & g c= h )
set k = the Element of product f;
reconsider k = the Element of product f as Function ;
take  k +* g ; ::_thesis: ( k +* g in product f & g c= k +* g )
thus  k +* g in product f by A1, A2, Th53; ::_thesis: g c= k +* g
thus  g c= k +* g by FUNCT_4:25; ::_thesis: verum
end;
given h being Function such that A3: h in product f and
A4: g c= h ; ::_thesis: g in sproduct f
A5: dom h = dom f by A3, Th9;
A6: dom g c= dom h by A4, RELAT_1:11;
now__::_thesis:_for_x_being_set_st_x_in_dom_g_holds_
g_._x_in_f_._x
let x be set ; ::_thesis: ( x in dom g implies g . x in f . x )
assume A7: x in dom g ; ::_thesis: g . x in f . x
then  g . x = h . x by A4, GRFUNC_1:2;
hence  g . x in f . x by A3, A5, A6, A7, Th9; ::_thesis: verum
end;
hence  g in sproduct f by A5, A6, Def9; ::_thesis: verum
end;

theorem Th55: :: CARD_3:55
for f being Function holds sproduct f c= PFuncs ((dom f),(union (rng f)))
proof
let f be Function; ::_thesis: sproduct f c= PFuncs ((dom f),(union (rng f)))
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in sproduct f or x in PFuncs ((dom f),(union (rng f))) )
assume  x in sproduct f ; ::_thesis: x in PFuncs ((dom f),(union (rng f)))
then  x is PartFunc of (dom f),(union (rng f)) by Th52;
hence  x in PFuncs ((dom f),(union (rng f))) by PARTFUN1:45; ::_thesis: verum
end;

theorem Th56: :: CARD_3:56
for f, g being Function st f c= g holds
sproduct f c= sproduct g
proof
let f, g be Function; ::_thesis: ( f c= g implies sproduct f c= sproduct g )
assume A1: f c= g ; ::_thesis: sproduct f c= sproduct g
then A2: dom f c= dom g by GRFUNC_1:2;
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in sproduct f or y in sproduct g )
assume  y in sproduct f ; ::_thesis: y in sproduct g
then consider h being Function such that
A3: y = h and
A4: dom h c= dom f and
A5: for x being set st x in dom h holds
h . x in f . x by Def9;
A6: dom h c= dom g by A2, A4, XBOOLE_1:1;
now__::_thesis:_for_x_being_set_st_x_in_dom_h_holds_
h_._x_in_g_._x
let x be set ; ::_thesis: ( x in dom h implies h . x in g . x )
assume A7: x in dom h ; ::_thesis: h . x in g . x
then  f . x = g . x by A1, A4, GRFUNC_1:2;
hence  h . x in g . x by A5, A7; ::_thesis: verum
end;
hence  y in sproduct g by A3, A6, Def9; ::_thesis: verum
end;

theorem Th57: :: CARD_3:57
sproduct {} = {{}}
proof
 sproduct {} c= PFuncs ({},{}) by Th55, RELAT_1:38, ZFMISC_1:2;
hence  sproduct {} c= {{}} by PARTFUN1:48; :: according to XBOOLE_0:def_10 ::_thesis: {{}} c= sproduct {}
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {{}} or x in sproduct {} )
assume  x in {{}} ; ::_thesis: x in sproduct {}
then  x = {} by TARSKI:def_1;
hence  x in sproduct {} by Th50; ::_thesis: verum
end;

theorem :: CARD_3:58
for A, B being set holds PFuncs (A,B) = sproduct (A --> B)
proof
let A, B be set ; ::_thesis: PFuncs (A,B) = sproduct (A --> B)
now__::_thesis:_(_(_A_=_{}_&_PFuncs_(A,B)_=_sproduct_(A_-->_B)_)_or_(_A_<>_{}_&_PFuncs_(A,B)_c=_sproduct_(A_-->_B)_&_sproduct_(A_-->_B)_c=_PFuncs_(A,B)_)_)
percases ( A = {} or A <> {} ) ;
caseA1: A = {} ; ::_thesis: PFuncs (A,B) = sproduct (A --> B)
then  A --> B = {} --> B ;
hence  PFuncs (A,B) = sproduct (A --> B) by A1, Th57, PARTFUN1:48; ::_thesis: verum
end;
case A <> {} ; ::_thesis: ( PFuncs (A,B) c= sproduct (A --> B) & sproduct (A --> B) c= PFuncs (A,B) )
then A2: rng (A --> B) = {B} by FUNCOP_1:8;
A3: dom (A --> B) = A by FUNCOP_1:13;
A4: B = union (rng (A --> B)) by A2, ZFMISC_1:25;
thus  PFuncs (A,B) c= sproduct (A --> B) ::_thesis: sproduct (A --> B) c= PFuncs (A,B)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in PFuncs (A,B) or x in sproduct (A --> B) )
assume  x in PFuncs (A,B) ; ::_thesis: x in sproduct (A --> B)
then consider f being Function such that
A5: x = f and
A6: dom f c= A and
A7: rng f c= B by PARTFUN1:def_3;
A8: dom f c= dom (A --> B) by A6, FUNCOP_1:13;
now__::_thesis:_for_x_being_set_st_x_in_dom_f_holds_
f_._x_in_(A_-->_B)_._x
let x be set ; ::_thesis: ( x in dom f implies f . x in (A --> B) . x )
assume A9: x in dom f ; ::_thesis: f . x in (A --> B) . x
then  f . x in rng f by FUNCT_1:def_3;
then  f . x in B by A7;
hence  f . x in (A --> B) . x by A6, A9, FUNCOP_1:7; ::_thesis: verum
end;
hence  x in sproduct (A --> B) by A5, A8, Def9; ::_thesis: verum
end;
thus  sproduct (A --> B) c= PFuncs (A,B) by A3, A4, Th55; ::_thesis: verum
end;
end;
end;
hence  PFuncs (A,B) = sproduct (A --> B) by XBOOLE_0:def_10; ::_thesis: verum
end;

theorem :: CARD_3:59
for A, B being non empty set
for f being Function of A,B holds sproduct f = sproduct (f |  {  x where x is Element of A : f . x <> {}  }  )
proof
let A, B be non empty set ; ::_thesis: for f being Function of A,B holds sproduct f = sproduct (f |  {  x where x is Element of A : f . x <> {}  }  )
let f be Function of A,B; ::_thesis: sproduct f = sproduct (f |  {  x where x is Element of A : f . x <> {}  }  )
set X =  {  x where x is Element of A : f . x <> {}  }  ;
thus  sproduct f c= sproduct (f |  {  x where x is Element of A : f . x <> {}  }  ) :: according to XBOOLE_0:def_10 ::_thesis: sproduct (f |  {  x where x is Element of A : f . x <> {}  }  ) c= sproduct f
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in sproduct f or x in sproduct (f |  {  x where x is Element of A : f . x <> {}  }  ) )
assume  x in sproduct f ; ::_thesis: x in sproduct (f |  {  x where x is Element of A : f . x <> {}  }  )
then consider g being Function such that
A1: x = g and
A2: dom g c= dom f and
A3: for x being set st x in dom g holds
g . x in f . x by Def9;
A4: now__::_thesis:_for_x_being_set_st_x_in_dom_g_holds_
x_in__{__x_where_x_is_Element_of_A_:_f_._x_<>_{}__}_
let x be set ; ::_thesis: ( x in dom g implies x in  {  x where x is Element of A : f . x <> {}  }  )
assume A5: x in dom g ; ::_thesis: x in  {  x where x is Element of A : f . x <> {}  }
then reconsider a = x as Element of A by A2, FUNCT_2:def_1;
 f . a <> {} by A3, A5;
hence  x in  {  x where x is Element of A : f . x <> {}  }  ; ::_thesis: verum
end;
A6: now__::_thesis:_for_x_being_set_st_x_in_dom_g_holds_
x_in_(dom_f)_/\__{__x_where_x_is_Element_of_A_:_f_._x_<>_{}__}_
let x be set ; ::_thesis: ( x in dom g implies x in (dom f) /\  {  x where x is Element of A : f . x <> {}  }  )
assume A7: x in dom g ; ::_thesis: x in (dom f) /\  {  x where x is Element of A : f . x <> {}  }
then  x in  {  x where x is Element of A : f . x <> {}  }  by A4;
hence  x in (dom f) /\  {  x where x is Element of A : f . x <> {}  }  by A2, A7, XBOOLE_0:def_4; ::_thesis: verum
end;
A8: dom g c= dom (f |  {  x where x is Element of A : f . x <> {}  }  )
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in dom g or x in dom (f |  {  x where x is Element of A : f . x <> {}  }  ) )
assume  x in dom g ; ::_thesis: x in dom (f |  {  x where x is Element of A : f . x <> {}  }  )
then  x in (dom f) /\  {  x where x is Element of A : f . x <> {}  }  by A6;
hence  x in dom (f |  {  x where x is Element of A : f . x <> {}  }  ) by RELAT_1:61; ::_thesis: verum
end;
now__::_thesis:_for_x_being_set_st_x_in_dom_g_holds_
g_._x_in_(f_|__{__x_where_x_is_Element_of_A_:_f_._x_<>_{}__}__)_._x
let x be set ; ::_thesis: ( x in dom g implies g . x in (f |  {  x where x is Element of A : f . x <> {}  }  ) . x )
assume A9: x in dom g ; ::_thesis: g . x in (f |  {  x where x is Element of A : f . x <> {}  }  ) . x
then  g . x in f . x by A3;
hence  g . x in (f |  {  x where x is Element of A : f . x <> {}  }  ) . x by A6, A9, FUNCT_1:48; ::_thesis: verum
end;
hence  x in sproduct (f |  {  x where x is Element of A : f . x <> {}  }  ) by A1, A8, Def9; ::_thesis: verum
end;
thus  sproduct (f |  {  x where x is Element of A : f . x <> {}  }  ) c= sproduct f by Th56, RELAT_1:59; ::_thesis: verum
end;

theorem Th60: :: CARD_3:60
for x, y being set
for f being Function st x in dom f & y in f . x holds
x .--> y in sproduct f
proof
let x, y be set ; ::_thesis: for f being Function st x in dom f & y in f . x holds
x .--> y in sproduct f
let f be Function; ::_thesis: ( x in dom f & y in f . x implies x .--> y in sproduct f )
assume that
A1: x in dom f and
A2: y in f . x ; ::_thesis: x .--> y in sproduct f
 dom (x .--> y) = {x} by FUNCOP_1:13;
then A3: dom (x .--> y) c= dom f by A1, ZFMISC_1:31;
now__::_thesis:_for_z_being_set_st_z_in_dom_(x_.-->_y)_holds_
(x_.-->_y)_._z_in_f_._z
let z be set ; ::_thesis: ( z in dom (x .--> y) implies (x .--> y) . z in f . z )
assume  z in dom (x .--> y) ; ::_thesis: (x .--> y) . z in f . z
then  z = x by TARSKI:def_1;
hence  (x .--> y) . z in f . z by A2, FUNCOP_1:72; ::_thesis: verum
end;
hence  x .--> y in sproduct f by A3, Def9; ::_thesis: verum
end;

theorem :: CARD_3:61
for f being Function holds
( sproduct f = {{}} iff for x being set st x in dom f holds
f . x = {} )
proof
let f be Function; ::_thesis: ( sproduct f = {{}} iff for x being set st x in dom f holds
f . x = {} )
thus  ( sproduct f = {{}} implies for x being set st x in dom f holds
f . x = {} ) ::_thesis: ( ( for x being set st x in dom f holds
f . x = {} ) implies sproduct f = {{}} )
proof
assume A1: sproduct f = {{}} ; ::_thesis: for x being set st x in dom f holds
f . x = {}
let x be set ; ::_thesis: ( x in dom f implies f . x = {} )
assume A2: x in dom f ; ::_thesis: f . x = {}
assume A3: f . x <> {} ; ::_thesis: contradiction
set y = the Element of f . x;
 x .--> the Element of f . x in sproduct f by A2, A3, Th60;
hence  contradiction by A1, TARSKI:def_1; ::_thesis: verum
end;
assume A4: for x being set st x in dom f holds
f . x = {} ; ::_thesis: sproduct f = {{}}
now__::_thesis:_for_x_being_set_holds_
(_(_x_in_sproduct_f_implies_x_=_{}_)_&_(_x_=_{}_implies_x_in_sproduct_f_)_)
let x be set ; ::_thesis: ( ( x in sproduct f implies x = {} ) & ( x = {} implies x in sproduct f ) )
thus  ( x in sproduct f implies x = {} ) ::_thesis: ( x = {} implies x in sproduct f )
proof
assume  x in sproduct f ; ::_thesis: x = {}
then consider g being Function such that
A5: x = g and
A6: dom g c= dom f and
A7: for y being set st y in dom g holds
g . y in f . y by Def9;
assume A8: x <> {} ; ::_thesis: contradiction
set y = the Element of dom g;
A9: f . the Element of dom g <> {} by A5, A7, A8;
 the Element of dom g in dom f by A5, A6, A8, TARSKI:def_3;
hence  contradiction by A4, A9; ::_thesis: verum
end;
thus  ( x = {} implies x in sproduct f ) by Th50; ::_thesis: verum
end;
hence  sproduct f = {{}} by TARSKI:def_1; ::_thesis: verum
end;

theorem Th62: :: CARD_3:62
for f being Function
for A being set st A c= sproduct f & ( for h1, h2 being Function st h1 in A & h2 in A holds
h1 tolerates h2 ) holds
union A in sproduct f
proof
let f be Function; ::_thesis: for A being set st A c= sproduct f & ( for h1, h2 being Function st h1 in A & h2 in A holds
h1 tolerates h2 ) holds
union A in sproduct f
let A be set ; ::_thesis: ( A c= sproduct f & ( for h1, h2 being Function st h1 in A & h2 in A holds
h1 tolerates h2 ) implies union A in sproduct f )
assume that
A1: A c= sproduct f and
A2: for h1, h2 being Function st h1 in A & h2 in A holds
h1 tolerates h2 ; ::_thesis: union A in sproduct f
reconsider g = union A as Function by A1, A2, PARTFUN1:78;
A3: dom g c= dom f
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in dom g or x in dom f )
assume  x in dom g ; ::_thesis: x in dom f
then consider y being set  such that
A4: [x,y] in g by XTUPLE_0:def_12;
consider h being set  such that
A5: [x,y] in h and
A6: h in A by A4, TARSKI:def_4;
reconsider h = h as Function by A1, A6;
A7: x in dom h by A5, XTUPLE_0:def_12;
 dom h c= dom f by A1, A6, Th49;
hence  x in dom f by A7; ::_thesis: verum
end;
now__::_thesis:_for_x_being_set_st_x_in_dom_g_holds_
g_._x_in_f_._x
let x be set ; ::_thesis: ( x in dom g implies g . x in f . x )
assume  x in dom g ; ::_thesis: g . x in f . x
then consider y being set  such that
A8: [x,y] in g by XTUPLE_0:def_12;
consider h being set  such that
A9: [x,y] in h and
A10: h in A by A8, TARSKI:def_4;
reconsider h = h as Function by A1, A10;
A11: x in dom h by A9, XTUPLE_0:def_12;
h . x = y by A9, FUNCT_1:1
.= g . x by A8, FUNCT_1:1 ;
hence  g . x in f . x by A1, A10, A11, Th49; ::_thesis: verum
end;
hence  union A in sproduct f by A3, Def9; ::_thesis: verum
end;

theorem :: CARD_3:63
for g, h, f being Function st g tolerates h & g in sproduct f & h in sproduct f holds
g \/ h in sproduct f
proof
let g, h, f be Function; ::_thesis: ( g tolerates h & g in sproduct f & h in sproduct f implies g \/ h in sproduct f )
assume that
A1: g tolerates h and
A2: g in sproduct f and
A3: h in sproduct f ; ::_thesis: g \/ h in sproduct f
A4: {g,h} c= sproduct f by A2, A3, ZFMISC_1:32;
A5: now__::_thesis:_for_h1,_h2_being_Function_st_h1_in_{g,h}_&_h2_in_{g,h}_holds_
h1_tolerates_h2
let h1, h2 be Function; ::_thesis: ( h1 in {g,h} & h2 in {g,h} implies h1 tolerates h2 )
assume that
A6: h1 in {g,h} and
A7: h2 in {g,h} ; ::_thesis: h1 tolerates h2
A8: ( h1 = g or h1 = h ) by A6, TARSKI:def_2;
 ( h2 = g or h2 = h ) by A7, TARSKI:def_2;
hence  h1 tolerates h2 by A1, A8; ::_thesis: verum
end;
 union {g,h} = g \/ h by ZFMISC_1:75;
hence  g \/ h in sproduct f by A4, A5, Th62; ::_thesis: verum
end;

theorem Th64: :: CARD_3:64
for x being set
for h, f being Function st x c= h & h in sproduct f holds
x in sproduct f
proof
let x be set ; ::_thesis: for h, f being Function st x c= h & h in sproduct f holds
x in sproduct f
let h, f be Function; ::_thesis: ( x c= h & h in sproduct f implies x in sproduct f )
assume that
A1: x c= h and
A2: h in sproduct f ; ::_thesis: x in sproduct f
reconsider g = x as Function by A1;
A3: dom g c= dom h by A1, GRFUNC_1:2;
 dom h c= dom f by A2, Th49;
then A4: dom g c= dom f by A3, XBOOLE_1:1;
now__::_thesis:_for_x_being_set_st_x_in_dom_g_holds_
g_._x_in_f_._x
let x be set ; ::_thesis: ( x in dom g implies g . x in f . x )
assume A5: x in dom g ; ::_thesis: g . x in f . x
then  h . x in f . x by A2, A3, Th49;
hence  g . x in f . x by A1, A5, GRFUNC_1:2; ::_thesis: verum
end;
hence  x in sproduct f by A4, Def9; ::_thesis: verum
end;

theorem Th65: :: CARD_3:65
for g, f being Function
for A being set st g in sproduct f holds
g | A in sproduct f by Th64, RELAT_1:59;

theorem Th66: :: CARD_3:66
for g, f being Function
for A being set st g in sproduct f holds
g | A in sproduct (f | A)
proof
let g, f be Function; ::_thesis: for A being set st g in sproduct f holds
g | A in sproduct (f | A)
let A be set ; ::_thesis: ( g in sproduct f implies g | A in sproduct (f | A) )
A1: dom (g | A) = (dom g) /\ A by RELAT_1:61;
A2: dom (f | A) = (dom f) /\ A by RELAT_1:61;
assume A3: g in sproduct f ; ::_thesis: g | A in sproduct (f | A)
then A4: dom (g | A) c= dom (f | A) by A1, A2, Th49, XBOOLE_1:26;
now__::_thesis:_for_x_being_set_st_x_in_dom_(g_|_A)_holds_
(g_|_A)_._x_in_(f_|_A)_._x
let x be set ; ::_thesis: ( x in dom (g | A) implies (g | A) . x in (f | A) . x )
assume A5: x in dom (g | A) ; ::_thesis: (g | A) . x in (f | A) . x
then A6: (g | A) . x = g . x by FUNCT_1:47;
A7: (f | A) . x = f . x by A4, A5, FUNCT_1:47;
 x in dom g by A1, A5, XBOOLE_0:def_4;
hence  (g | A) . x in (f | A) . x by A3, A6, A7, Th49; ::_thesis: verum
end;
hence  g | A in sproduct (f | A) by A4, Def9; ::_thesis: verum
end;

theorem :: CARD_3:67
for h, f, g being Function st h in sproduct (f +* g) holds
ex f9, g9 being Function st
( f9 in sproduct f & g9 in sproduct g & h = f9 +* g9 )
proof
let h, f, g be Function; ::_thesis: ( h in sproduct (f +* g) implies ex f9, g9 being Function st
( f9 in sproduct f & g9 in sproduct g & h = f9 +* g9 ) )
assume A1: h in sproduct (f +* g) ; ::_thesis: ex f9, g9 being Function st
( f9 in sproduct f & g9 in sproduct g & h = f9 +* g9 )
take  h | ((dom f) \ (dom g)) ; ::_thesis: ex g9 being Function st
( h | ((dom f) \ (dom g)) in sproduct f & g9 in sproduct g & h = (h | ((dom f) \ (dom g))) +* g9 )
take  h | (dom g) ; ::_thesis: ( h | ((dom f) \ (dom g)) in sproduct f & h | (dom g) in sproduct g & h = (h | ((dom f) \ (dom g))) +* (h | (dom g)) )
A2: h | ((dom f) \ (dom g)) in sproduct ((f +* g) | ((dom f) \ (dom g))) by A1, Th66;
 sproduct ((f +* g) | ((dom f) \ (dom g))) c= sproduct f by Th56, FUNCT_4:24;
hence  h | ((dom f) \ (dom g)) in sproduct f by A2; ::_thesis: ( h | (dom g) in sproduct g & h = (h | ((dom f) \ (dom g))) +* (h | (dom g)) )
 (f +* g) | (dom g) = g by FUNCT_4:23;
hence  h | (dom g) in sproduct g by A1, Th66; ::_thesis: h = (h | ((dom f) \ (dom g))) +* (h | (dom g))
 dom h c= dom (f +* g) by A1, Th49;
then  dom h c= (dom f) \/ (dom g) by FUNCT_4:def_1;
then  dom h c= ((dom f) \ (dom g)) \/ (dom g) by XBOOLE_1:39;
hence  h = (h | ((dom f) \ (dom g))) +* (h | (dom g)) by FUNCT_4:70; ::_thesis: verum
end;

theorem Th68: :: CARD_3:68
for g, f, f9, g9 being Function st dom g misses (dom f9) \ (dom g9) & f9 in sproduct f & g9 in sproduct g holds
f9 +* g9 in sproduct (f +* g)
proof
let g, f be Function; ::_thesis: for f9, g9 being Function st dom g misses (dom f9) \ (dom g9) & f9 in sproduct f & g9 in sproduct g holds
f9 +* g9 in sproduct (f +* g)
let f9, g9 be Function; ::_thesis: ( dom g misses (dom f9) \ (dom g9) & f9 in sproduct f & g9 in sproduct g implies f9 +* g9 in sproduct (f +* g) )
assume that
A1: dom g misses (dom f9) \ (dom g9) and
A2: f9 in sproduct f and
A3: g9 in sproduct g ; ::_thesis: f9 +* g9 in sproduct (f +* g)
set h = f9 +* g9;
A4: dom f9 c= dom f by A2, Th49;
A5: dom g9 c= dom g by A3, Th49;
then A6: (dom f9) \/ (dom g9) c= (dom f) \/ (dom g) by A4, XBOOLE_1:13;
A7: dom (f9 +* g9) = (dom f9) \/ (dom g9) by FUNCT_4:def_1;
then A8: dom (f9 +* g9) c= dom (f +* g) by A6, FUNCT_4:def_1;
 for x being set st x in dom (f9 +* g9) holds
(f9 +* g9) . x in (f +* g) . x
proof
let x be set ; ::_thesis: ( x in dom (f9 +* g9) implies (f9 +* g9) . x in (f +* g) . x )
assume A9: x in dom (f9 +* g9) ; ::_thesis: (f9 +* g9) . x in (f +* g) . x
then  x in dom (f +* g) by A8;
then A10: x in (dom f) \/ (dom g) by FUNCT_4:def_1;
 x in ((dom f9) \ (dom g9)) \/ (dom g9) by A7, A9, XBOOLE_1:39;
then A11: ( x in (dom f9) \ (dom g9) or x in dom g9 ) by XBOOLE_0:def_3;
now__::_thesis:_(_(_x_in_dom_g_&_(f9_+*_g9)_._x_in_g_._x_)_or_(_not_x_in_dom_g_&_(f9_+*_g9)_._x_in_f_._x_)_)
percases ( x in dom g or not x in dom g ) ;
caseA12: x in dom g ; ::_thesis: (f9 +* g9) . x in g . x
then  (f9 +* g9) . x = g9 . x by A1, A7, A9, A11, FUNCT_4:def_1, XBOOLE_0:3;
hence  (f9 +* g9) . x in g . x by A1, A3, A11, A12, Th49, XBOOLE_0:3; ::_thesis: verum
end;
case not x in dom g ; ::_thesis: (f9 +* g9) . x in f . x
then A13: not x in dom g9 by A5;
then A14: (f9 +* g9) . x = f9 . x by A7, A9, FUNCT_4:def_1;
 x in dom f9 by A7, A9, A13, XBOOLE_0:def_3;
hence  (f9 +* g9) . x in f . x by A2, A14, Th49; ::_thesis: verum
end;
end;
end;
hence  (f9 +* g9) . x in (f +* g) . x by A10, FUNCT_4:def_1; ::_thesis: verum
end;
hence  f9 +* g9 in sproduct (f +* g) by A8, Def9; ::_thesis: verum
end;

theorem :: CARD_3:69
for g, f, f9, g9 being Function st dom f9 misses (dom g) \ (dom g9) & f9 in sproduct f & g9 in sproduct g holds
f9 +* g9 in sproduct (f +* g)
proof
let g, f be Function; ::_thesis: for f9, g9 being Function st dom f9 misses (dom g) \ (dom g9) & f9 in sproduct f & g9 in sproduct g holds
f9 +* g9 in sproduct (f +* g)
let f9, g9 be Function; ::_thesis: ( dom f9 misses (dom g) \ (dom g9) & f9 in sproduct f & g9 in sproduct g implies f9 +* g9 in sproduct (f +* g) )
assume  dom f9 misses (dom g) \ (dom g9) ; ::_thesis: ( not f9 in sproduct f or not g9 in sproduct g or f9 +* g9 in sproduct (f +* g) )
then  dom g misses (dom f9) \ (dom g9) by XBOOLE_1:81;
hence  ( not f9 in sproduct f or not g9 in sproduct g or f9 +* g9 in sproduct (f +* g) ) by Th68; ::_thesis: verum
end;

theorem Th70: :: CARD_3:70
for g, f, h being Function st g in sproduct f & h in sproduct f holds
g +* h in sproduct f
proof
let g, f, h be Function; ::_thesis: ( g in sproduct f & h in sproduct f implies g +* h in sproduct f )
assume that
A1: g in sproduct f and
A2: h in sproduct f ; ::_thesis: g +* h in sproduct f
A3: dom g c= dom f by A1, Th49;
 dom h c= dom f by A2, Th49;
then  (dom g) \/ (dom h) c= dom f by A3, XBOOLE_1:8;
then A4: dom (g +* h) c= dom f by FUNCT_4:def_1;
now__::_thesis:_for_x_being_set_st_x_in_dom_(g_+*_h)_holds_
(g_+*_h)_._x_in_f_._x
let x be set ; ::_thesis: ( x in dom (g +* h) implies (g +* h) . x in f . x )
assume  x in dom (g +* h) ; ::_thesis: (g +* h) . x in f . x
then  x in (dom g) \/ (dom h) by FUNCT_4:def_1;
then A5: x in ((dom g) \ (dom h)) \/ (dom h) by XBOOLE_1:39;
now__::_thesis:_(g_+*_h)_._x_in_f_._x
percases ( x in dom h or x in (dom g) \ (dom h) ) by A5, XBOOLE_0:def_3;
supposeA6: x in dom h ; ::_thesis: (g +* h) . x in f . x
then  h . x in f . x by A2, Th49;
hence  (g +* h) . x in f . x by A6, FUNCT_4:13; ::_thesis: verum
end;
supposeA7: x in (dom g) \ (dom h) ; ::_thesis: (g +* h) . x in f . x
then A8: g . x in f . x by A1, Th49;
 not x in dom h by A7, XBOOLE_0:def_5;
hence  (g +* h) . x in f . x by A8, FUNCT_4:11; ::_thesis: verum
end;
end;
end;
hence  (g +* h) . x in f . x ; ::_thesis: verum
end;
hence  g +* h in sproduct f by A4, Def9; ::_thesis: verum
end;

theorem :: CARD_3:71
for f being Function
for x1, x2, y1, y2 being set st x1 in dom f & y1 in f . x1 & x2 in dom f & y2 in f . x2 holds
(x1,x2) --> (y1,y2) in sproduct f
proof
let f be Function; ::_thesis: for x1, x2, y1, y2 being set st x1 in dom f & y1 in f . x1 & x2 in dom f & y2 in f . x2 holds
(x1,x2) --> (y1,y2) in sproduct f
let x1, x2, y1, y2 be set ; ::_thesis: ( x1 in dom f & y1 in f . x1 & x2 in dom f & y2 in f . x2 implies (x1,x2) --> (y1,y2) in sproduct f )
assume that
A1: x1 in dom f and
A2: y1 in f . x1 ; ::_thesis: ( not x2 in dom f or not y2 in f . x2 or (x1,x2) --> (y1,y2) in sproduct f )
A3: x1 .--> y1 in sproduct f by A1, A2, Th60;
assume that
A4: x2 in dom f and
A5: y2 in f . x2 ; ::_thesis: (x1,x2) --> (y1,y2) in sproduct f
A6: x2 .--> y2 in sproduct f by A4, A5, Th60;
 (x1,x2) --> (y1,y2) = (x1 .--> y1) +* (x2 .--> y2) by FUNCT_4:def_4;
hence  (x1,x2) --> (y1,y2) in sproduct f by A3, A6, Th70; ::_thesis: verum
end;

begin

definition
let IT be set ;
attrIT is with_common_domain  means :Def10: :: CARD_3:def 10
 for f, g being Function st f in IT & g in IT holds
dom f = dom g;
end;

:: deftheorem Def10 defines with_common_domain CARD_3:def_10_:_
 for IT being set holds
( IT is with_common_domain iff for f, g being Function st f in IT & g in IT holds
dom f = dom g );

registration
cluster non empty functional with_common_domain for set ;
existence
 ex b1 being set st
( b1 is with_common_domain & b1 is functional & not b1 is empty )
proof
set h = the Function;
take A = { the Function}; ::_thesis: ( A is with_common_domain & A is functional & not A is empty )
 for f, g being Function st f in A & g in A holds
dom f = dom g
proof
let f, g be Function; ::_thesis: ( f in A & g in A implies dom f = dom g )
assume that
A1: f in A and
A2: g in A ; ::_thesis: dom f = dom g
 f = the Function by A1, TARSKI:def_1;
hence  dom f = dom g by A2, TARSKI:def_1; ::_thesis: verum
end;
hence  A is with_common_domain by Def10; ::_thesis: ( A is functional & not A is empty )
thus  A is functional ; ::_thesis: not A is empty
thus  not A is empty ; ::_thesis: verum
end;
end;

registration
let f be Function;
cluster{f} ->  with_common_domain ;
coherence
 {f} is with_common_domain
proof
let g, h be Function; :: according to CARD_3:def_10 ::_thesis: ( g in {f} & h in {f} implies dom g = dom h )
assume  g in {f} ; ::_thesis: ( not h in {f} or dom g = dom h )
then  g = f by TARSKI:def_1;
hence  ( not h in {f} or dom g = dom h ) by TARSKI:def_1; ::_thesis: verum
end;
end;

definition
let X be functional set ;
func DOM X ->  set  equals :: CARD_3:def 11
 meet  {  (dom f) where f is Element of X : verum  }  ;
coherence
 meet  {  (dom f) where f is Element of X : verum  }  is set ;
end;

:: deftheorem  defines DOM CARD_3:def_11_:_
 for X being functional set holds DOM X = meet  {  (dom f) where f is Element of X : verum  }  ;

LmX:  for X being functional with_common_domain set
for f being Function st f in X holds
dom f = DOM X
proof
let X be functional with_common_domain set ; ::_thesis: for f being Function st f in X holds
dom f = DOM X
set A =  {  (dom f) where f is Element of X : verum  }  ;
let f be Function; ::_thesis: ( f in X implies dom f = DOM X )
assume Z: f in X ; ::_thesis: dom f = DOM X
then  dom f in  {  (dom f) where f is Element of X : verum  }  ;
then X: {(dom f)} c=  {  (dom f) where f is Element of X : verum  }  by ZFMISC_1:31;
  {  (dom f) where f is Element of X : verum  }  c= {(dom f)}
proof
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in  {  (dom f) where f is Element of X : verum  }  or e in {(dom f)} )
assume  e in  {  (dom f) where f is Element of X : verum  }  ; ::_thesis: e in {(dom f)}
then consider g being Element of X such that
W: e = dom g ;
 e = dom f by W, Def10, Z;
hence  e in {(dom f)} by TARSKI:def_1; ::_thesis: verum
end;
then   {  (dom f) where f is Element of X : verum  }  = {(dom f)} by X, XBOOLE_0:def_10;
hence  dom f = DOM X by SETFAM_1:10; ::_thesis: verum
end;

theorem Th72: :: CARD_3:72
for X being functional with_common_domain set st X = {{}} holds
DOM X = {}
proof
let X be functional with_common_domain set ; ::_thesis: ( X = {{}} implies DOM X = {} )
assume A1: X = {{}} ; ::_thesis: DOM X = {}
 {} in {{}} by TARSKI:def_1;
hence  DOM X = {} by A1, LmX, RELAT_1:38; ::_thesis: verum
end;

registration
let X be empty set ;
cluster DOM X ->  empty ;
coherence
 DOM X is empty
proof
set A =  {  (dom f) where f is Element of X : verum  }  ;
X:  {  (dom f) where f is Element of X : verum  }  c= {{}}
proof
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in  {  (dom f) where f is Element of X : verum  }  or e in {{}} )
assume  e in  {  (dom f) where f is Element of X : verum  }  ; ::_thesis: e in {{}}
then  ex f being Element of X st e = dom f ;
then  e = dom {} by SUBSET_1:def_1;
hence  e in {{}} by TARSKI:def_1; ::_thesis: verum
end;
 {{}} c=  {  (dom f) where f is Element of X : verum  }
proof
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in {{}} or e in  {  (dom f) where f is Element of X : verum  }  )
assume  e in {{}} ; ::_thesis: e in  {  (dom f) where f is Element of X : verum  }
then  e = {} by TARSKI:def_1;
then  e = dom {} ;
then  e = dom the Element of X by SUBSET_1:def_1;
hence  e in  {  (dom f) where f is Element of X : verum  }  ; ::_thesis: verum
end;
then   {  (dom f) where f is Element of X : verum  }  = {{}} by X, XBOOLE_0:def_10;
hence  DOM X is empty by SETFAM_1:10; ::_thesis: verum
end;
end;

begin

definition
let S be functional set ;
func product" S ->  Function means :Def12: :: CARD_3:def 12
( dom it = DOM S & ( for i being set st i in dom it holds
it . i = pi (S,i) ) );
existence
 ex b1 being Function st
( dom b1 = DOM S & ( for i being set st i in dom b1 holds
b1 . i = pi (S,i) ) )
proof
percases ( S = {} or S <> {} ) ;
supposeS: S = {} ; ::_thesis: ex b1 being Function st
( dom b1 = DOM S & ( for i being set st i in dom b1 holds
b1 . i = pi (S,i) ) )
take  {} ; ::_thesis: ( dom {} = DOM S & ( for i being set st i in dom {} holds
{} . i = pi (S,i) ) )
thus  ( dom {} = DOM S & ( for i being set st i in dom {} holds
{} . i = pi (S,i) ) ) by S; ::_thesis: verum
end;
suppose S <> {} ; ::_thesis: ex b1 being Function st
( dom b1 = DOM S & ( for i being set st i in dom b1 holds
b1 . i = pi (S,i) ) )
then reconsider S1 = S as non empty functional set ;
set D =  {  (dom f) where f is Element of S1 : verum  }  ;
defpred S2[ set , set ] means $2 = pi (S,$1);
A1: for e being set st e in meet  {  (dom f) where f is Element of S1 : verum  }  holds
ex u being set st S2[e,u] ;
consider g being Function such that
A2: dom g = meet  {  (dom f) where f is Element of S1 : verum  }  and
A3: for e being set st e in meet  {  (dom f) where f is Element of S1 : verum  }  holds
S2[e,g . e] from CLASSES1:sch_1(A1);
take  g ; ::_thesis: ( dom g = DOM S & ( for i being set st i in dom g holds
g . i = pi (S,i) ) )
thus  ( dom g = DOM S & ( for i being set st i in dom g holds
g . i = pi (S,i) ) ) by A2, A3; ::_thesis: verum
end;
end;
end;
uniqueness
 for b1, b2 being Function st dom b1 = DOM S & ( for i being set st i in dom b1 holds
b1 . i = pi (S,i) ) & dom b2 = DOM S & ( for i being set st i in dom b2 holds
b2 . i = pi (S,i) ) holds
b1 = b2
proof
let f, g be Function; ::_thesis: ( dom f = DOM S & ( for i being set st i in dom f holds
f . i = pi (S,i) ) & dom g = DOM S & ( for i being set st i in dom g holds
g . i = pi (S,i) ) implies f = g )
assume that
Z1: dom f = DOM S and
Z2: for i being set st i in dom f holds
f . i = pi (S,i) and
Z3: dom g = DOM S and
Z4: for i being set st i in dom g holds
g . i = pi (S,i) ; ::_thesis: f = g
 for x being set st x in dom f holds
f . x = g . x
proof
let x be set ; ::_thesis: ( x in dom f implies f . x = g . x )
assume Z: x in dom f ; ::_thesis: f . x = g . x
hence f . x = pi (S,x) by Z2
.= g . x by Z1, Z3, Z, Z4 ;
::_thesis: verum
end;
hence  f = g by Z1, Z3, FUNCT_1:def_11; ::_thesis: verum
end;
end;

:: deftheorem Def12 defines product" CARD_3:def_12_:_
 for S being functional set
for b2 being Function holds
( b2 = product" S iff ( dom b2 = DOM S & ( for i being set st i in dom b2 holds
b2 . i = pi (S,i) ) ) );

theorem :: CARD_3:73
canceled;

theorem Th74: :: CARD_3:74
for S being non empty functional set
for i being set st i in dom (product" S) holds
(product" S) . i =  {  (f . i) where f is Element of S : verum  }
proof
let S be non empty functional set ; ::_thesis: for i being set st i in dom (product" S) holds
(product" S) . i =  {  (f . i) where f is Element of S : verum  }
let i be set ; ::_thesis: ( i in dom (product" S) implies (product" S) . i =  {  (f . i) where f is Element of S : verum  }  )
assume A1: i in dom (product" S) ; ::_thesis: (product" S) . i =  {  (f . i) where f is Element of S : verum  }
hereby  :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis:  {  (f . i) where f is Element of S : verum  }  c= (product" S) . i
let x be set ; ::_thesis: ( x in (product" S) . i implies x in  {  (f . i) where f is Element of S : verum  }  )
assume  x in (product" S) . i ; ::_thesis: x in  {  (f . i) where f is Element of S : verum  }
then  x in pi (S,i) by A1, Def12;
then  ex f being Function st
( f in S & x = f . i ) by Def6;
hence  x in  {  (f . i) where f is Element of S : verum  }  ; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in  {  (f . i) where f is Element of S : verum  }  or x in (product" S) . i )
assume  x in  {  (f . i) where f is Element of S : verum  }  ; ::_thesis: x in (product" S) . i
then  ex f being Element of S st x = f . i ;
then  x in pi (S,i) by Def6;
hence  x in (product" S) . i by A1, Def12; ::_thesis: verum
end;

definition
let S be set ;
attrS is product-like  means :Def13: :: CARD_3:def 13
 ex f being Function st S = product f;
end;

:: deftheorem Def13 defines product-like CARD_3:def_13_:_
 for S being set holds
( S is product-like iff ex f being Function st S = product f );

registration
let f be Function;
cluster product f ->  product-like ;
coherence
 product f is product-like by Def13;
end;

registration
cluster product-like  ->  functional with_common_domain for set ;
coherence
 for b1 being set st b1 is product-like holds
( b1 is functional & b1 is with_common_domain )
proof
let S be set ; ::_thesis: ( S is product-like implies ( S is functional & S is with_common_domain ) )
given f being Function such that A1: S = product f ; :: according to CARD_3:def_13 ::_thesis: ( S is functional & S is with_common_domain )
thus  S is functional by A1; ::_thesis: S is with_common_domain
let h, g be Function; :: according to CARD_3:def_10 ::_thesis: ( h in S & g in S implies dom h = dom g )
assume that
A2: h in S and
A3: g in S ; ::_thesis: dom h = dom g
thus  dom h = dom f by A1, A2, Th9
.= dom g by A1, A3, Th9 ; ::_thesis: verum
end;
end;

registration
cluster non empty product-like for set ;
existence
 ex b1 being set st
( b1 is product-like & not b1 is empty )
proof
set B = the with_non-empty_elements set ;
set f = the Function of 0, the with_non-empty_elements set ;
take  product the Function of 0, the with_non-empty_elements set ; ::_thesis: ( product the Function of 0, the with_non-empty_elements set is product-like & not product the Function of 0, the with_non-empty_elements set is empty )
thus  ( product the Function of 0, the with_non-empty_elements set is product-like & not product the Function of 0, the with_non-empty_elements set is empty ) ; ::_thesis: verum
end;
end;

theorem :: CARD_3:75
canceled;

theorem :: CARD_3:76
canceled;

theorem Th77: :: CARD_3:77
for S being functional with_common_domain set holds S c= product (product" S)
proof
let S be functional with_common_domain set ; ::_thesis: S c= product (product" S)
let f be set ; :: according to TARSKI:def_3 ::_thesis: ( not f in S or f in product (product" S) )
assume A1: f in S ; ::_thesis: f in product (product" S)
then reconsider f = f as Element of S ;
A2: dom f = DOM S by A1, LmX
.= dom (product" S) by Def12 ;
 for i being set st i in dom (product" S) holds
f . i in (product" S) . i
proof
let i be set ; ::_thesis: ( i in dom (product" S) implies f . i in (product" S) . i )
assume  i in dom (product" S) ; ::_thesis: f . i in (product" S) . i
then  (product" S) . i = pi (S,i) by Def12;
hence  f . i in (product" S) . i by A1, Def6; ::_thesis: verum
end;
hence  f in product (product" S) by A2, Th9; ::_thesis: verum
end;

theorem :: CARD_3:78
for S being non empty product-like set holds S = product (product" S)
proof
let S be non empty product-like set ; ::_thesis: S = product (product" S)
thus  S c= product (product" S) by Th77; :: according to XBOOLE_0:def_10 ::_thesis: product (product" S) c= S
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in product (product" S) or x in S )
assume  x in product (product" S) ; ::_thesis: x in S
then consider g being Function such that
A1: x = g and
A2: dom g = dom (product" S) and
A3: for z being set st z in dom (product" S) holds
g . z in (product" S) . z by Def5;
consider p being Function such that
A4: S = product p by Def13;
set s = the Element of S;
A5: dom g = DOM S by A2, Def12
.= dom the Element of S by LmX
.= dom p by A4, Th9 ;
 for z being set st z in dom p holds
g . z in p . z
proof
let z be set ; ::_thesis: ( z in dom p implies g . z in p . z )
assume A6: z in dom p ; ::_thesis: g . z in p . z
then  g . z in (product" S) . z by A2, A3, A5;
then  g . z in pi (S,z) by A2, A5, A6, Def12;
then  ex f being Function st
( f in S & g . z = f . z ) by Def6;
hence  g . z in p . z by A4, A6, Th9; ::_thesis: verum
end;
hence  x in S by A1, A4, A5, Th9; ::_thesis: verum
end;

theorem :: CARD_3:79
for f being Function
for s, t being Element of product f
for A being set holds s +* (t | A) is Element of product f
proof
let f be Function; ::_thesis: for s, t being Element of product f
for A being set holds s +* (t | A) is Element of product f
let s, t be Element of product f; ::_thesis: for A being set holds s +* (t | A) is Element of product f
let A be set ; ::_thesis: s +* (t | A) is Element of product f
percases ( f is non-empty or not f is non-empty ) ;
suppose f is non-empty ; ::_thesis: s +* (t | A) is Element of product f
then  product f <> {} ;
then A1: t in product f ;
 product f c= sproduct f by Th51;
hence  s +* (t | A) is Element of product f by A1, Th53, Th65; ::_thesis: verum
end;
suppose not f is non-empty ; ::_thesis: s +* (t | A) is Element of product f
then  {} in rng f by RELAT_1:def_9;
then A2: product f = {} by Th26;
then A3: s = {} by SUBSET_1:def_1;
 t = {} by A2, SUBSET_1:def_1;
then  t | A = {} ;
hence  s +* (t | A) is Element of product f by A3; ::_thesis: verum
end;
end;
end;

theorem :: CARD_3:80
for f being non-empty Function
for p being Element of sproduct f ex s being Element of product f st p c= s
proof
let f be non-empty Function; ::_thesis: for p being Element of sproduct f ex s being Element of product f st p c= s
let p be Element of sproduct f; ::_thesis: ex s being Element of product f st p c= s
set h = the Element of product f;
reconsider s = the Element of product f +* p as Element of product f by Th53;
take  s ; ::_thesis: p c= s
thus  p c= s by FUNCT_4:25; ::_thesis: verum
end;

theorem Th81: :: CARD_3:81
for g, f being Function
for A being set st g in product f holds
g | A in sproduct f
proof
let g, f be Function; ::_thesis: for A being set st g in product f holds
g | A in sproduct f
let A be set ; ::_thesis: ( g in product f implies g | A in sproduct f )
A1: product f c= sproduct f by Th51;
assume  g in product f ; ::_thesis: g | A in sproduct f
hence  g | A in sproduct f by A1, Th64, RELAT_1:59; ::_thesis: verum
end;

definition
let f be non-empty Function;
let g be Element of product f;
let X be set ;
:: original: |
redefine funcg | X ->  Element of sproduct f;
coherence
 g | X is Element of sproduct f by Th81;
end;

theorem :: CARD_3:82
for f being non-empty Function
for s, ss being Element of product f
for A being set holds (ss +* (s | A)) | A = s | A
proof
let f be non-empty Function; ::_thesis: for s, ss being Element of product f
for A being set holds (ss +* (s | A)) | A = s | A
let s, ss be Element of product f; ::_thesis: for A being set holds (ss +* (s | A)) | A = s | A
let A be set ; ::_thesis: (ss +* (s | A)) | A = s | A
dom s = dom f by Th9
.= dom ss by Th9 ;
then  A /\ (dom ss) c= A /\ (dom s) ;
hence  (ss +* (s | A)) | A = s | A by FUNCT_4:88; ::_thesis: verum
end;

theorem :: CARD_3:83
for M, x, g being Function st x in product M holds
x * g in product (M * g)
proof
let M, x, g be Function; ::_thesis: ( x in product M implies x * g in product (M * g) )
assume A1: x in product M ; ::_thesis: x * g in product (M * g)
set xg = x * g;
set Mg = M * g;
A2: ex gg being Function st
( x = gg & dom gg = dom M & ( for x being set st x in dom M holds
gg . x in M . x ) ) by A1, Def5;
then A3: dom (x * g) = dom (M * g) by RELAT_1:163;
now__::_thesis:_for_y_being_set_st_y_in_dom_(M_*_g)_holds_
(x_*_g)_._y_in_(M_*_g)_._y
let y be set ; ::_thesis: ( y in dom (M * g) implies (x * g) . y in (M * g) . y )
assume A4: y in dom (M * g) ; ::_thesis: (x * g) . y in (M * g) . y
then A5: y in dom g by FUNCT_1:11;
A6: g . y in dom M by A4, FUNCT_1:11;
A7: (x * g) . y = x . (g . y) by A5, FUNCT_1:13;
 (M * g) . y = M . (g . y) by A5, FUNCT_1:13;
hence  (x * g) . y in (M * g) . y by A2, A6, A7; ::_thesis: verum
end;
hence  x * g in product (M * g) by A3, Def5; ::_thesis: verum
end;

theorem :: CARD_3:84
for X being set holds
( X is finite iff card X in omega ) by Th42, CARD_1:47;


theorem Th85: :: CARD_3:85
for A being Ordinal holds
( A is infinite iff omega c= A )
proof
let A be Ordinal; ::_thesis: ( A is infinite iff omega c= A )
 ( omega c= A iff not A in omega ) by ORDINAL1:16;
hence  ( A is infinite iff omega c= A ) ; ::_thesis: verum
end;

theorem :: CARD_3:86
for N, M being Cardinal st N is finite & not M is finite holds
( N in M & N c= M )
proof
let N, M be Cardinal; ::_thesis: ( N is finite & not M is finite implies ( N in M & N c= M ) )
assume that
A1: N is finite and
A2: not M is finite ; ::_thesis: ( N in M & N c= M )
A3: N in omega by A1, CARD_1:61;
 omega c= M by A2, Th85;
hence  N in M by A3; ::_thesis: N c= M
thus  N c= M by A1, A2; ::_thesis: verum
end;

theorem :: CARD_3:87
for X being set holds
( not X is finite iff ex Y being set st
( Y c= X & card Y = omega ) )
proof
let X be set ; ::_thesis: ( not X is finite iff ex Y being set st
( Y c= X & card Y = omega ) )
thus  ( not X is finite implies ex Y being set st
( Y c= X & card Y = omega ) ) ::_thesis: ( ex Y being set st
( Y c= X & card Y = omega ) implies not X is finite )
proof
assume  not X is finite ; ::_thesis: ex Y being set st
( Y c= X & card Y = omega )
then  not card X in omega ;
then A1: omega c= card X by CARD_1:4;
 card X,X are_equipotent by CARD_1:def_2;
then consider f being Function such that
A2: f is one-to-one and
A3: dom f = card X and
A4: rng f = X by WELLORD2:def_4;
take Y = f .: omega; ::_thesis: ( Y c= X & card Y = omega )
thus  Y c= X by A4, RELAT_1:111; ::_thesis: card Y = omega
 omega ,Y are_equipotent
proof
take  f | omega ; :: according to WELLORD2:def_4 ::_thesis: ( f | omega is one-to-one & proj1 (f | omega) = omega & proj2 (f | omega) = Y )
thus  ( f | omega is one-to-one & proj1 (f | omega) = omega & proj2 (f | omega) = Y ) by A1, A2, A3, FUNCT_1:52, RELAT_1:62, RELAT_1:115; ::_thesis: verum
end;
hence  card Y = omega by CARD_1:def_2; ::_thesis: verum
end;
given Y being set  such that A5: Y c= X and
A6: card Y = omega ; ::_thesis: not X is finite
thus  not X is finite by A5, A6; ::_thesis: verum
end;

theorem Th88: :: CARD_3:88
for X, Y being set holds
( card X = card Y iff nextcard X = nextcard Y )
proof
let X, Y be set ; ::_thesis: ( card X = card Y iff nextcard X = nextcard Y )
thus  ( card X = card Y implies nextcard X = nextcard Y ) by CARD_1:16; ::_thesis: ( nextcard X = nextcard Y implies card X = card Y )
assume that
A1: nextcard X = nextcard Y and
A2: card X <> card Y ; ::_thesis: contradiction
 ( card X in card Y or card Y in card X ) by A2, ORDINAL1:14;
then  ( ( nextcard X c= card Y & card Y in nextcard Y ) or ( nextcard Y c= card X & card X in nextcard X ) ) by CARD_1:def_3;
hence  contradiction by A1, ORDINAL1:12; ::_thesis: verum
end;

theorem :: CARD_3:89
for N, M being Cardinal st nextcard N = nextcard M holds
M = N
proof
let N, M be Cardinal; ::_thesis: ( nextcard N = nextcard M implies M = N )
A1: card N = N by CARD_1:def_2;
 card M = M by CARD_1:def_2;
hence  ( nextcard N = nextcard M implies M = N ) by A1, Th88; ::_thesis: verum
end;

theorem Th90: :: CARD_3:90
for N, M being Cardinal holds
( N in M iff nextcard N c= M )
proof
let N, M be Cardinal; ::_thesis: ( N in M iff nextcard N c= M )
A1: N in nextcard N by CARD_1:18;
 card N = N by CARD_1:def_2;
hence  ( N in M iff nextcard N c= M ) by A1, CARD_1:def_3; ::_thesis: verum
end;

theorem :: CARD_3:91
for N, M being Cardinal holds
( N in nextcard M iff N c= M )
proof
let N, M be Cardinal; ::_thesis: ( N in nextcard M iff N c= M )
A1: ( not N c= M iff M in N ) by CARD_1:4;
 ( N in nextcard M iff not nextcard M c= N ) by CARD_1:4;
hence  ( N in nextcard M iff N c= M ) by A1, Th90; ::_thesis: verum
end;

theorem :: CARD_3:92
for M, N being Cardinal st M is finite & ( N c= M or N in M ) holds
N is finite
proof
let M, N be Cardinal; ::_thesis: ( M is finite & ( N c= M or N in M ) implies N is finite )
assume that
A1: M is finite and
A2: ( N c= M or N in M ) ; ::_thesis: N is finite
 N c= M by A2, CARD_1:3;
hence  N is finite by A1; ::_thesis: verum
end;


definition
let X be set ;
attrX is countable  means :Def14: :: CARD_3:def 14
 card X c= omega ;
attrX is denumerable  means :: CARD_3:def 15
 card X = omega ;
end;

:: deftheorem Def14 defines countable CARD_3:def_14_:_
 for X being set holds
( X is countable iff card X c= omega );

:: deftheorem  defines denumerable CARD_3:def_15_:_
 for X being set holds
( X is denumerable iff card X = omega );

registration
cluster denumerable  ->  infinite countable for set ;
coherence
 for b1 being set st b1 is denumerable holds
( b1 is countable & b1 is infinite )
proof
let X be set ; ::_thesis: ( X is denumerable implies ( X is countable & X is infinite ) )
assume A1: card X = omega ; :: according to CARD_3:def_15 ::_thesis: ( X is countable & X is infinite )
hence  card X c= omega ; :: according to CARD_3:def_14 ::_thesis: X is infinite
thus  X is infinite by A1; ::_thesis: verum
end;
cluster infinite countable  ->  denumerable for set ;
coherence
 for b1 being set st b1 is countable & b1 is infinite holds
b1 is denumerable
proof
let X be set ; ::_thesis: ( X is countable & X is infinite implies X is denumerable )
assume A2: card X c= omega ; :: according to CARD_3:def_14 ::_thesis: ( not X is infinite or X is denumerable )
assume  X is infinite ; ::_thesis: X is denumerable
then  omega c= card X by Th85;
hence  card X = omega by A2, XBOOLE_0:def_10; :: according to CARD_3:def_15 ::_thesis: verum
end;
end;

registration
cluster finite  ->  countable for set ;
coherence
 for b1 being set st b1 is finite holds
b1 is countable
proof
let X be set ; ::_thesis: ( X is finite implies X is countable )
assume  X is finite ; ::_thesis: X is countable
then consider n being Nat such that
A1: X,n are_equipotent by CARD_1:43;
 card n = card X by A1, CARD_1:5;
hence  card X c= omega ; :: according to CARD_3:def_14 ::_thesis: verum
end;
end;

registration
cluster omega  ->  denumerable ;
coherence
 omega is denumerable
proof
thus  card omega = omega by CARD_1:47; :: according to CARD_3:def_15 ::_thesis: verum
end;
end;

registration
cluster denumerable for set ;
existence
 ex b1 being set st b1 is denumerable
proof
take  omega ; ::_thesis: omega is denumerable
thus  omega is denumerable ; ::_thesis: verum
end;
end;

theorem Th93: :: CARD_3:93
for X being set holds
( X is countable iff ex f being Function st
( dom f = omega & X c= rng f ) )
proof
let X be set ; ::_thesis: ( X is countable iff ex f being Function st
( dom f = omega & X c= rng f ) )
thus  ( X is countable implies ex f being Function st
( dom f = omega & X c= rng f ) ) ::_thesis: ( ex f being Function st
( dom f = omega & X c= rng f ) implies X is countable )
proof
assume  card X c= omega ; :: according to CARD_3:def_14 ::_thesis: ex f being Function st
( dom f = omega & X c= rng f )
hence  ex f being Function st
( dom f = omega & X c= rng f ) by CARD_1:12, CARD_1:47; ::_thesis: verum
end;
assume  ex f being Function st
( dom f = omega & X c= rng f ) ; ::_thesis: X is countable
hence  card X c= omega by CARD_1:12, CARD_1:47; :: according to CARD_3:def_14 ::_thesis: verum
end;

registration
let X be countable set ;
cluster  ->  countable for Element of bool X;
coherence
 for b1 being Subset of X holds b1 is countable
proof
let Y be Subset of X; ::_thesis: Y is countable
A1: card Y c= card X by CARD_1:11;
 card X c= omega by Def14;
hence  card Y c= omega by A1, XBOOLE_1:1; :: according to CARD_3:def_14 ::_thesis: verum
end;
end;

Lm2:  for Y, X being set st Y c= X & X is countable holds
Y is countable
;

theorem :: CARD_3:94
for X, Y being set st X is countable holds
X /\ Y is countable by Lm2, XBOOLE_1:17;

theorem :: CARD_3:95
for X, Y being set st X is countable holds
X \ Y is countable ;

theorem :: CARD_3:96
for A being non empty countable set ex f being Function of omega,A st rng f = A
proof
let A be non empty countable set ; ::_thesis: ex f being Function of omega,A st rng f = A
consider f being Function such that
A1: dom f = omega and
A2: A c= rng f by Th93;
consider x being set  such that
A3: x in A by XBOOLE_0:def_1;
set F = (f | (f " A)) +* ((omega \ (f " A)) --> x);
A4: ( rng ((f | (f " A)) +* ((omega \ (f " A)) --> x)) = A & dom ((f | (f " A)) +* ((omega \ (f " A)) --> x)) = omega )
proof
A5: f " A c= omega by A1, RELAT_1:132;
A6: dom (f | (f " A)) = omega /\ (f " A) by A1, RELAT_1:61;
percases ( omega = f " A or omega <> f " A ) ;
supposeA7: omega = f " A ; ::_thesis: ( rng ((f | (f " A)) +* ((omega \ (f " A)) --> x)) = A & dom ((f | (f " A)) +* ((omega \ (f " A)) --> x)) = omega )
then A8: omega \ (f " A) = {} by XBOOLE_1:37;
then  (dom (f | (f " A))) /\ (dom ((omega \ (f " A)) --> x)) = {} ;
then  dom (f | (f " A)) misses dom ((omega \ (f " A)) --> x) by XBOOLE_0:def_7;
then  (f | (f " A)) +* ((omega \ (f " A)) --> x) = (f | (f " A)) \/ ((omega \ (f " A)) --> x) by FUNCT_4:31;
hence  rng ((f | (f " A)) +* ((omega \ (f " A)) --> x)) = (rng (f | (f " A))) \/ (rng ((omega \ (f " A)) --> x)) by RELAT_1:12
.= (rng (f | (f " A))) \/ {} by A8
.= f .: (f " A) by RELAT_1:115
.= A by A2, FUNCT_1:77 ;
::_thesis: dom ((f | (f " A)) +* ((omega \ (f " A)) --> x)) = omega
thus  dom ((f | (f " A)) +* ((omega \ (f " A)) --> x)) = (dom (f | (f " A))) \/ (dom ((omega \ (f " A)) --> x)) by FUNCT_4:def_1
.= (dom (f | (f " A))) \/ {} by A8
.= omega by A6, A7 ; ::_thesis: verum
end;
supposeA9: omega <> f " A ; ::_thesis: ( rng ((f | (f " A)) +* ((omega \ (f " A)) --> x)) = A & dom ((f | (f " A)) +* ((omega \ (f " A)) --> x)) = omega )
A10: now__::_thesis:_not_omega_\_(f_"_A)_is_empty
assume  omega \ (f " A) is empty ; ::_thesis: contradiction
then  omega c= f " A by XBOOLE_1:37;
hence  contradiction by A5, A9, XBOOLE_0:def_10; ::_thesis: verum
end;
 dom ((omega \ (f " A)) --> x) = omega \ (f " A) by FUNCOP_1:13;
then  (f | (f " A)) +* ((omega \ (f " A)) --> x) = (f | (f " A)) \/ ((omega \ (f " A)) --> x) by A6, FUNCT_4:31, XBOOLE_1:89;
hence  rng ((f | (f " A)) +* ((omega \ (f " A)) --> x)) = (rng (f | (f " A))) \/ (rng ((omega \ (f " A)) --> x)) by RELAT_1:12
.= (rng (f | (f " A))) \/ {x} by A10, FUNCOP_1:8
.= (f .: (f " A)) \/ {x} by RELAT_1:115
.= A \/ {x} by A2, FUNCT_1:77
.= A by A3, ZFMISC_1:40 ;
::_thesis: dom ((f | (f " A)) +* ((omega \ (f " A)) --> x)) = omega
thus  dom ((f | (f " A)) +* ((omega \ (f " A)) --> x)) = (dom (f | (f " A))) \/ (dom ((omega \ (f " A)) --> x)) by FUNCT_4:def_1
.= (omega /\ (f " A)) \/ (omega \ (f " A)) by A6, FUNCOP_1:13
.= omega by XBOOLE_1:51 ; ::_thesis: verum
end;
end;
end;
then reconsider F = (f | (f " A)) +* ((omega \ (f " A)) --> x) as Function of omega,A by FUNCT_2:def_1, RELSET_1:4;
take  F ; ::_thesis: rng F = A
thus  rng F = A by A4; ::_thesis: verum
end;

theorem :: CARD_3:97
for f, g being non-empty Function
for x being Element of product f
for y being Element of product g holds x +* y in product (f +* g)
proof
let f, g be non-empty Function; ::_thesis: for x being Element of product f
for y being Element of product g holds x +* y in product (f +* g)
let x be Element of product f; ::_thesis: for y being Element of product g holds x +* y in product (f +* g)
let y be Element of product g; ::_thesis: x +* y in product (f +* g)
A1: dom x = dom f by Th9;
A2: dom y = dom g by Th9;
then A3: dom (x +* y) = (dom f) \/ (dom g) by A1, FUNCT_4:def_1;
A4: dom (f +* g) = (dom f) \/ (dom g) by FUNCT_4:def_1;
now__::_thesis:_for_z_being_set_st_z_in_dom_(f_+*_g)_holds_
(x_+*_y)_._z_in_(f_+*_g)_._z
let z be set ; ::_thesis: ( z in dom (f +* g) implies (x +* y) . z in (f +* g) . z )
assume A5: z in dom (f +* g) ; ::_thesis: (x +* y) . z in (f +* g) . z
then  ( z in dom g or ( not z in dom g & z in dom f ) ) by A4, XBOOLE_0:def_3;
then  ( ( (x +* y) . z = x . z & (f +* g) . z = f . z & x . z in f . z ) or ( (x +* y) . z = y . z & (f +* g) . z = g . z & y . z in g . z ) ) by A1, A2, A4, A5, Th9, FUNCT_4:def_1;
hence  (x +* y) . z in (f +* g) . z ; ::_thesis: verum
end;
hence  x +* y in product (f +* g) by A3, A4, Th9; ::_thesis: verum
end;

theorem :: CARD_3:98
for f, g being non-empty Function
for x being Element of product (f +* g) holds x | (dom g) in product g
proof
let f, g be non-empty Function; ::_thesis: for x being Element of product (f +* g) holds x | (dom g) in product g
let x be Element of product (f +* g); ::_thesis: x | (dom g) in product g
A1: dom x = dom (f +* g) by Th9;
A2: dom (f +* g) = (dom f) \/ (dom g) by FUNCT_4:def_1;
then A3: dom g c= dom x by A1, XBOOLE_1:7;
A4: dom (x | (dom g)) = dom g by A1, A2, RELAT_1:62, XBOOLE_1:7;
now__::_thesis:_for_z_being_set_st_z_in_dom_(x_|_(dom_g))_holds_
(x_|_(dom_g))_._z_in_g_._z
let z be set ; ::_thesis: ( z in dom (x | (dom g)) implies (x | (dom g)) . z in g . z )
assume A5: z in dom (x | (dom g)) ; ::_thesis: (x | (dom g)) . z in g . z
then A6: (x | (dom g)) . z = x . z by FUNCT_1:47;
 (f +* g) . z = g . z by A4, A5, FUNCT_4:13;
hence  (x | (dom g)) . z in g . z by A1, A3, A4, A5, A6, Th9; ::_thesis: verum
end;
hence  x | (dom g) in product g by A4, Th9; ::_thesis: verum
end;

theorem :: CARD_3:99
for f, g being non-empty Function st f tolerates g holds
for x being Element of product (f +* g) holds x | (dom f) in product f
proof
let f, g be non-empty Function; ::_thesis: ( f tolerates g implies for x being Element of product (f +* g) holds x | (dom f) in product f )
assume A1: f tolerates g ; ::_thesis: for x being Element of product (f +* g) holds x | (dom f) in product f
let x be Element of product (f +* g); ::_thesis: x | (dom f) in product f
A2: dom x = dom (f +* g) by Th9;
A3: dom (f +* g) = (dom f) \/ (dom g) by FUNCT_4:def_1;
then A4: dom f c= dom x by A2, XBOOLE_1:7;
A5: dom (x | (dom f)) = dom f by A2, A3, RELAT_1:62, XBOOLE_1:7;
now__::_thesis:_for_z_being_set_st_z_in_dom_(x_|_(dom_f))_holds_
(x_|_(dom_f))_._z_in_f_._z
let z be set ; ::_thesis: ( z in dom (x | (dom f)) implies (x | (dom f)) . z in f . z )
assume A6: z in dom (x | (dom f)) ; ::_thesis: (x | (dom f)) . z in f . z
then A7: (x | (dom f)) . z = x . z by FUNCT_1:47;
 (f +* g) . z = f . z by A1, A5, A6, FUNCT_4:15;
hence  (x | (dom f)) . z in f . z by A2, A4, A5, A6, A7, Th9; ::_thesis: verum
end;
hence  x | (dom f) in product f by A5, Th9; ::_thesis: verum
end;

theorem Th100: :: CARD_3:100
for S being functional with_common_domain set
for f being Function st f in S holds
dom f = dom (product" S)
proof
let S be functional with_common_domain set ; ::_thesis: for f being Function st f in S holds
dom f = dom (product" S)
let f be Function; ::_thesis: ( f in S implies dom f = dom (product" S) )
assume A1: f in S ; ::_thesis: dom f = dom (product" S)
thus  dom f = DOM S by A1, LmX
.= dom (product" S) by Def12 ; ::_thesis: verum
end;

theorem Th101: :: CARD_3:101
for S being functional set
for f being Function
for i being set st f in S & i in dom (product" S) holds
f . i in (product" S) . i
proof
let S be functional set ; ::_thesis: for f being Function
for i being set st f in S & i in dom (product" S) holds
f . i in (product" S) . i
let F be Function; ::_thesis: for i being set st F in S & i in dom (product" S) holds
F . i in (product" S) . i
let i be set ; ::_thesis: ( F in S & i in dom (product" S) implies F . i in (product" S) . i )
assume A1: F in S ; ::_thesis: ( not i in dom (product" S) or F . i in (product" S) . i )
assume  i in dom (product" S) ; ::_thesis: F . i in (product" S) . i
then  (product" S) . i =  {  (f . i) where f is Element of S : verum  }  by A1, Th74;
hence  F . i in (product" S) . i by A1; ::_thesis: verum
end;

theorem :: CARD_3:102
for S being functional with_common_domain set
for f being Function
for i being set st f in S & i in dom f holds
f . i in (product" S) . i
proof
let S be functional with_common_domain set ; ::_thesis: for f being Function
for i being set st f in S & i in dom f holds
f . i in (product" S) . i
let f be Function; ::_thesis: for i being set st f in S & i in dom f holds
f . i in (product" S) . i
let i be set ; ::_thesis: ( f in S & i in dom f implies f . i in (product" S) . i )
assume that
A1: f in S and
A2: i in dom f ; ::_thesis: f . i in (product" S) . i
 dom f = dom (product" S) by A1, Th100;
hence  f . i in (product" S) . i by A1, A2, Th101; ::_thesis: verum
end;

registration
let X be with_common_domain set ;
cluster  ->  with_common_domain for Element of bool X;
coherence
 for b1 being Subset of X holds b1 is with_common_domain
proof
let Y be Subset of X; ::_thesis: Y is with_common_domain
let f, g be Function; :: according to CARD_3:def_10 ::_thesis: ( f in Y & g in Y implies dom f = dom g )
thus  ( f in Y & g in Y implies dom f = dom g ) by Def10; ::_thesis: verum
end;
end;

definition
let f be Function;
let x be set ;
func proj (f,x) ->  Function means :Def16: :: CARD_3:def 16
( dom it = product f & ( for y being Function st y in dom it holds
it . y = y . x ) );
existence
 ex b1 being Function st
( dom b1 = product f & ( for y being Function st y in dom b1 holds
b1 . y = y . x ) )
proof
defpred S2[ set , set ] means  for g being Function st $1 = g holds
$2 = g . x;
A1: now__::_thesis:_for_q_being_set_st_q_in_product_f_holds_
ex_y_being_set_st_S2[q,y]
let q be set ; ::_thesis: ( q in product f implies ex y being set st S2[q,y] )
assume  q in product f ; ::_thesis: ex y being set st S2[q,y]
then reconsider q1 = q as Function ;
take y = q1 . x; ::_thesis: S2[q,y]
thus  S2[q,y] ; ::_thesis: verum
end;
consider F being Function such that
A2: ( dom F = product f & ( for a being set st a in product f holds
S2[a,F . a] ) ) from CLASSES1:sch_1(A1);
take  F ; ::_thesis: ( dom F = product f & ( for y being Function st y in dom F holds
F . y = y . x ) )
thus  ( dom F = product f & ( for y being Function st y in dom F holds
F . y = y . x ) ) by A2; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Function st dom b1 = product f & ( for y being Function st y in dom b1 holds
b1 . y = y . x ) & dom b2 = product f & ( for y being Function st y in dom b2 holds
b2 . y = y . x ) holds
b1 = b2
proof
let F, G be Function; ::_thesis: ( dom F = product f & ( for y being Function st y in dom F holds
F . y = y . x ) & dom G = product f & ( for y being Function st y in dom G holds
G . y = y . x ) implies F = G )
assume that
A3: dom F = product f and
A4: for y being Function st y in dom F holds
F . y = y . x and
A5: dom G = product f and
A6: for y being Function st y in dom G holds
G . y = y . x ; ::_thesis: F = G
now__::_thesis:_for_y_being_set_st_y_in_product_f_holds_
F_._y_=_G_._y
let y be set ; ::_thesis: ( y in product f implies F . y = G . y )
assume A7: y in product f ; ::_thesis: F . y = G . y
then reconsider x1 = y as Function ;
thus F . y = x1 . x by A3, A4, A7
.= G . y by A5, A6, A7 ; ::_thesis: verum
end;
hence  F = G by A3, A5, FUNCT_1:2; ::_thesis: verum
end;
end;

:: deftheorem Def16 defines proj CARD_3:def_16_:_
 for f being Function
for x being set
for b3 being Function holds
( b3 = proj (f,x) iff ( dom b3 = product f & ( for y being Function st y in dom b3 holds
b3 . y = y . x ) ) );

registration
let f be Function;
let x be set ;
cluster proj (f,x) ->  product f -defined ;
coherence
 proj (f,x) is product f -defined
proof
 dom (proj (f,x)) = product f by Def16;
hence  proj (f,x) is product f -defined by RELAT_1:def_18; ::_thesis: verum
end;
end;

registration
let f be Function;
let x be set ;
cluster proj (f,x) ->  total ;
coherence
 proj (f,x) is total
proof
 dom (proj (f,x)) = product f by Def16;
hence  proj (f,x) is total by PARTFUN1:def_2; ::_thesis: verum
end;
end;

registration
let f be non-empty Function;
cluster  -> f -compatible for Element of product f;
coherence
 for b1 being Element of product f holds b1 is f -compatible
proof
let e be Element of product f; ::_thesis: e is f -compatible
let x be set ; :: according to FUNCT_1:def_14 ::_thesis: ( not x in proj1 e or e . x in f . x )
assume  x in dom e ; ::_thesis: e . x in f . x
then  x in dom f by Th9;
hence  e . x in f . x by Th9; ::_thesis: verum
end;
end;

registration
let I be set ;
let f be non-empty I -defined Function;
cluster  -> I -defined for Element of product f;
coherence
 for b1 being Element of product f holds b1 is I -defined ;
end;

registration
let f be Function;
cluster  -> f -compatible for Element of sproduct f;
coherence
 for b1 being Element of sproduct f holds b1 is f -compatible
proof
let e be Element of sproduct f; ::_thesis: e is f -compatible
let x be set ; :: according to FUNCT_1:def_14 ::_thesis: ( not x in proj1 e or e . x in f . x )
thus  ( not x in proj1 e or e . x in f . x ) by Th49; ::_thesis: verum
end;
end;

registration
let I be set ;
let f be I -defined Function;
cluster  -> I -defined for Element of sproduct f;
coherence
 for b1 being Element of sproduct f holds b1 is I -defined ;
end;

registration
let I be set ;
let f be non-empty I -defined total Function;
cluster  ->  total for Element of product f;
coherence
 for b1 being Element of product f holds b1 is total
proof
let e be Element of product f; ::_thesis: e is total
thus  dom e = dom f by Th9
.= I by PARTFUN1:def_2 ; :: according to PARTFUN1:def_2 ::_thesis: verum
end;
end;

theorem Th103: :: CARD_3:103
for I being set
for f being non-empty b1 -defined Function
for p being b1 -defined b2 -compatible Function holds p in sproduct f
proof
let I be set ; ::_thesis: for f being non-empty I -defined Function
for p being I -defined b1 -compatible Function holds p in sproduct f
let f be non-empty I -defined Function; ::_thesis: for p being I -defined f -compatible Function holds p in sproduct f
let p be I -defined f -compatible Function; ::_thesis: p in sproduct f
A1: dom p c= dom f by FUNCT_1:105;
 for x being set st x in dom p holds
p . x in f . x by FUNCT_1:def_14;
hence  p in sproduct f by A1, Def9; ::_thesis: verum
end;

theorem :: CARD_3:104
for I being set
for f being non-empty b1 -defined Function
for p being b1 -defined b2 -compatible Function ex s being Element of product f st p c= s
proof
let I be set ; ::_thesis: for f being non-empty I -defined Function
for p being I -defined b1 -compatible Function ex s being Element of product f st p c= s
let f be non-empty I -defined Function; ::_thesis: for p being I -defined f -compatible Function ex s being Element of product f st p c= s
let p be I -defined f -compatible Function; ::_thesis: ex s being Element of product f st p c= s
reconsider p = p as Element of sproduct f by Th103;
set h = the Element of product f;
reconsider s = the Element of product f +* p as Element of product f by Th53;
take  s ; ::_thesis: p c= s
thus  p c= s by FUNCT_4:25; ::_thesis: verum
end;

registration
let X be infinite set ;
let a be set ;
clusterX --> a ->  infinite ;
coherence
 not X --> a is finite ;
end;

registration
cluster Relation-like Function-like infinite for set ;
existence
 ex b1 being Function st b1 is infinite
proof
take  omega --> 0 ; ::_thesis: omega --> 0 is infinite
thus  omega --> 0 is infinite ; ::_thesis: verum
end;
end;

registration
let R be infinite Relation;
cluster field R ->  infinite ;
coherence
 not field R is finite by ORDERS_1:86;
end;

registration
let X be infinite set ;
cluster RelIncl X ->  infinite ;
coherence
 not RelIncl X is finite by CARD_1:63;
end;

theorem :: CARD_3:105
for R, S being Relation st R,S are_isomorphic & R is finite holds
S is finite
proof
let R, S be Relation; ::_thesis: ( R,S are_isomorphic & R is finite implies S is finite )
given F being Function such that A1: F is_isomorphism_of R,S ; :: according to WELLORD1:def_8 ::_thesis: ( not R is finite or S is finite )
assume  R is finite ; ::_thesis: S is finite
then  field R is finite ;
then  dom F is finite by A1, WELLORD1:def_7;
then  rng F is finite by FINSET_1:8;
then  field S is finite by A1, WELLORD1:def_7;
hence  S is finite ; ::_thesis: verum
end;

theorem :: CARD_3:106
product" {{}} = {}
proof
dom (product" {{}}) = DOM {{}} by Def12
.= {} by Th72 ;
hence  product" {{}} = {} ; ::_thesis: verum
end;

theorem Th107: :: CARD_3:107
for I being set
for f being V8() ManySortedSet of I
for s being b2 -compatible ManySortedSet of I holds s in product f
proof
let I be set ; ::_thesis: for f being V8() ManySortedSet of I
for s being b1 -compatible ManySortedSet of I holds s in product f
let f be V8() ManySortedSet of I; ::_thesis: for s being f -compatible ManySortedSet of I holds s in product f
let s be f -compatible ManySortedSet of I; ::_thesis: s in product f
A1: dom s = I by PARTFUN1:def_2
.= dom f by PARTFUN1:def_2 ;
then  for x being set st x in dom f holds
s . x in f . x by FUNCT_1:def_14;
hence  s in product f by A1, Th9; ::_thesis: verum
end;

registration
let I be set ;
let f be V8() ManySortedSet of I;
cluster  ->  total for Element of product f;
coherence
 for b1 being Element of product f holds b1 is total ;
end;

definition
let I be set ;
let f be V8() ManySortedSet of I;
let M be f -compatible ManySortedSet of I;
func down M ->  Element of product f equals :: CARD_3:def 17
M;
coherence
 M is Element of product f by Th107;
end;

:: deftheorem  defines down CARD_3:def_17_:_
 for I being set
for f being V8() ManySortedSet of I
for M being b2 -compatible ManySortedSet of I holds down M = M;

theorem :: CARD_3:108
for X being functional with_common_domain set
for f being Function st f in X holds
dom f = DOM X by LmX;

theorem :: CARD_3:109
for x being set
for X being non empty functional set st ( for f being Function st f in X holds
x in dom f ) holds
x in DOM X
proof
let x be set ; ::_thesis: for X being non empty functional set st ( for f being Function st f in X holds
x in dom f ) holds
x in DOM X
let X be non empty functional set ; ::_thesis: ( ( for f being Function st f in X holds
x in dom f ) implies x in DOM X )
assume Z: for f being Function st f in X holds
x in dom f ; ::_thesis: x in DOM X
set A =  {  (dom f) where f is Element of X : verum  }  ;
consider Y being set  such that
W: Y in X by XBOOLE_0:def_1;
reconsider Y = Y as Function by W;
S: dom Y in  {  (dom f) where f is Element of X : verum  }  by W;
 for Y being set st Y in  {  (dom f) where f is Element of X : verum  }  holds
x in Y
proof
let Y be set ; ::_thesis: ( Y in  {  (dom f) where f is Element of X : verum  }  implies x in Y )
assume  Y in  {  (dom f) where f is Element of X : verum  }  ; ::_thesis: x in Y
then  ex f being Element of X st Y = dom f ;
hence  x in Y by Z; ::_thesis: verum
end;
hence  x in DOM X by S, SETFAM_1:def_1; ::_thesis: verum
end;