environ
vocabularies HIDDEN, NUMBERS, SUBSET_1, REAL_1, FINSEQ_1, RELAT_1, FINSET_1, CLASSES1, ORDINAL4, CARD_1, ARYTM_3, FUNCT_2, XBOOLE_0, TARSKI, NAT_1, FUNCT_1, ARYTM_1, XXREAL_0, CARD_3, VALUED_0, FUNCOP_1, FUNCT_4, RFINSEQ;
notations HIDDEN, TARSKI, XBOOLE_0, SUBSET_1, CARD_1, ORDINAL1, NUMBERS, RELAT_1, FUNCT_1, RELSET_1, FUNCT_2, FINSEQ_1, XCMPLX_0, XREAL_0, NAT_1, REAL_1, CLASSES1, SEQM_3, FINSEQ_4, FINSET_1, FUNCOP_1, FUNCT_4, VALUED_0, RVSUM_1, XXREAL_0;
definitions TARSKI, XBOOLE_0, SEQM_3, CLASSES1;
theorems TARSKI, FINSEQ_1, FINSEQ_2, FINSEQ_3, NAT_1, FUNCT_1, FUNCT_2, CARD_1, CARD_2, RVSUM_1, ZFMISC_1, RELAT_1, XBOOLE_0, XBOOLE_1, XCMPLX_1, XREAL_1, FINSEQ_4, XXREAL_0, FINSOP_1, FUNCOP_1, FUNCT_4, ORDINAL1, XREAL_0, CLASSES1, INT_1;
schemes NAT_1, FINSEQ_1;
registrations XBOOLE_0, RELAT_1, FUNCT_1, FINSET_1, NUMBERS, XREAL_0, NAT_1, FINSEQ_1, FUNCOP_1, VALUED_0, CARD_1, INT_1, RELSET_1, RVSUM_1, ORDINAL1;
constructors HIDDEN, PARTFUN1, WELLORD2, REAL_1, SQUARE_1, NAT_1, BINOP_2, SEQM_3, FINSEQ_4, FINSOP_1, RVSUM_1, FUNCOP_1, CLASSES1, RELSET_1;
requirements HIDDEN, REAL, NUMERALS, BOOLE, SUBSET, ARITHM;
equalities RVSUM_1, FUNCOP_1, RELAT_1;
expansions TARSKI, XBOOLE_0, SEQM_3, CLASSES1;
defpred S1[ Nat] means for X being finite set
for F being Function st card (dom (F | X)) = $1 holds
ex a being FinSequence st F | X,a are_fiberwise_equipotent ;
Lm1:
S1[ 0 ]
Lm2:
for n being Nat st S1[n] holds
S1[n + 1]
Lm3:
for n being Nat
for D being non empty set
for f being FinSequence of D st len f <= n holds
f | n = f
Lm4:
for f, g being non-increasing FinSequence of REAL
for n being Nat st len f = n + 1 & len f = len g & f,g are_fiberwise_equipotent holds
( f . (len f) = g . (len g) & f | n,g | n are_fiberwise_equipotent )
defpred S2[ Nat] means for R being FinSequence of REAL st $1 = len R holds
ex b being non-increasing FinSequence of REAL st R,b are_fiberwise_equipotent ;
Lm5:
S2[ 0 ]
Lm6:
for n being Nat st S2[n] holds
S2[n + 1]
Lm7:
for n being Nat
for g1, g2 being non-increasing FinSequence of REAL st n = len g1 & g1,g2 are_fiberwise_equipotent holds
g1 = g2