let n be 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:15;
rng fn c= rng R by RELAT_1:70;
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:5, RELAT_1:61;
A4: n in NAT by ORDINAL1:def 12;
assume A5: 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 A6: len fn = n by FINSEQ_1:def 3, A4;
then consider a being non-increasing FinSequence of REAL such that
A7: fn,a are_fiberwise_equipotent by A1;
A8: len fn = len a by A7, Th3;
A9: Seg (len a) = dom a by FINSEQ_1:def 3;

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

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 A10: 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))*>;
A11: len (a ^ <*(R . (n + 1))*>) = n + (len <*(R . (n + 1))*>) by A6, A8, FINSEQ_1:22
.= n + 1 by FINSEQ_1:39 ;

now :: thesis: for m being Nat st m in dom (a ^ <*(R . (n + 1))*>) & m + 1 in dom (a ^ <*(R . (n + 1))*>) holds
(a ^ <*(R . (n + 1))*>) . m >= (a ^ <*(R . (n + 1))*>) . (m + 1)

let m be Nat; :: thesis: ( m in dom (a ^ <*(R . (n + 1))*>) & m + 1 in dom (a ^ <*(R . (n + 1))*>) implies (a ^ <*(R . (n + 1))*>) . b₁ >= (a ^ <*(R . (n + 1))*>) . (b₁ + 1) )
assume that
A12: m in dom (a ^ <*(R . (n + 1))*>) and
A13: m + 1 in dom (a ^ <*(R . (n + 1))*>) ; :: thesis: (a ^ <*(R . (n + 1))*>) . b₁ >= (a ^ <*(R . (n + 1))*>) . (b₁ + 1)
A14: 1 <= m + 1 by A13, FINSEQ_3:25;
set r = (a ^ <*(R . (n + 1))*>) . m;
set s = (a ^ <*(R . (n + 1))*>) . (m + 1);
A15: 1 <= m by A12, FINSEQ_3:25;
A16: m + 1 <= len (a ^ <*(R . (n + 1))*>) by A13, FINSEQ_3:25;
then m <= (n + 1) - 1 by A11, XREAL_1:19;
then m in Seg n by A15, FINSEQ_1:1;
then A17: m in dom a by A6, A8, FINSEQ_1:def 3;
then A18: (a ^ <*(R . (n + 1))*>) . m = a . m by FINSEQ_1:def 7;
A19: a . m in rng a by A17, FUNCT_1:def 3;
reconsider b = a ^ <*(R . (n + 1))*> as FinSequence of REAL by RVSUM_1:145;

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

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

then (a ^ <*(R . (n + 1))*>) . (m + 1) = R . (n + 1) by A6, A8, A11, FINSEQ_1:42;
hence (a ^ <*(R . (n + 1))*>) . m >= (a ^ <*(R . (n + 1))*>) . (m + 1) by A10, A18, A19; :: thesis: verum

end;

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

then m + 1 < len b by A16, XXREAL_0:1;
then m + 1 <= (n + 1) - 1 by A11, NAT_1:13;
then m + 1 in Seg n by A14, FINSEQ_1:1;
then A20: m + 1 in dom a by A6, A8, 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 A17, A18, A20, Def3; :: thesis: verum

end;

end;

end;

then reconsider b = a ^ <*(R . (n + 1))*> as non-increasing FinSequence of REAL by Def3, RVSUM_1:145;
take b = b; :: thesis: R,b are_fiberwise_equipotent
fn ^ <*(R . (n + 1))*> = R by A5, A2, Th7;
hence R,b are_fiberwise_equipotent by A7, Th1; :: thesis: verum

end;

case A21: 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) ) );
A22: ex k being Nat st S₃[k]

proof

consider t being Real such that
A23: t in rng a and
A24: t < R . (n + 1) by A21;
consider k being Nat such that
A25: k in dom a and
A26: a . k = t by A23, FINSEQ_2:10;
reconsider k = k as Element of NAT by ORDINAL1:def 12;
take k ; :: thesis: S₃[k]
thus k in dom a by A25; :: 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 A24, A26; :: thesis: verum

end;

consider mi being Nat such that
A27: ( S₃[mi] & ( for m being Nat st S₃[m] holds
mi <= m ) ) from NAT_1:sch 5(A22);
1 <= mi by A27, FINSEQ_3:25;
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 A28: k <= mi by XREAL_1:19;
A29: mi <= len a by A27, FINSEQ_3:25;
then A30: k <= len a by A28, XXREAL_0:2;
then A31: len (a /^ k) = (len a) - k by Def1;
A32: dom ((a | k) ^ <*(R . (n + 1))*>) = Seg (len ((a | k) ^ <*(R . (n + 1))*>)) by FINSEQ_1:def 3;
A33: dom (a | k) c= dom ((a | k) ^ <*(R . (n + 1))*>) by FINSEQ_1:26;
set ak = a /^ k;
set b = ((a | k) ^ <*(R . (n + 1))*>) ^ (a /^ k);
A34: dom (a | k) = Seg (len (a | k)) by FINSEQ_1:def 3;
A35: len (a | k) = k by A29, A28, FINSEQ_1:59, XXREAL_0:2;
then A36: len ((a | k) ^ <*(R . (n + 1))*>) = k + (len <*(R . (n + 1))*>) by FINSEQ_1:22
.= k + 1 by FINSEQ_1:39 ;
then A37: len (((a | k) ^ <*(R . (n + 1))*>) ^ (a /^ k)) = (k + 1) + (len (a /^ k)) by FINSEQ_1:22;
k + 1 <= len a by A27, FINSEQ_3:25;
then A38: 1 <= len (a /^ k) by A31, XREAL_1:19;

now :: thesis: for m being Nat st m in dom (((a | k) ^ <*(R . (n + 1))*>) ^ (a /^ k)) & m + 1 in dom (((a | k) ^ <*(R . (n + 1))*>) ^ (a /^ k)) holds
(((a | k) ^ <*(R . (n + 1))*>) ^ (a /^ k)) . m >= (((a | k) ^ <*(R . (n + 1))*>) ^ (a /^ k)) . (m + 1)

let m be 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
A39: m in dom (((a | k) ^ <*(R . (n + 1))*>) ^ (a /^ k)) and
A40: 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)
A41: 1 <= m + 1 by A40, FINSEQ_3:25;
A42: m + 1 <= len (((a | k) ^ <*(R . (n + 1))*>) ^ (a /^ k)) by A40, FINSEQ_3:25;
set r = (((a | k) ^ <*(R . (n + 1))*>) ^ (a /^ k)) . m;
set s = (((a | k) ^ <*(R . (n + 1))*>) ^ (a /^ k)) . (m + 1);
A43: 1 <= m by A39, FINSEQ_3:25;
A44: m <= len (((a | k) ^ <*(R . (n + 1))*>) ^ (a /^ k)) by A39, FINSEQ_3:25;

now :: thesis: ( ( m + 1 <= k & (((a | k) ^ <*(R . (n + 1))*>) ^ (a /^ k)) . m >= (((a | k) ^ <*(R . (n + 1))*>) ^ (a /^ k)) . (m + 1) ) or ( k < m + 1 & (((a | k) ^ <*(R . (n + 1))*>) ^ (a /^ k)) . m >= (((a | k) ^ <*(R . (n + 1))*>) ^ (a /^ k)) . (m + 1) ) )

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

case A45: 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:26;
then A46: dom (a | k) c= dom a by Th8;
A47: dom a = Seg (len a) by FINSEQ_1:def 3;
m <= k by A45, NAT_1:13;
then A48: m in Seg k by A43, FINSEQ_1:1;
1 <= k by A41, A45, XXREAL_0:2;
then A49: k in dom a by A30, A47, FINSEQ_1:1;
then A50: a . m = (a | k) . m by A48, Th6;
A51: m + 1 in Seg k by A41, A45, FINSEQ_1:1;
then A52: a . (m + 1) = (a | k) . (m + 1) by A49, Th6;
A53: (((a | k) ^ <*(R . (n + 1))*>) ^ (a /^ k)) . (m + 1) = ((a | k) ^ <*(R . (n + 1))*>) . (m + 1) by A35, A34, A33, A51, FINSEQ_1:def 7
.= a . (m + 1) by A35, A34, A51, A52, FINSEQ_1:def 7 ;
(((a | k) ^ <*(R . (n + 1))*>) ^ (a /^ k)) . m = ((a | k) ^ <*(R . (n + 1))*>) . m by A35, A34, A33, A48, FINSEQ_1:def 7
.= a . m by A35, A34, A48, A50, FINSEQ_1:def 7 ;
hence (((a | k) ^ <*(R . (n + 1))*>) ^ (a /^ k)) . m >= (((a | k) ^ <*(R . (n + 1))*>) ^ (a /^ k)) . (m + 1) by A35, A34, A48, A51, A53, A46, Def3; :: 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 A54: k <= m by NAT_1:13;

now :: thesis: ( ( k = m & (((a | k) ^ <*(R . (n + 1))*>) ^ (a /^ k)) . m >= (((a | k) ^ <*(R . (n + 1))*>) ^ (a /^ k)) . (m + 1) ) or ( k <> m & (((a | k) ^ <*(R . (n + 1))*>) ^ (a /^ k)) . m >= (((a | k) ^ <*(R . (n + 1))*>) ^ (a /^ k)) . (m + 1) ) )

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

case A55: 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 A36, A32, FINSEQ_1:4;
then A56: (((a | k) ^ <*(R . (n + 1))*>) ^ (a /^ k)) . (m + 1) = ((a | k) ^ <*(R . (n + 1))*>) . (k + 1) by A55, FINSEQ_1:def 7
.= R . (n + 1) by A35, FINSEQ_1:42 ;
A57: m in Seg k by A43, A55, FINSEQ_1:1;
A58: k in dom a by A9, A30, A43, A55, FINSEQ_1:1;
then A59: a . m = (a | k) . m by A57, Th6;
A60: (((a | k) ^ <*(R . (n + 1))*>) ^ (a /^ k)) . m = ((a | k) ^ <*(R . (n + 1))*>) . m by A35, A34, A33, A57, FINSEQ_1:def 7
.= a . m by A35, A34, A57, A59, FINSEQ_1:def 7 ;

now :: thesis: not (((a | k) ^ <*(R . (n + 1))*>) ^ (a /^ k)) . (m + 1) > (((a | k) ^ <*(R . (n + 1))*>) ^ (a /^ k)) . m

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 A55, A60, A56;
then mi <= k by A27, A58;
hence contradiction by XREAL_1:44; :: 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 A54, XXREAL_0:1;
then A61: k + 1 <= m by NAT_1:13;
then A62: k + 1 < m + 1 by NAT_1:13;
max (0,(m - (k + 1))) = m - (k + 1) by A61, FINSEQ_2:4;
then reconsider l = m - (k + 1) as Element of NAT by FINSEQ_2:5;
A63: l + 1 = (m + 1) - (k + 1) ;
then A64: l + 1 <= (len (((a | k) ^ <*(R . (n + 1))*>) ^ (a /^ k))) - (k + 1) by A42, XREAL_1:13;
l <= l + 1 by NAT_1:11;
then A65: l <= len (a /^ k) by A37, A64, XXREAL_0:2;
1 <= l + 1 by NAT_1:11;
then A66: l + 1 in dom (a /^ k) by A37, A64, FINSEQ_3:25;
1 <= (l + 1) + k by A39, FINSEQ_3:25;
then A67: (k + l) + 1 <= len a by A31, A37, A64, XREAL_1:19;
then A68: (k + l) + 1 in dom a by A43, FINSEQ_3:25;
k + l <= (k + l) + 1 by NAT_1:11;
then A69: k + l <= len a by A67, XXREAL_0:2;
A70: k + (l + 1) <= len a by A31, A37, A64, XREAL_1:19;

now :: thesis: ( ( k + 1 = m & (((a | k) ^ <*(R . (n + 1))*>) ^ (a /^ k)) . m >= (((a | k) ^ <*(R . (n + 1))*>) ^ (a /^ k)) . (m + 1) ) or ( k + 1 <> m & (((a | k) ^ <*(R . (n + 1))*>) ^ (a /^ k)) . m >= (((a | k) ^ <*(R . (n + 1))*>) ^ (a /^ k)) . (m + 1) ) )

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

case A71: 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 A43, FINSEQ_1:1;
then A72: (((a | k) ^ <*(R . (n + 1))*>) ^ (a /^ k)) . m = ((a | k) ^ <*(R . (n + 1))*>) . (k + 1) by A36, A32, A71, FINSEQ_1:def 7
.= R . (n + 1) by A35, FINSEQ_1:42 ;
A73: 1 in dom (a /^ k) by A38, FINSEQ_3:25;
(((a | k) ^ <*(R . (n + 1))*>) ^ (a /^ k)) . (m + 1) = (a /^ k) . (((k + 1) + 1) - (k + 1)) by A36, A42, A62, A71, FINSEQ_1:24
.= a . mi by A30, A73, Def1 ;
hence (((a | k) ^ <*(R . (n + 1))*>) ^ (a /^ k)) . m >= (((a | k) ^ <*(R . (n + 1))*>) ^ (a /^ k)) . (m + 1) by A27, A72; :: 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 A74: k + 1 < m by A61, XXREAL_0:1;
then (k + 1) + 1 <= m by NAT_1:13;
then A75: 1 <= l by XREAL_1:19;
then A76: l in dom (a /^ k) by A65, FINSEQ_3:25;
l <= k + l by NAT_1:11;
then 1 <= k + l by A75, XXREAL_0:2;
then A77: k + l in dom a by A69, FINSEQ_3:25;
A78: (((a | k) ^ <*(R . (n + 1))*>) ^ (a /^ k)) . m = (a /^ k) . l by A36, A44, A74, FINSEQ_1:24
.= a . (k + l) by A30, A76, Def1 ;
(((a | k) ^ <*(R . (n + 1))*>) ^ (a /^ k)) . (m + 1) = (a /^ k) . (l + 1) by A36, A42, A62, A63, FINSEQ_1:24
.= a . ((k + l) + 1) by A30, A66, A70, Def1 ;
hence (((a | k) ^ <*(R . (n + 1))*>) ^ (a /^ k)) . m >= (((a | k) ^ <*(R . (n + 1))*>) ^ (a /^ k)) . (m + 1) by A68, A78, A77, Def3; :: 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 Def3, RVSUM_1:145;
take b = b; :: thesis: R,b are_fiberwise_equipotent

now :: thesis: for x being object holds card (Coim (b,x)) = card (Coim (R,x))

let x be object ; :: thesis: card (Coim (b,x)) = card (Coim (R,x))
A79: card (Coim (fn,x)) = card (Coim (a,x)) by A7;
thus card (Coim (b,x)) = (card (((a | k) ^ <*(R . (n + 1))*>) " {x})) + (card ((a /^ k) " {x})) by FINSEQ_3:57
.= ((card ((a | k) " {x})) + (card (<*(R . (n + 1))*> " {x}))) + (card ((a /^ k) " {x})) by FINSEQ_3:57
.= ((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:57
.= (card (fn " {x})) + (card (<*(R . (n + 1))*> " {x})) by A79, Th8
.= card ((fn ^ <*(R . (n + 1))*>) " {x}) by FINSEQ_3:57
.= card (Coim (R,x)) by A5, A2, Th7 ; :: thesis: verum

end;

hence R,b are_fiberwise_equipotent ; :: thesis: verum

end;

end;

end;

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