begin
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem Th14:
theorem
theorem Th16:
theorem Th17:
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 Element of NAT st S1[n] holds
S1[n + 1]
theorem
:: deftheorem RFINSEQ:def 1 :
canceled;
:: deftheorem Def2 defines /^ RFINSEQ:def 2 :
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
theorem Th19:
theorem Th20:
theorem Th21:
theorem
:: deftheorem Def3 defines MIM RFINSEQ:def 3 :
theorem Th23:
theorem Th24:
theorem Th25:
theorem Th26:
theorem
theorem
theorem Th29:
theorem
:: deftheorem Def4 defines non-increasing RFINSEQ:def 4 :
theorem Th31:
theorem Th32:
theorem Th33:
theorem
Lm4:
for f, g being non-increasing FinSequence of REAL
for n being Element of 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 Element of NAT st S2[n] holds
S2[n + 1]
theorem
Lm7:
for n being Element of NAT
for g1, g2 being non-increasing FinSequence of REAL st n = len g1 & g1,g2 are_fiberwise_equipotent holds
g1 = g2
theorem
theorem
theorem
begin
theorem
theorem
theorem
theorem
theorem Th43:
theorem Th44:
theorem