begin
:: deftheorem Def1 defines max_p RFINSEQ2:def 1 :
:: deftheorem Def2 defines min_p RFINSEQ2:def 2 :
:: deftheorem defines max RFINSEQ2:def 3 :
:: deftheorem defines min RFINSEQ2:def 4 :
theorem Th1:
theorem Th2:
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
Lm1:
for f, g being FinSequence of REAL st f,g are_fiberwise_equipotent holds
max f <= max g
theorem Th14:
Lm2:
for f, g being FinSequence of REAL st f,g are_fiberwise_equipotent holds
min f >= min g
theorem Th15:
:: deftheorem Def5 defines sort_d RFINSEQ2:def 5 :
theorem Th16:
theorem Th17:
Lm3:
for f, g being non-decreasing 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 )
theorem Th18:
Lm4:
for n being Element of NAT
for g1, g2 being non-decreasing FinSequence of REAL st n = len g1 & g1,g2 are_fiberwise_equipotent holds
g1 = g2
theorem Th19:
:: deftheorem Def6 defines sort_a RFINSEQ2:def 6 :
theorem
theorem
theorem
theorem
theorem Th24:
theorem Th25:
theorem Th26:
theorem Th27:
theorem
theorem
theorem Th30:
theorem Th31:
theorem