let n be Nat; :: thesis: ( S2[n] implies S2[n + 1] )
assume A1: S2[n] ; :: thesis: S2[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 ;
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 ;
then A6: len fn = n by ;
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 ;
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
.= 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))*>) . b1 >= (a ^ <*(R . (n + 1))*>) . (b1 + 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))*>) . b1 >= (a ^ <*(R . (n + 1))*>) . (b1 + 1)
A14: 1 <= m + 1 by ;
set r = (a ^ <*(R . (n + 1))*>) . m;
set s = (a ^ <*(R . (n + 1))*>) . (m + 1);
A15: 1 <= m by ;
A16: m + 1 <= len (a ^ <*(R . (n + 1))*>) by ;
then m <= (n + 1) - 1 by ;
then m in Seg n by ;
then A17: m in dom a by ;
then A18: (a ^ <*(R . (n + 1))*>) . m = a . m by FINSEQ_1:def 7;
A19: a . m in rng a by ;
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))*>) . b1 >= (a ^ <*(R . (n + 1))*>) . (b1 + 1)
then (a ^ <*(R . (n + 1))*>) . (m + 1) = R . (n + 1) by ;
hence (a ^ <*(R . (n + 1))*>) . m >= (a ^ <*(R . (n + 1))*>) . (m + 1) by ; :: thesis: verum
end;
suppose m + 1 <> len b ; :: thesis: (a ^ <*(R . (n + 1))*>) . b1 >= (a ^ <*(R . (n + 1))*>) . (b1 + 1)
then m + 1 < len b by ;
then m + 1 <= (n + 1) - 1 by ;
then m + 1 in Seg n by ;
then A20: m + 1 in dom a by ;
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 ; :: thesis: verum
end;
end;
end;
then reconsider b = a ^ <*(R . (n + 1))*> as non-increasing FinSequence of REAL by ;
take b = b; :: thesis:
fn ^ <*(R . (n + 1))*> = R by A5, A2, Th7;
hence R,b are_fiberwise_equipotent by ; :: 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 S3[ 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 S3[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 ;
reconsider k = k as Element of NAT by ORDINAL1:def 12;
take k ; :: thesis: S3[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 ; :: thesis: verum
end;
consider mi being Nat such that
A27: ( S3[mi] & ( for m being Nat st S3[m] holds
mi <= m ) ) from 1 <= mi by ;
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 ;
then A30: k <= len a by ;
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 ;
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 ;
then A38: 1 <= len (a /^ k) by ;
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 ;
A42: m + 1 <= len (((a | k) ^ <*(R . (n + 1))*>) ^ (a /^ k)) by ;
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 ;
A44: m <= len (((a | k) ^ <*(R . (n + 1))*>) ^ (a /^ k)) by ;
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 ;
A47: dom a = Seg (len a) by FINSEQ_1:def 3;
m <= k by ;
then A48: m in Seg k by ;
1 <= k by ;
then A49: k in dom a by ;
then A50: a . m = (a | k) . m by ;
A51: m + 1 in Seg k by ;
then A52: a . (m + 1) = (a | k) . (m + 1) by ;
A53: (((a | k) ^ <*(R . (n + 1))*>) ^ (a /^ k)) . (m + 1) = ((a | k) ^ <*(R . (n + 1))*>) . (m + 1) by
.= a . (m + 1) by ;
(((a | k) ^ <*(R . (n + 1))*>) ^ (a /^ k)) . m = ((a | k) ^ <*(R . (n + 1))*>) . m by
.= a . m by ;
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 ;
then A56: (((a | k) ^ <*(R . (n + 1))*>) ^ (a /^ k)) . (m + 1) = ((a | k) ^ <*(R . (n + 1))*>) . (k + 1) by
.= R . (n + 1) by ;
A57: m in Seg k by ;
A58: k in dom a by ;
then A59: a . m = (a | k) . m by ;
A60: (((a | k) ^ <*(R . (n + 1))*>) ^ (a /^ k)) . m = ((a | k) ^ <*(R . (n + 1))*>) . m by
.= a . m by ;
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 ;
then mi <= k by ;
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 ;
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 ;
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 ;
l <= l + 1 by NAT_1:11;
then A65: l <= len (a /^ k) by ;
1 <= l + 1 by NAT_1:11;
then A66: l + 1 in dom (a /^ k) by ;
1 <= (l + 1) + k by ;
then A67: (k + l) + 1 <= len a by ;
then A68: (k + l) + 1 in dom a by ;
k + l <= (k + l) + 1 by NAT_1:11;
then A69: k + l <= len a by ;
A70: k + (l + 1) <= len a by ;
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 ;
then A72: (((a | k) ^ <*(R . (n + 1))*>) ^ (a /^ k)) . m = ((a | k) ^ <*(R . (n + 1))*>) . (k + 1) by
.= R . (n + 1) by ;
A73: 1 in dom (a /^ k) by ;
(((a | k) ^ <*(R . (n + 1))*>) ^ (a /^ k)) . (m + 1) = (a /^ k) . (((k + 1) + 1) - (k + 1)) by
.= a . mi by ;
hence (((a | k) ^ <*(R . (n + 1))*>) ^ (a /^ k)) . m >= (((a | k) ^ <*(R . (n + 1))*>) ^ (a /^ k)) . (m + 1) by ; :: 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 ;
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 ;
l <= k + l by NAT_1:11;
then 1 <= k + l by ;
then A77: k + l in dom a by ;
A78: (((a | k) ^ <*(R . (n + 1))*>) ^ (a /^ k)) . m = (a /^ k) . l by
.= a . (k + l) by ;
(((a | k) ^ <*(R . (n + 1))*>) ^ (a /^ k)) . (m + 1) = (a /^ k) . (l + 1) by
.= a . ((k + l) + 1) by ;
hence (((a | k) ^ <*(R . (n + 1))*>) ^ (a /^ k)) . m >= (((a | k) ^ <*(R . (n + 1))*>) ^ (a /^ k)) . (m + 1) by ; :: 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 ;
take b = b; :: thesis:
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
.= 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