let n be Element of NAT ; :: thesis: ( S₂[n] implies S₂[n + 1] )
assume A1: S₂[n] ; :: thesis: S₂[n + 1]
let R be FinSequence of REAL ; :: thesis: ( n + 1 = len R implies ex b being non-increasing FinSequence of REAL st R,b are_fiberwise_equipotent )
set fn = R | (Seg n);
A2: R | (Seg n) = R | n by FINSEQ_1:def 15;
set q = R . (n + 1);
reconsider fn = R | (Seg n) as FinSequence by FINSEQ_1:19;
rng fn c= rng R by RELAT_1:99;
then rng fn c= REAL by XBOOLE_1:1;
then reconsider fn = fn as FinSequence of REAL by FINSEQ_1:def 4;
n <= n + 1 by NAT_1:11;
then A3: ( dom fn = (dom R) /\ (Seg n) & Seg n c= Seg (n + 1) ) by FINSEQ_1:7, RELAT_1:90;
assume A4: n + 1 = len R ; :: thesis: ex b being non-increasing FinSequence of REAL st R,b are_fiberwise_equipotent
then dom R = Seg (n + 1) by FINSEQ_1:def 3;
then dom fn = Seg n by A3, XBOOLE_1:28;
then A5: len fn = n by FINSEQ_1:def 3;
then consider a being non-increasing FinSequence of REAL such that
A6: fn,a are_fiberwise_equipotent by A1;
A7: len fn = len a by A6, Th16;
A8: Seg (len a) = dom a by FINSEQ_1:def 3;

now

per cases ( for t being Real st t in rng a holds
R . (n + 1) <= t or ex t being Real st
( t in rng a & not R . (n + 1) <= t ) ) ;

case A9: for t being Real st t in rng a holds
R . (n + 1) <= t ; :: thesis: ex b being non-increasing FinSequence of REAL st R,b are_fiberwise_equipotent

set b = a ^ <*(R . (n + 1))*>;
A10: len (a ^ <*(R . (n + 1))*>) = n + (len <*(R . (n + 1))*>) by A5, A7, FINSEQ_1:35
.= n + 1 by FINSEQ_1:56 ;

now

let m be Element of NAT ; :: thesis: ( m in dom (a ^ <*(R . (n + 1))*>) & m + 1 in dom (a ^ <*(R . (n + 1))*>) implies (a ^ <*(R . (n + 1))*>) . m >= (a ^ <*(R . (n + 1))*>) . (m + 1) )
assume that
A11: m in dom (a ^ <*(R . (n + 1))*>) and
A12: m + 1 in dom (a ^ <*(R . (n + 1))*>) ; :: thesis: (a ^ <*(R . (n + 1))*>) . m >= (a ^ <*(R . (n + 1))*>) . (m + 1)
A13: 1 <= m + 1 by A12, FINSEQ_3:27;
set r = (a ^ <*(R . (n + 1))*>) . m;
set s = (a ^ <*(R . (n + 1))*>) . (m + 1);
A14: 1 <= m by A11, FINSEQ_3:27;
A15: m + 1 <= len (a ^ <*(R . (n + 1))*>) by A12, FINSEQ_3:27;
then m <= (n + 1) - 1 by A10, XREAL_1:21;
then m in Seg n by A14, FINSEQ_1:3;
then A16: m in dom a by A5, A7, FINSEQ_1:def 3;
then A17: (a ^ <*(R . (n + 1))*>) . m = a . m by FINSEQ_1:def 7;
A18: a . m in rng a by A16, FUNCT_1:def 5;

now

per cases ( m + 1 = len (a ^ <*(R . (n + 1))*>) or m + 1 <> len (a ^ <*(R . (n + 1))*>) ) ;

case m + 1 = len (a ^ <*(R . (n + 1))*>) ; :: thesis: (a ^ <*(R . (n + 1))*>) . m >= (a ^ <*(R . (n + 1))*>) . (m + 1)

then (a ^ <*(R . (n + 1))*>) . (m + 1) = R . (n + 1) by A5, A7, A10, FINSEQ_1:59;
hence (a ^ <*(R . (n + 1))*>) . m >= (a ^ <*(R . (n + 1))*>) . (m + 1) by A9, A17, A18; :: thesis: verum

end;

case m + 1 <> len (a ^ <*(R . (n + 1))*>) ; :: thesis: (a ^ <*(R . (n + 1))*>) . m >= (a ^ <*(R . (n + 1))*>) . (m + 1)

then m + 1 < len (a ^ <*(R . (n + 1))*>) by A15, XXREAL_0:1;
then m + 1 <= (n + 1) - 1 by A10, NAT_1:13;
then m + 1 in Seg n by A13, FINSEQ_1:3;
then A19: m + 1 in dom a by A5, A7, FINSEQ_1:def 3;
then a . (m + 1) = (a ^ <*(R . (n + 1))*>) . (m + 1) by FINSEQ_1:def 7;
hence (a ^ <*(R . (n + 1))*>) . m >= (a ^ <*(R . (n + 1))*>) . (m + 1) by A16, A17, A19, Def4; :: thesis: verum

end;

end;

end;

hence (a ^ <*(R . (n + 1))*>) . m >= (a ^ <*(R . (n + 1))*>) . (m + 1) ; :: thesis: verum

end;

then reconsider b = a ^ <*(R . (n + 1))*> as non-increasing FinSequence of REAL by Def4;
take b = b; :: thesis: R,b are_fiberwise_equipotent
fn ^ <*(R . (n + 1))*> = R by A4, A2, Th20;
hence R,b are_fiberwise_equipotent by A6, Th14; :: thesis: verum

end;

case A20: ex t being Real st
( t in rng a & not R . (n + 1) <= t ) ; :: thesis: ex b being non-increasing FinSequence of REAL st R,b are_fiberwise_equipotent

defpred S₃[ Nat] means ( $1 in dom a & ( for r being Real st r = a . $1 holds
r < R . (n + 1) ) );
A21: ex k being Nat st S₃[k]

proof

consider t being Real such that
A22: t in rng a and
A23: t < R . (n + 1) by A20;
consider k being Nat such that
A24: k in dom a and
A25: a . k = t by A22, FINSEQ_2:11;
reconsider k = k as Element of NAT by ORDINAL1:def 13;
take k ; :: thesis: S₃[k]
thus k in dom a by A24; :: thesis: for r being Real st r = a . k holds
r < R . (n + 1)
let r be Real; :: thesis: ( r = a . k implies r < R . (n + 1) )
assume r = a . k ; :: thesis: r < R . (n + 1)
hence r < R . (n + 1) by A23, A25; :: thesis: verum

end;

consider mi being Nat such that
A26: ( S₃[mi] & ( for m being Nat st S₃[m] holds
mi <= m ) ) from NAT_1:sch 5(A21);
1 <= mi by A26, FINSEQ_3:27;
then max (0,(mi - 1)) = mi - 1 by FINSEQ_2:4;
then reconsider k = mi - 1 as Element of NAT by FINSEQ_2:5;
mi < mi + 1 by NAT_1:13;
then A27: k <= mi by XREAL_1:21;
A28: mi <= len a by A26, FINSEQ_3:27;
then A29: k <= len a by A27, XXREAL_0:2;
then A30: len (a /^ k) = (len a) - k by Def2;
A31: dom ((a | k) ^ <*(R . (n + 1))*>) = Seg (len ((a | k) ^ <*(R . (n + 1))*>)) by FINSEQ_1:def 3;
A32: dom (a | k) c= dom ((a | k) ^ <*(R . (n + 1))*>) by FINSEQ_1:39;
set ak = a /^ k;
set b = ((a | k) ^ <*(R . (n + 1))*>) ^ (a /^ k);
A33: dom (a | k) = Seg (len (a | k)) by FINSEQ_1:def 3;
A34: len (a | k) = k by A28, A27, FINSEQ_1:80, XXREAL_0:2;
then A35: len ((a | k) ^ <*(R . (n + 1))*>) = k + (len <*(R . (n + 1))*>) by FINSEQ_1:35
.= k + 1 by FINSEQ_1:56 ;
then A36: len (((a | k) ^ <*(R . (n + 1))*>) ^ (a /^ k)) = (k + 1) + (len (a /^ k)) by FINSEQ_1:35;
k + 1 <= len a by A26, FINSEQ_3:27;
then A37: 1 <= len (a /^ k) by A30, XREAL_1:21;

now

let m be Element of NAT ; :: thesis: ( m in dom (((a | k) ^ <*(R . (n + 1))*>) ^ (a /^ k)) & m + 1 in dom (((a | k) ^ <*(R . (n + 1))*>) ^ (a /^ k)) implies (((a | k) ^ <*(R . (n + 1))*>) ^ (a /^ k)) . m >= (((a | k) ^ <*(R . (n + 1))*>) ^ (a /^ k)) . (m + 1) )
assume that
A38: m in dom (((a | k) ^ <*(R . (n + 1))*>) ^ (a /^ k)) and
A39: m + 1 in dom (((a | k) ^ <*(R . (n + 1))*>) ^ (a /^ k)) ; :: thesis: (((a | k) ^ <*(R . (n + 1))*>) ^ (a /^ k)) . m >= (((a | k) ^ <*(R . (n + 1))*>) ^ (a /^ k)) . (m + 1)
A40: 1 <= m + 1 by A39, FINSEQ_3:27;
A41: m + 1 <= len (((a | k) ^ <*(R . (n + 1))*>) ^ (a /^ k)) by A39, FINSEQ_3:27;
set r = (((a | k) ^ <*(R . (n + 1))*>) ^ (a /^ k)) . m;
set s = (((a | k) ^ <*(R . (n + 1))*>) ^ (a /^ k)) . (m + 1);
A42: 1 <= m by A38, FINSEQ_3:27;
A43: m <= len (((a | k) ^ <*(R . (n + 1))*>) ^ (a /^ k)) by A38, FINSEQ_3:27;

now

per cases ( m + 1 <= k or k < m + 1 ) ;

case A44: m + 1 <= k ; :: thesis: (((a | k) ^ <*(R . (n + 1))*>) ^ (a /^ k)) . m >= (((a | k) ^ <*(R . (n + 1))*>) ^ (a /^ k)) . (m + 1)

dom (a | k) c= dom ((a | k) ^ (a /^ k)) by FINSEQ_1:39;
then A45: dom (a | k) c= dom a by Th21;
A46: dom a = Seg (len a) by FINSEQ_1:def 3;
m <= k by A44, NAT_1:13;
then A47: m in Seg k by A42, FINSEQ_1:3;
1 <= k by A40, A44, XXREAL_0:2;
then A48: k in dom a by A29, A46, FINSEQ_1:3;
then A49: a . m = (a | k) . m by A47, Th19;
A50: m + 1 in Seg k by A40, A44, FINSEQ_1:3;
then A51: a . (m + 1) = (a | k) . (m + 1) by A48, Th19;
A52: (((a | k) ^ <*(R . (n + 1))*>) ^ (a /^ k)) . (m + 1) = ((a | k) ^ <*(R . (n + 1))*>) . (m + 1) by A34, A33, A32, A50, FINSEQ_1:def 7
.= a . (m + 1) by A34, A33, A50, A51, FINSEQ_1:def 7 ;
(((a | k) ^ <*(R . (n + 1))*>) ^ (a /^ k)) . m = ((a | k) ^ <*(R . (n + 1))*>) . m by A34, A33, A32, A47, FINSEQ_1:def 7
.= a . m by A34, A33, A47, A49, FINSEQ_1:def 7 ;
hence (((a | k) ^ <*(R . (n + 1))*>) ^ (a /^ k)) . m >= (((a | k) ^ <*(R . (n + 1))*>) ^ (a /^ k)) . (m + 1) by A34, A33, A47, A50, A52, A45, Def4; :: thesis: verum

end;

case k < m + 1 ; :: thesis: (((a | k) ^ <*(R . (n + 1))*>) ^ (a /^ k)) . m >= (((a | k) ^ <*(R . (n + 1))*>) ^ (a /^ k)) . (m + 1)

then A53: k <= m by NAT_1:13;

now

per cases ( k = m or k <> m ) ;

case A54: k = m ; :: thesis: (((a | k) ^ <*(R . (n + 1))*>) ^ (a /^ k)) . m >= (((a | k) ^ <*(R . (n + 1))*>) ^ (a /^ k)) . (m + 1)

then m + 1 in dom ((a | k) ^ <*(R . (n + 1))*>) by A35, A31, FINSEQ_1:6;
then A55: (((a | k) ^ <*(R . (n + 1))*>) ^ (a /^ k)) . (m + 1) = ((a | k) ^ <*(R . (n + 1))*>) . (k + 1) by A54, FINSEQ_1:def 7
.= R . (n + 1) by A34, FINSEQ_1:59 ;
A56: m in Seg k by A42, A54, FINSEQ_1:3;
A57: k in dom a by A8, A29, A42, A54, FINSEQ_1:3;
then A58: a . m = (a | k) . m by A56, Th19;
A59: (((a | k) ^ <*(R . (n + 1))*>) ^ (a /^ k)) . m = ((a | k) ^ <*(R . (n + 1))*>) . m by A34, A33, A32, A56, FINSEQ_1:def 7
.= a . m by A34, A33, A56, A58, FINSEQ_1:def 7 ;

now

assume (((a | k) ^ <*(R . (n + 1))*>) ^ (a /^ k)) . (m + 1) > (((a | k) ^ <*(R . (n + 1))*>) ^ (a /^ k)) . m ; :: thesis: contradiction
then for t being Real st t = a . k holds
t < R . (n + 1) by A54, A59, A55;
then mi <= k by A26, A57;
hence contradiction by XREAL_1:46; :: thesis: verum

end;

hence (((a | k) ^ <*(R . (n + 1))*>) ^ (a /^ k)) . m >= (((a | k) ^ <*(R . (n + 1))*>) ^ (a /^ k)) . (m + 1) ; :: thesis: verum

end;

case k <> m ; :: thesis: (((a | k) ^ <*(R . (n + 1))*>) ^ (a /^ k)) . m >= (((a | k) ^ <*(R . (n + 1))*>) ^ (a /^ k)) . (m + 1)

then k < m by A53, XXREAL_0:1;
then A60: k + 1 <= m by NAT_1:13;
then A61: k + 1 < m + 1 by NAT_1:13;
max (0,(m - (k + 1))) = m - (k + 1) by A60, FINSEQ_2:4;
then reconsider l = m - (k + 1) as Element of NAT by FINSEQ_2:5;
A62: l + 1 = (m + 1) - (k + 1) ;
then A63: l + 1 <= (len (((a | k) ^ <*(R . (n + 1))*>) ^ (a /^ k))) - (k + 1) by A41, XREAL_1:15;
l <= l + 1 by NAT_1:11;
then A64: l <= len (a /^ k) by A36, A63, XXREAL_0:2;
1 <= l + 1 by NAT_1:11;
then A65: l + 1 in dom (a /^ k) by A36, A63, FINSEQ_3:27;
1 <= (l + 1) + k by A38, FINSEQ_3:27;
then A66: (k + l) + 1 <= len a by A30, A36, A63, XREAL_1:21;
then A67: (k + l) + 1 in dom a by A42, FINSEQ_3:27;
k + l <= (k + l) + 1 by NAT_1:11;
then A68: k + l <= len a by A66, XXREAL_0:2;
A69: k + (l + 1) <= len a by A30, A36, A63, XREAL_1:21;

now

per cases ( k + 1 = m or k + 1 <> m ) ;

case A70: k + 1 = m ; :: thesis: (((a | k) ^ <*(R . (n + 1))*>) ^ (a /^ k)) . m >= (((a | k) ^ <*(R . (n + 1))*>) ^ (a /^ k)) . (m + 1)

then m in Seg (k + 1) by A42, FINSEQ_1:3;
then A71: (((a | k) ^ <*(R . (n + 1))*>) ^ (a /^ k)) . m = ((a | k) ^ <*(R . (n + 1))*>) . (k + 1) by A35, A31, A70, FINSEQ_1:def 7
.= R . (n + 1) by A34, FINSEQ_1:59 ;
A72: 1 in dom (a /^ k) by A37, FINSEQ_3:27;
(((a | k) ^ <*(R . (n + 1))*>) ^ (a /^ k)) . (m + 1) = (a /^ k) . (((k + 1) + 1) - (k + 1)) by A35, A41, A61, A70, FINSEQ_1:37
.= a . mi by A29, A72, Def2 ;
hence (((a | k) ^ <*(R . (n + 1))*>) ^ (a /^ k)) . m >= (((a | k) ^ <*(R . (n + 1))*>) ^ (a /^ k)) . (m + 1) by A26, A71; :: thesis: verum

end;

case k + 1 <> m ; :: thesis: (((a | k) ^ <*(R . (n + 1))*>) ^ (a /^ k)) . m >= (((a | k) ^ <*(R . (n + 1))*>) ^ (a /^ k)) . (m + 1)

then A73: k + 1 < m by A60, XXREAL_0:1;
then (k + 1) + 1 <= m by NAT_1:13;
then A74: 1 <= l by XREAL_1:21;
then A75: l in dom (a /^ k) by A64, FINSEQ_3:27;
l <= k + l by NAT_1:11;
then 1 <= k + l by A74, XXREAL_0:2;
then A76: k + l in dom a by A68, FINSEQ_3:27;
A77: (((a | k) ^ <*(R . (n + 1))*>) ^ (a /^ k)) . m = (a /^ k) . l by A35, A43, A73, FINSEQ_1:37
.= a . (k + l) by A29, A75, Def2 ;
(((a | k) ^ <*(R . (n + 1))*>) ^ (a /^ k)) . (m + 1) = (a /^ k) . (l + 1) by A35, A41, A61, A62, FINSEQ_1:37
.= a . ((k + l) + 1) by A29, A65, A69, Def2 ;
hence (((a | k) ^ <*(R . (n + 1))*>) ^ (a /^ k)) . m >= (((a | k) ^ <*(R . (n + 1))*>) ^ (a /^ k)) . (m + 1) by A67, A77, A76, Def4; :: thesis: verum

end;

end;

end;

hence (((a | k) ^ <*(R . (n + 1))*>) ^ (a /^ k)) . m >= (((a | k) ^ <*(R . (n + 1))*>) ^ (a /^ k)) . (m + 1) ; :: thesis: verum

end;

end;

end;

hence (((a | k) ^ <*(R . (n + 1))*>) ^ (a /^ k)) . m >= (((a | k) ^ <*(R . (n + 1))*>) ^ (a /^ k)) . (m + 1) ; :: thesis: verum

end;

end;

end;

hence (((a | k) ^ <*(R . (n + 1))*>) ^ (a /^ k)) . m >= (((a | k) ^ <*(R . (n + 1))*>) ^ (a /^ k)) . (m + 1) ; :: thesis: verum

end;

then reconsider b = ((a | k) ^ <*(R . (n + 1))*>) ^ (a /^ k) as non-increasing FinSequence of REAL by Def4;
take b = b; :: thesis: R,b are_fiberwise_equipotent

now

let x be set ; :: thesis: card (Coim (b,x)) = card (Coim (R,x))
A78: card (Coim (fn,x)) = card (Coim (a,x)) by A6, CLASSES1:def 9;
thus card (Coim (b,x)) = (card (((a | k) ^ <*(R . (n + 1))*>) " {x})) + (card ((a /^ k) " {x})) by FINSEQ_3:63
.= ((card ((a | k) " {x})) + (card (<*(R . (n + 1))*> " {x}))) + (card ((a /^ k) " {x})) by FINSEQ_3:63
.= ((card ((a | k) " {x})) + (card ((a /^ k) " {x}))) + (card (<*(R . (n + 1))*> " {x}))
.= (card (((a | k) ^ (a /^ k)) " {x})) + (card (<*(R . (n + 1))*> " {x})) by FINSEQ_3:63
.= (card (fn " {x})) + (card (<*(R . (n + 1))*> " {x})) by A78, Th21
.= card ((fn ^ <*(R . (n + 1))*>) " {x}) by FINSEQ_3:63
.= card (Coim (R,x)) by A4, A2, Th20 ; :: thesis: verum

end;

hence R,b are_fiberwise_equipotent by CLASSES1:def 9; :: thesis: verum

end;

end;

end;

hence ex b being non-increasing FinSequence of REAL st R,b are_fiberwise_equipotent ; :: thesis: verum