:: by Grzegorz Bancerek

::

:: Received April 10, 1990

:: Copyright (c) 1990-2021 Association of Mizar Users

definition

let IT be Function;

end;
attr IT is Cardinal-yielding means :Def1: :: CARD_3:def 1

for x being object st x in dom IT holds

IT . x is Cardinal;

for x being object st x in dom IT holds

IT . x is Cardinal;

:: deftheorem Def1 defines Cardinal-yielding CARD_3:def 1 :

for IT being Function holds

( IT is Cardinal-yielding iff for x being object st x in dom IT holds

IT . x is Cardinal );

for IT being Function holds

( IT is Cardinal-yielding iff for x being object st x in dom IT holds

IT . x is Cardinal );

registration
end;

registration
end;

registration
end;

definition

let f be Function;

ex b_{1} being Cardinal-Function st

( dom b_{1} = dom f & ( for x being object st x in dom f holds

b_{1} . x = card (f . x) ) )

for b_{1}, b_{2} being Cardinal-Function st dom b_{1} = dom f & ( for x being object st x in dom f holds

b_{1} . x = card (f . x) ) & dom b_{2} = dom f & ( for x being object st x in dom f holds

b_{2} . x = card (f . x) ) holds

b_{1} = b_{2}

ex b_{1} being Function st

( dom b_{1} = dom f & ( for x being object st x in dom f holds

b_{1} . x = [:(f . x),{x}:] ) )

for b_{1}, b_{2} being Function st dom b_{1} = dom f & ( for x being object st x in dom f holds

b_{1} . x = [:(f . x),{x}:] ) & dom b_{2} = dom f & ( for x being object st x in dom f holds

b_{2} . x = [:(f . x),{x}:] ) holds

b_{1} = b_{2}

coherence

union (rng f) is set ;

;

defpred S_{1}[ object ] means ex g being Function st

( $1 = g & dom g = dom f & ( for x being object st x in dom f holds

g . x in f . x ) );

ex b_{1} being set st

for x being object holds

( x in b_{1} iff ex g being Function st

( x = g & dom g = dom f & ( for y being object st y in dom f holds

g . y in f . y ) ) )

for b_{1}, b_{2} being set st ( for x being object holds

( x in b_{1} iff ex g being Function st

( x = g & dom g = dom f & ( for y being object st y in dom f holds

g . y in f . y ) ) ) ) & ( for x being object holds

( x in b_{2} iff ex g being Function st

( x = g & dom g = dom f & ( for y being object st y in dom f holds

g . y in f . y ) ) ) ) holds

b_{1} = b_{2}

end;
func Card f -> Cardinal-Function means :Def2: :: CARD_3:def 2

( dom it = dom f & ( for x being object st x in dom f holds

it . x = card (f . x) ) );

existence ( dom it = dom f & ( for x being object st x in dom f holds

it . x = card (f . x) ) );

ex b

( dom b

b

proof end;

uniqueness for b

b

b

b

proof end;

func disjoin f -> Function means :Def3: :: CARD_3:def 3

( dom it = dom f & ( for x being object st x in dom f holds

it . x = [:(f . x),{x}:] ) );

existence ( dom it = dom f & ( for x being object st x in dom f holds

it . x = [:(f . x),{x}:] ) );

ex b

( dom b

b

proof end;

uniqueness for b

b

b

b

proof end;

correctness coherence

union (rng f) is set ;

;

defpred S

( $1 = g & dom g = dom f & ( for x being object st x in dom f holds

g . x in f . x ) );

func product f -> set means :Def5: :: CARD_3:def 5

for x being object holds

( x in it iff ex g being Function st

( x = g & dom g = dom f & ( for y being object st y in dom f holds

g . y in f . y ) ) );

existence for x being object holds

( x in it iff ex g being Function st

( x = g & dom g = dom f & ( for y being object st y in dom f holds

g . y in f . y ) ) );

ex b

for x being object holds

( x in b

( x = g & dom g = dom f & ( for y being object st y in dom f holds

g . y in f . y ) ) )

proof end;

uniqueness for b

( x in b

( x = g & dom g = dom f & ( for y being object st y in dom f holds

g . y in f . y ) ) ) ) & ( for x being object holds

( x in b

( x = g & dom g = dom f & ( for y being object st y in dom f holds

g . y in f . y ) ) ) ) holds

b

proof end;

:: deftheorem Def2 defines Card CARD_3:def 2 :

for f being Function

for b_{2} being Cardinal-Function holds

( b_{2} = Card f iff ( dom b_{2} = dom f & ( for x being object st x in dom f holds

b_{2} . x = card (f . x) ) ) );

for f being Function

for b

( b

b

:: deftheorem Def3 defines disjoin CARD_3:def 3 :

for f, b_{2} being Function holds

( b_{2} = disjoin f iff ( dom b_{2} = dom f & ( for x being object st x in dom f holds

b_{2} . x = [:(f . x),{x}:] ) ) );

for f, b

( b

b

:: deftheorem Def5 defines product CARD_3:def 5 :

for f being Function

for b_{2} being set holds

( b_{2} = product f iff for x being object holds

( x in b_{2} iff ex g being Function st

( x = g & dom g = dom f & ( for y being object st y in dom f holds

g . y in f . y ) ) ) );

for f being Function

for b

( b

( x in b

( x = g & dom g = dom f & ( for y being object st y in dom f holds

g . y in f . y ) ) ) );

theorem :: CARD_3:5

for x, y being object

for f being Function st x in dom f & y in dom f & x <> y holds

(disjoin f) . x misses (disjoin f) . y

for f being Function st x in dom f & y in dom f & x <> y holds

(disjoin f) . x misses (disjoin f) . y

proof end;

theorem Th9: :: CARD_3:9

for f, g being Function holds

( g in product f iff ( dom g = dom f & ( for x being object st x in dom f holds

g . x in f . x ) ) )

( g in product f iff ( dom g = dom f & ( for x being object st x in dom f holds

g . x in f . x ) ) )

proof end;

defpred S

definition

let x be object ;

let X be set ;

defpred S_{2}[ object , object ] means ex g being Function st

( $1 = g & $2 = g . x );

ex b_{1} being set st

for y being object holds

( y in b_{1} iff ex f being Function st

( f in X & y = f . x ) )

for b_{1}, b_{2} being set st ( for y being object holds

( y in b_{1} iff ex f being Function st

( f in X & y = f . x ) ) ) & ( for y being object holds

( y in b_{2} iff ex f being Function st

( f in X & y = f . x ) ) ) holds

b_{1} = b_{2}

end;
let X be set ;

defpred S

( $1 = g & $2 = g . x );

func pi (X,x) -> set means :Def6: :: CARD_3:def 6

for y being object holds

( y in it iff ex f being Function st

( f in X & y = f . x ) );

existence for y being object holds

( y in it iff ex f being Function st

( f in X & y = f . x ) );

ex b

for y being object holds

( y in b

( f in X & y = f . x ) )

proof end;

uniqueness for b

( y in b

( f in X & y = f . x ) ) ) & ( for y being object holds

( y in b

( f in X & y = f . x ) ) ) holds

b

proof end;

:: deftheorem Def6 defines pi CARD_3:def 6 :

for x being object

for X, b_{3} being set holds

( b_{3} = pi (X,x) iff for y being object holds

( y in b_{3} iff ex f being Function st

( f in X & y = f . x ) ) );

for x being object

for X, b

( b

( y in b

( f in X & y = f . x ) ) );

theorem :: CARD_3:12

for x being object

for f being Function st x in dom f & product f <> {} holds

pi ((product f),x) = f . x

for f being Function st x in dom f & product f <> {} holds

pi ((product f),x) = f . x

proof end;

theorem Th21: :: CARD_3:21

for x being object

for f being Function st x in Union (disjoin f) holds

ex y, z being object st x = [y,z]

for f being Function st x in Union (disjoin f) holds

ex y, z being object st x = [y,z]

proof end;

theorem Th22: :: CARD_3:22

for x being object

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)] ) )

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 end;

theorem Th27: :: CARD_3:27

for f, g being Function st dom f = dom g & ( for x being object st x in dom f holds

f . x c= g . x ) holds

product f c= product g

f . x c= g . x ) holds

product f c= product g

proof end;

definition

let F be Cardinal-Function;

correctness

coherence

card (Union (disjoin F)) is Cardinal;

;

correctness

coherence

card (product F) is Cardinal;

;

end;
correctness

coherence

card (Union (disjoin F)) is Cardinal;

;

correctness

coherence

card (product F) is Cardinal;

;

:: deftheorem defines Sum CARD_3:def 7 :

for F being Cardinal-Function holds Sum F = card (Union (disjoin F));

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);

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 object st x in dom F holds

F . x c= G . x ) holds

Sum F c= Sum G

F . x c= G . x ) holds

Sum F c= Sum G

proof end;

theorem :: CARD_3:32

:: Koenig Theorem

theorem :: CARD_3:41

for F, G being Cardinal-Function st dom F = dom G & ( for x being object st x in dom F holds

F . x in G . x ) holds

Sum F in Product G

F . x in G . x ) holds

Sum F in Product G

proof end;

Lm1: for x being object

for R being Relation st x in field R holds

ex y being object st

( [x,y] in R or [y,x] in R )

proof 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 ) ) ) )

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 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

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 end;

:: from AMI_1

registration
end;

registration

let A be set ;

let B be with_non-empty_elements set ;

coherence

for b_{1} being Function of A,B holds b_{1} is non-empty

end;
let B be with_non-empty_elements set ;

coherence

for b

proof end;

:: from PRVECT_1

:: from AMI_1, 2006.03.14, A.T.

:: from AMI_1, 2006.03.14, A.T.

theorem :: CARD_3:48

definition

let f be Function;

ex b_{1} being set st

for x being object holds

( x in b_{1} iff ex g being Function st

( x = g & dom g c= dom f & ( for x being object st x in dom g holds

g . x in f . x ) ) )

for b_{1}, b_{2} being set st ( for x being object holds

( x in b_{1} iff ex g being Function st

( x = g & dom g c= dom f & ( for x being object st x in dom g holds

g . x in f . x ) ) ) ) & ( for x being object holds

( x in b_{2} iff ex g being Function st

( x = g & dom g c= dom f & ( for x being object st x in dom g holds

g . x in f . x ) ) ) ) holds

b_{1} = b_{2}

end;
func sproduct f -> set means :Def9: :: CARD_3:def 9

for x being object holds

( x in it iff ex g being Function st

( x = g & dom g c= dom f & ( for x being object st x in dom g holds

g . x in f . x ) ) );

existence for x being object holds

( x in it iff ex g being Function st

( x = g & dom g c= dom f & ( for x being object st x in dom g holds

g . x in f . x ) ) );

ex b

for x being object holds

( x in b

( x = g & dom g c= dom f & ( for x being object st x in dom g holds

g . x in f . x ) ) )

proof end;

uniqueness for b

( x in b

( x = g & dom g c= dom f & ( for x being object st x in dom g holds

g . x in f . x ) ) ) ) & ( for x being object holds

( x in b

( x = g & dom g c= dom f & ( for x being object st x in dom g holds

g . x in f . x ) ) ) ) holds

b

proof end;

:: deftheorem Def9 defines sproduct CARD_3:def 9 :

for f being Function

for b_{2} being set holds

( b_{2} = sproduct f iff for x being object holds

( x in b_{2} iff ex g being Function st

( x = g & dom g c= dom f & ( for x being object st x in dom g holds

g . x in f . x ) ) ) );

for f being Function

for b

( b

( x in b

( x = g & dom g c= dom f & ( for x being object st x in dom g holds

g . x in f . x ) ) ) );

registration
end;

theorem Th49: :: CARD_3:49

for f, g being Function st g in sproduct f holds

( dom g c= dom f & ( for x being object st x in dom g holds

g . x in f . x ) )

( dom g c= dom f & ( for x being object st x in dom g holds

g . x in f . x ) )

proof end;

registration
end;

theorem Th52: :: CARD_3:52

for x being object

for f being Function st x in sproduct f holds

x is PartFunc of (dom f),(union (rng f))

for f being Function st x in sproduct f holds

x is PartFunc of (dom f),(union (rng f))

proof 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 ) )

( g in sproduct f iff ex h being Function st

( h in product f & g c= h ) )

proof 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 <> {} } )

for f being Function of A,B holds sproduct f = sproduct (f | { x where x is Element of A : f . x <> {} } )

proof end;

theorem :: CARD_3:61

for f being Function holds

( sproduct f = {{}} iff for x being object st x in dom f holds

f . x = {} )

( sproduct f = {{}} iff for x being object st x in dom f holds

f . x = {} )

proof 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

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 end;

theorem :: CARD_3:63

for f, g, h being Function st g tolerates h & g in sproduct f & h in sproduct f holds

g \/ h in sproduct f

g \/ h in sproduct f

proof end;

theorem :: CARD_3:67

for f, g, h 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 )

ex f9, g9 being Function st

( f9 in sproduct f & g9 in sproduct g & h = f9 +* g9 )

proof end;

theorem Th68: :: CARD_3:68

for f, g, 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)

f9 +* g9 in sproduct (f +* g)

proof end;

theorem :: CARD_3:69

for f, g, 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)

f9 +* g9 in sproduct (f +* g)

proof 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

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 end;

definition

let IT be set ;

end;
attr IT 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;

for f, g being Function st f in IT & g in IT holds

dom f = dom g;

:: 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 );

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

existence

ex b_{1} being set st

( b_{1} is with_common_domain & b_{1} is functional & not b_{1} is empty )

end;
ex b

( b

proof end;

definition
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 } ;

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

Lm2: for X being functional with_common_domain set

for f being Function st f in X holds

dom f = DOM X

proof end;

definition

let S be functional set ;

ex b_{1} being Function st

( dom b_{1} = DOM S & ( for i being set st i in dom b_{1} holds

b_{1} . i = pi (S,i) ) )

for b_{1}, b_{2} being Function st dom b_{1} = DOM S & ( for i being set st i in dom b_{1} holds

b_{1} . i = pi (S,i) ) & dom b_{2} = DOM S & ( for i being set st i in dom b_{2} holds

b_{2} . i = pi (S,i) ) holds

b_{1} = b_{2}

end;
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 ( dom it = DOM S & ( for i being set st i in dom it holds

it . i = pi (S,i) ) );

ex b

( dom b

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem Def12 defines product" CARD_3:def 12 :

for S being functional set

for b_{2} being Function holds

( b_{2} = product" S iff ( dom b_{2} = DOM S & ( for i being set st i in dom b_{2} holds

b_{2} . i = pi (S,i) ) ) );

for S being functional set

for b

( b

b

::$CT

theorem Th73: :: 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 }

for i being set st i in dom (product" S) holds

(product" S) . i = { (f . i) where f is Element of S : verum }

proof 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 );

for S being set holds

( S is product-like iff ex f being Function st S = product f );

registration
end;

registration

coherence

for b_{1} being set st b_{1} is product-like holds

( b_{1} is functional & b_{1} is with_common_domain )

end;
for b

( b

proof end;

registration
end;

::$CT 2

:: from AMI_1, 2008.04.11, A.T. (generalized)

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

for s, t being Element of product f

for A being set holds s +* (t | A) is Element of product f

proof 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

for p being Element of sproduct f ex s being Element of product f st p c= s

proof end;

:: needed, 2008.04.20, A.T.

definition

let f be non-empty Function;

let g be Element of product f;

let X be set ;

:: original: |

redefine func g | X -> Element of sproduct f;

coherence

g | X is Element of sproduct f by Th78;

end;
let g be Element of product f;

let X be set ;

:: original: |

redefine func g | X -> Element of sproduct f;

coherence

g | X is Element of sproduct f by Th78;

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

for s, ss being Element of product f

for A being set holds (ss +* (s | A)) | A = s | A

proof end;

:: from PRE_CIRC, 2008.06.02, A.T.

:: moved from CARD_4, 2008.10.08, A.T.

:: deftheorem Def14 defines countable CARD_3:def 14 :

for X being set holds

( X is countable iff card X c= omega );

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 );

for X being set holds

( X is denumerable iff card X = omega );

registration

coherence

for b_{1} being set st b_{1} is denumerable holds

( b_{1} is countable & b_{1} is infinite )
;

coherence

for b_{1} being set st b_{1} is countable & b_{1} is infinite holds

b_{1} is denumerable

end;
for b

( b

coherence

for b

b

proof end;

registration
end;

registration
end;

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

Y is countable

;

theorem :: CARD_3:94

:: from CIRCCOMB, 2009.01.26, A.T.

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)

for x being Element of product f

for y being Element of product g holds x +* y in product (f +* g)

proof 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

for x being Element of product (f +* g) holds x | (dom g) in product g

proof 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

for x being Element of product (f +* g) holds x | (dom f) in product f

proof end;

:: missing, 2009.09.06, A.T.

theorem Th97: :: 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)

for f being Function st f in S holds

dom f = dom (product" S)

proof end;

theorem Th98: :: 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

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 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

for f being Function

for i being set st f in S & i in dom f holds

f . i in (product" S) . i

proof end;

:: 2009.09.12, A.T.

registration

let X be with_common_domain set ;

coherence

for b_{1} being Subset of X holds b_{1} is with_common_domain
by Def10;

end;
coherence

for b

:: from PRALG_3, 2009.09.18, A.T.

definition

let f be Function;

let x be object ;

ex b_{1} being Function st

( dom b_{1} = product f & ( for y being Function st y in dom b_{1} holds

b_{1} . y = y . x ) )

for b_{1}, b_{2} being Function st dom b_{1} = product f & ( for y being Function st y in dom b_{1} holds

b_{1} . y = y . x ) & dom b_{2} = product f & ( for y being Function st y in dom b_{2} holds

b_{2} . y = y . x ) holds

b_{1} = b_{2}

end;
let x be object ;

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 ( dom it = product f & ( for y being Function st y in dom it holds

it . y = y . x ) );

ex b

( dom b

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem Def16 defines proj CARD_3:def 16 :

for f being Function

for x being object

for b_{3} being Function holds

( b_{3} = proj (f,x) iff ( dom b_{3} = product f & ( for y being Function st y in dom b_{3} holds

b_{3} . y = y . x ) ) );

for f being Function

for x being object

for b

( b

b

registration
end;

registration

let f be non-empty Function;

coherence

for b_{1} being Element of product f holds b_{1} is f -compatible

end;
coherence

for b

proof end;

registration

let I be set ;

let f be non-empty I -defined Function;

coherence

for b_{1} being Element of product f holds b_{1} is I -defined
;

end;
let f be non-empty I -defined Function;

coherence

for b

registration

let f be Function;

coherence

for b_{1} being Element of sproduct f holds b_{1} is f -compatible
by Th49;

end;
coherence

for b

registration

let I be set ;

let f be I -defined Function;

coherence

for b_{1} being Element of sproduct f holds b_{1} is I -defined
;

end;
let f be I -defined Function;

coherence

for b

registration

let I be set ;

let f be non-empty I -defined total Function;

coherence

for b_{1} being Element of product f holds b_{1} is total

end;
let f be non-empty I -defined total Function;

coherence

for b

proof end;

theorem Th100: :: CARD_3:103

for I being set

for f being non-empty b_{1} -defined Function

for p being b_{1} -defined b_{2} -compatible Function holds p in sproduct f

for f being non-empty b

for p being b

proof end;

theorem :: CARD_3:104

for I being set

for f being non-empty b_{1} -defined Function

for p being b_{1} -defined b_{2} -compatible Function ex s being Element of product f st p c= s

for f being non-empty b

for p being b

proof end;

:: from AMISTD_2, 2010.01.10, A.T

Lm4: for R being Relation st field R is finite holds

R is finite

proof end;

registration
end;

theorem Th104: :: CARD_3:107

for I being set

for f being V8() ManySortedSet of I

for s being b_{2} -compatible ManySortedSet of I holds s in product f

for f being V8() ManySortedSet of I

for s being b

proof end;

registration

let I be set ;

let f be V8() ManySortedSet of I;

coherence

for b_{1} being Element of product f holds b_{1} is total
;

end;
let f be V8() ManySortedSet of I;

coherence

for b

definition

let I be set ;

let f be V8() ManySortedSet of I;

let M be f -compatible ManySortedSet of I;

coherence

M is Element of product f by Th104;

end;
let f be V8() ManySortedSet of I;

let M be f -compatible ManySortedSet of I;

coherence

M is Element of product f by Th104;

:: deftheorem defines down CARD_3:def 17 :

for I being set

for f being V8() ManySortedSet of I

for M being b_{2} -compatible ManySortedSet of I holds down M = M;

for I being set

for f being V8() ManySortedSet of I

for M being b

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 Lm2;

for f being Function st f in X holds

dom f = DOM X by Lm2;

theorem :: CARD_3:109

for x being object

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

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 end;