let p be real-valued FinSequence; :: thesis: ex q being non-decreasing FinSequence of REAL st p,q are_fiberwise_equipotent
consider q being non-increasing FinSequence of REAL such that
A1: p,q are_fiberwise_equipotent by RFINSEQ:22;
for n being Nat st n in dom (Rev q) & n + 1 in dom (Rev q) holds
(Rev q) . n <= (Rev q) . (n + 1)

proof

let n be Nat; :: thesis: ( n in dom (Rev q) & n + 1 in dom (Rev q) implies (Rev q) . n <= (Rev q) . (n + 1) )
assume that
A2: n in dom (Rev q) and
A3: n + 1 in dom (Rev q) ; :: thesis: (Rev q) . n <= (Rev q) . (n + 1)
(Rev q) . n <= (Rev q) . (n + 1)

proof

n in Seg (len (Rev q)) by A2, FINSEQ_1:def 3;
then 1 <= n by FINSEQ_1:1;
then n - 1 >= 0 by XREAL_1:48;
then (len q) + 0 <= (len q) + (n - 1) by XREAL_1:7;
then A4: (len q) - (n - 1) <= len q by XREAL_1:20;
n in Seg (len (Rev q)) by A2, FINSEQ_1:def 3;
then n in Seg (len q) by FINSEQ_5:def 3;
then n <= len q by FINSEQ_1:1;
then consider m being Nat such that
A5: len q = n + m by NAT_1:10;
reconsider m = m as Nat ;
( m + 1 = ((len q) - n) + 1 & 1 <= ((len q) - n) + 1 ) by A5, NAT_1:11;
then ((len q) - n) + 1 in Seg (len q) by A4, FINSEQ_1:1;
then A6: ((len q) - n) + 1 in dom q by FINSEQ_1:def 3;
set x = (Rev q) . n;
set y = (Rev q) . (n + 1);
A7: ((len q) - (n + 1)) + 1 = (len q) - n ;
len q <= (len q) + n by NAT_1:11;
then A8: ((len q) - (n + 1)) + 1 <= len q by A7, XREAL_1:20;
n + 1 in Seg (len (Rev q)) by A3, FINSEQ_1:def 3;
then n + 1 in Seg (len q) by FINSEQ_5:def 3;
then n + 1 <= len q by FINSEQ_1:1;
then 1 <= ((len q) - (n + 1)) + 1 by A7, XREAL_1:19;
then ((len q) - (n + 1)) + 1 in Seg (len q) by A5, A8, FINSEQ_1:1;
then A9: ((len q) - (n + 1)) + 1 in dom q by FINSEQ_1:def 3;
( (Rev q) . n = q . (((len q) - n) + 1) & (Rev q) . (n + 1) = q . (((len q) - (n + 1)) + 1) ) by A2, A3, FINSEQ_5:def 3;
hence (Rev q) . n <= (Rev q) . (n + 1) by A6, A9, RFINSEQ:def 3; :: thesis: verum

end;

hence (Rev q) . n <= (Rev q) . (n + 1) ; :: thesis: verum

end;

then reconsider r = Rev q as non-decreasing FinSequence of REAL by Def1;
take r ; :: thesis: p,r are_fiberwise_equipotent
p, Rev q are_fiberwise_equipotent

proof

defpred S₁[ Nat] means for p being real-valued FinSequence
for q being real-valued non-increasing FinSequence st len p = $1 & p,q are_fiberwise_equipotent holds
p, Rev q are_fiberwise_equipotent ;
A10: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A11: S₁[k] ; :: thesis: S₁[k + 1]
S₁[k + 1]

proof

let p be real-valued FinSequence; :: thesis: for q being real-valued non-increasing FinSequence st len p = k + 1 & p,q are_fiberwise_equipotent holds
p, Rev q are_fiberwise_equipotent
let q be real-valued non-increasing FinSequence; :: thesis: ( len p = k + 1 & p,q are_fiberwise_equipotent implies p, Rev q are_fiberwise_equipotent )
consider q1 being non-increasing FinSequence of REAL such that
A12: p,q1 are_fiberwise_equipotent by RFINSEQ:22;
reconsider kk = k as Element of NAT by ORDINAL1:def 12;
reconsider q1k = q1 | kk as non-increasing FinSequence of REAL by RFINSEQ:20;
A13: (Rev q1k) ^ <*(q1 . (k + 1))*>,<*(q1 . (k + 1))*> ^ (Rev q1k) are_fiberwise_equipotent by RFINSEQ:2;
assume A14: len p = k + 1 ; :: thesis: ( not p,q are_fiberwise_equipotent or p, Rev q are_fiberwise_equipotent )
then A15: len q1 = k + 1 by A12, RFINSEQ:3;
len p = len q1 by A12, RFINSEQ:3;
then len (q1 | k) = k by A14, FINSEQ_1:59, NAT_1:11;
then q1 | k, Rev q1k are_fiberwise_equipotent by A11;
then (q1 | k) ^ <*(q1 . (k + 1))*>,(Rev q1k) ^ <*(q1 . (k + 1))*> are_fiberwise_equipotent by RFINSEQ:1;
then q1,(Rev q1k) ^ <*(q1 . (k + 1))*> are_fiberwise_equipotent by A15, RFINSEQ:7;
then A16: q1,<*(q1 . (k + 1))*> ^ (Rev q1k) are_fiberwise_equipotent by A13, CLASSES1:76;
A17: <*(q1 . (k + 1))*> ^ (Rev q1k) = Rev ((q1 | k) ^ <*(q1 . (k + 1))*>) by FINSEQ_5:63
.= Rev q1 by A15, RFINSEQ:7 ;
assume p,q are_fiberwise_equipotent ; :: thesis: p, Rev q are_fiberwise_equipotent
then q = q1 by A12, CLASSES1:76, RFINSEQ:23;
hence p, Rev q are_fiberwise_equipotent by A12, A16, A17, CLASSES1:76; :: thesis: verum

end;

hence S₁[k + 1] ; :: thesis: verum

end;

A18: len p = len p ;
A19: S₁[ 0 ]

proof

let p be real-valued FinSequence; :: thesis: for q being real-valued non-increasing FinSequence st len p = 0 & p,q are_fiberwise_equipotent holds
p, Rev q are_fiberwise_equipotent
let q be real-valued non-increasing FinSequence; :: thesis: ( len p = 0 & p,q are_fiberwise_equipotent implies p, Rev q are_fiberwise_equipotent )
assume A20: len p = 0 ; :: thesis: ( not p,q are_fiberwise_equipotent or p, Rev q are_fiberwise_equipotent )
assume p,q are_fiberwise_equipotent ; :: thesis: p, Rev q are_fiberwise_equipotent
then len q = 0 by A20, RFINSEQ:3;
then len (Rev q) = 0 by FINSEQ_5:def 3;
then Rev q = {} ;
then A21: rng (Rev q) = {} ;
p = {} by A20;
then A22: rng p = {} ;
for x being object holds card (Coim (p,x)) = card (Coim ((Rev q),x))

proof

let x be object ; :: thesis: card (Coim (p,x)) = card (Coim ((Rev q),x))
card (p " {x}) = 0 by A22, CARD_1:27, FUNCT_1:72;
hence card (Coim (p,x)) = card (Coim ((Rev q),x)) by A21, CARD_1:27, FUNCT_1:72; :: thesis: verum

end;

hence p, Rev q are_fiberwise_equipotent by CLASSES1:def 10; :: thesis: verum

end;

for k being Nat holds S₁[k] from NAT_1:sch 2(A19, A10);
hence p, Rev q are_fiberwise_equipotent by A1, A18; :: thesis: verum

end;

hence p,r are_fiberwise_equipotent ; :: thesis: verum