environ
vocabularies HIDDEN, NUMBERS, FUNCT_1, FINSEQ_1, NAT_1, RELAT_1, FINSET_1, CARD_1, XBOOLE_0, TARSKI, XXREAL_0, SUBSET_1, PARTFUN1, ARYTM_1, ARYTM_3, ORDINAL4, FINSEQ_4, FUNCT_2, EQREL_1, CARD_3, SETFAM_1;
notations HIDDEN, TARSKI, XBOOLE_0, ENUMSET1, SUBSET_1, ORDINAL1, RELAT_1, CARD_1, SETFAM_1, EQREL_1, NUMBERS, XCMPLX_0, FUNCT_1, PARTFUN1, FUNCT_2, FINSET_1, NAT_1, FINSEQ_1, FINSEQ_3, XXREAL_0;
definitions FUNCT_1, TARSKI, XBOOLE_0;
theorems CARD_1, CARD_2, ENUMSET1, FINSEQ_1, FINSEQ_2, FINSEQ_3, FUNCT_1, FUNCT_2, INT_1, NAT_1, PARTFUN1, TARSKI, WELLORD2, ZFMISC_1, RELAT_1, XBOOLE_0, XBOOLE_1, XREAL_1, XXREAL_0, ORDINAL1, GRFUNC_1, EQREL_1, RELSET_1, SETFAM_1;
schemes FINSEQ_1, FINSET_1, NAT_1, FUNCT_1, FINSEQ_2, FUNCT_2;
registrations XBOOLE_0, RELAT_1, FUNCT_1, FINSET_1, XREAL_0, INT_1, FINSEQ_1, ORDINAL1, CARD_1, RELSET_1, SUBSET_1, EQREL_1, NAT_1, PARTFUN1, FUNCT_2, XXREAL_0;
constructors HIDDEN, ENUMSET1, WELLORD2, FUNCT_2, XXREAL_0, REAL_1, PARTFUN1, NAT_1, INT_1, FINSEQ_3, RELSET_1, EQREL_1, SETFAM_1;
requirements HIDDEN, REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
equalities RELAT_1, FINSEQ_1, CARD_1, ORDINAL1;
expansions RELAT_1, FUNCT_1, XBOOLE_0, FINSEQ_1;
Lm1:
for A, B being finite set
for f being Function of A,B st card A = card B & rng f = B holds
f is one-to-one
::
deftheorem defines
<* FINSEQ_4:def 8 :
for x1, x2, x3, x4, x5 being object holds <*x1,x2,x3,x4,x5*> = <*x1,x2,x3*> ^ <*x4,x5*>;
registration
let x1,
x2,
x3,
x4 be
object ;
coherence
( not <*x1,x2,x3,x4*> is empty & <*x1,x2,x3,x4*> is Function-like & <*x1,x2,x3,x4*> is Relation-like )
;
let x5 be
object ;
coherence
( not <*x1,x2,x3,x4,x5*> is empty & <*x1,x2,x3,x4,x5*> is Function-like & <*x1,x2,x3,x4,x5*> is Relation-like )
;
end;
registration
let x1,
x2,
x3,
x4 be
object ;
coherence
<*x1,x2,x3,x4*> is FinSequence-like
;
let x5 be
object ;
coherence
<*x1,x2,x3,x4,x5*> is FinSequence-like
;
end;
definition
let D be non
empty set ;
let x1,
x2,
x3,
x4,
x5 be
Element of
D;
<*redefine func <*x1,x2,x3,x4,x5*> -> FinSequence of
D;
coherence
<*x1,x2,x3,x4,x5*> is FinSequence of D
end;
theorem Th74:
for
x1,
x2,
x3,
x4 being
object holds
(
<*x1,x2,x3,x4*> = <*x1,x2,x3*> ^ <*x4*> &
<*x1,x2,x3,x4*> = <*x1,x2*> ^ <*x3,x4*> &
<*x1,x2,x3,x4*> = <*x1*> ^ <*x2,x3,x4*> &
<*x1,x2,x3,x4*> = ((<*x1*> ^ <*x2*>) ^ <*x3*>) ^ <*x4*> )
theorem Th75:
for
x1,
x2,
x3,
x4,
x5 being
object holds
(
<*x1,x2,x3,x4,x5*> = <*x1,x2,x3*> ^ <*x4,x5*> &
<*x1,x2,x3,x4,x5*> = <*x1,x2,x3,x4*> ^ <*x5*> &
<*x1,x2,x3,x4,x5*> = (((<*x1*> ^ <*x2*>) ^ <*x3*>) ^ <*x4*>) ^ <*x5*> &
<*x1,x2,x3,x4,x5*> = <*x1,x2*> ^ <*x3,x4,x5*> &
<*x1,x2,x3,x4,x5*> = <*x1*> ^ <*x2,x3,x4,x5*> )
theorem
for
ND being non
empty set for
y1,
y2,
y3,
y4 being
Element of
ND holds
(
<*y1,y2,y3,y4*> /. 1
= y1 &
<*y1,y2,y3,y4*> /. 2
= y2 &
<*y1,y2,y3,y4*> /. 3
= y3 &
<*y1,y2,y3,y4*> /. 4
= y4 )
theorem
for
ND being non
empty set for
y1,
y2,
y3,
y4,
y5 being
Element of
ND holds
(
<*y1,y2,y3,y4,y5*> /. 1
= y1 &
<*y1,y2,y3,y4,y5*> /. 2
= y2 &
<*y1,y2,y3,y4,y5*> /. 3
= y3 &
<*y1,y2,y3,y4,y5*> /. 4
= y4 &
<*y1,y2,y3,y4,y5*> /. 5
= y5 )
registration
let x1,
x2,
x3,
x4 be
object ;
coherence
<*x1,x2,x3,x4*> is 4 -element
;
let x5 be
object ;
coherence
<*x1,x2,x3,x4,x5*> is 5 -element
;
end;
:: Pigeon Hole Principle