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