let p be FinSequence of REAL ; :: 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:35;
A2: Rev q is non-decreasing FinSequence of REAL

proof

for n being Element of 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 Element of NAT ; :: thesis: ( n in dom (Rev q) & n + 1 in dom (Rev q) implies (Rev q) . n <= (Rev q) . (n + 1) )
assume A3: ( n in dom (Rev q) & n + 1 in dom (Rev q) ) ; :: thesis: (Rev q) . n <= (Rev q) . (n + 1)
(Rev q) . n <= (Rev q) . (n + 1)

proof

set x = (Rev q) . n;
set y = (Rev q) . (n + 1);
A4: (Rev q) . n = q . (((len q) - n) + 1) by A3, FINSEQ_5:def 3;
A5: (Rev q) . (n + 1) = q . (((len q) - (n + 1)) + 1) by A3, FINSEQ_5:def 3;
n in Seg (len (Rev q)) by A3, FINSEQ_1:def 3;
then n in Seg (len q) by FINSEQ_5:def 3;
then n <= len q by FINSEQ_1:3;
then consider m being Nat such that
A6: len q = n + m by NAT_1:10;
reconsider m = m as Element of NAT by ORDINAL1:def 13;
A7: m + 1 = ((len q) - n) + 1 by A6;
A8: ((len q) - n) + 1 in dom q

proof

( 1 <= ((len q) - n) + 1 & ((len q) - n) + 1 <= len q )

proof

thus 1 <= ((len q) - n) + 1 by A6, NAT_1:11; :: thesis: ((len q) - n) + 1 <= len q
n in Seg (len (Rev q)) by A3, FINSEQ_1:def 3;
then 1 <= n by FINSEQ_1:3;
then n - 1 >= 0 by XREAL_1:50;
then (len q) + 0 <= (len q) + (n - 1) by XREAL_1:9;
then (len q) - (n - 1) <= len q by XREAL_1:22;
hence ((len q) - n) + 1 <= len q ; :: thesis: verum

end;

then ((len q) - n) + 1 in Seg (len q) by A7, FINSEQ_1:3;
hence ((len q) - n) + 1 in dom q by FINSEQ_1:def 3; :: thesis: verum

end;

A9: ((len q) - (n + 1)) + 1 = (len q) - n ;
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:3;
then A10: 1 <= ((len q) - (n + 1)) + 1 by A9, XREAL_1:21;
len q <= (len q) + n by NAT_1:11;
then ((len q) - (n + 1)) + 1 <= len q by A9, XREAL_1:22;
then ((len q) - (n + 1)) + 1 in Seg (len q) by A6, A10, FINSEQ_1:3;
then ((len q) - (n + 1)) + 1 in dom q by FINSEQ_1:def 3;
hence (Rev q) . n <= (Rev q) . (n + 1) by A4, A5, A8, RFINSEQ:def 4; :: thesis: verum

end;

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

end;

hence Rev q is non-decreasing FinSequence of REAL by Def1; :: thesis: verum

end;

A11: p, Rev q are_fiberwise_equipotent

proof

defpred S₁[ Element of NAT ] means for p being FinSequence of REAL
for q being non-increasing FinSequence of REAL st len p = $1 & p,q are_fiberwise_equipotent holds
p, Rev q are_fiberwise_equipotent ;
A12: S₁[ 0 ]

proof

let p be FinSequence of REAL ; :: thesis: for q being non-increasing FinSequence of REAL st len p = 0 & p,q are_fiberwise_equipotent holds
p, Rev q are_fiberwise_equipotent
let q be non-increasing FinSequence of REAL ; :: thesis: ( len p = 0 & p,q are_fiberwise_equipotent implies p, Rev q are_fiberwise_equipotent )
assume A13: len p = 0 ; :: thesis: ( not p,q are_fiberwise_equipotent or p, Rev q are_fiberwise_equipotent )
assume A14: p,q are_fiberwise_equipotent ; :: thesis: p, Rev q are_fiberwise_equipotent
p = {} by A13;
then A15: rng p = {} ;
len q = 0 by A13, A14, RFINSEQ:16;
then len (Rev q) = 0 by FINSEQ_5:def 3;
then Rev q = {} ;
then A16: rng (Rev q) = {} ;
for x being set holds card (Coim p,x) = card (Coim (Rev q),x)

proof

let x be set ; :: thesis: card (Coim p,x) = card (Coim (Rev q),x)
card (p " {x}) = 0 by A15, CARD_1:47, FUNCT_1:142;
hence card (Coim p,x) = card (Coim (Rev q),x) by A16, CARD_1:47, FUNCT_1:142; :: thesis: verum

end;

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

end;

A17: for k being Element of NAT st S₁[k] holds
S₁[k + 1]

proof

let k be Element of NAT ; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A18: S₁[k] ; :: thesis: S₁[k + 1]
S₁[k + 1]

proof

let p be FinSequence of REAL ; :: thesis: for q being non-increasing FinSequence of REAL st len p = k + 1 & p,q are_fiberwise_equipotent holds
p, Rev q are_fiberwise_equipotent
let q be non-increasing FinSequence of REAL ; :: thesis: ( len p = k + 1 & p,q are_fiberwise_equipotent implies p, Rev q are_fiberwise_equipotent )
assume A19: len p = k + 1 ; :: thesis: ( not p,q are_fiberwise_equipotent or p, Rev q are_fiberwise_equipotent )
assume A20: p,q are_fiberwise_equipotent ; :: thesis: p, Rev q are_fiberwise_equipotent
consider q1 being non-increasing FinSequence of REAL such that
A21: p,q1 are_fiberwise_equipotent by RFINSEQ:35;
len p = len q1 by A21, RFINSEQ:16;
then A22: len (q1 | k) = k by A19, FINSEQ_1:80, NAT_1:11;
A23: q = q1 by A20, A21, CLASSES1:84, RFINSEQ:36;
reconsider q1k = q1 | k as non-increasing FinSequence of REAL by RFINSEQ:33;
q1 | k, Rev q1k are_fiberwise_equipotent by A18, A22;
then A24: (q1 | k) ^ <*(q1 . (k + 1))*>,(Rev q1k) ^ <*(q1 . (k + 1))*> are_fiberwise_equipotent by RFINSEQ:14;
A25: len q1 = k + 1 by A19, A21, RFINSEQ:16;
then A26: q1,(Rev q1k) ^ <*(q1 . (k + 1))*> are_fiberwise_equipotent by A24, RFINSEQ:20;
(Rev q1k) ^ <*(q1 . (k + 1))*>,<*(q1 . (k + 1))*> ^ (Rev q1k) are_fiberwise_equipotent by RFINSEQ:15;
then A27: q1,<*(q1 . (k + 1))*> ^ (Rev q1k) are_fiberwise_equipotent by A26, CLASSES1:84;
<*(q1 . (k + 1))*> ^ (Rev q1k) = Rev ((q1 | k) ^ <*(q1 . (k + 1))*>) by FINSEQ_5:66
.= Rev q1 by A25, RFINSEQ:20 ;
hence p, Rev q are_fiberwise_equipotent by A21, A23, A27, CLASSES1:84; :: thesis: verum

end;

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

end;

A28: for k being Element of NAT holds S₁[k] from NAT_1:sch 1(A12, A17);
len p = len p ;
hence p, Rev q are_fiberwise_equipotent by A1, A28; :: thesis: verum

end;

reconsider r = Rev q as non-decreasing FinSequence of REAL by A2;
take r ; :: thesis: p,r are_fiberwise_equipotent
thus p,r are_fiberwise_equipotent by A11; :: thesis: verum