defpred S2[ Nat] means for f, g being FinSequence of REAL st f,g are_fiberwise_equipotent & len f = $1 holds
Sum f = Sum g;
A1:
S2[ 0 ]
A2:
for n being Element of NAT st S2[n] holds
S2[n + 1]
proof
let n be
Element of
NAT ;
:: thesis: ( S2[n] implies S2[n + 1] )
assume A3:
S2[
n]
;
:: thesis: S2[n + 1]
let f,
g be
FinSequence of
REAL ;
:: thesis: ( f,g are_fiberwise_equipotent & len f = n + 1 implies Sum f = Sum g )
assume A4:
(
f,
g are_fiberwise_equipotent &
len f = n + 1 )
;
:: thesis: Sum f = Sum g
then A5:
(
rng f = rng g &
len f = len g )
by Th16, CLASSES1:83;
0 < n + 1
by NAT_1:3;
then
0 + 1
<= n + 1
by NAT_1:13;
then A6:
n + 1
in dom f
by A4, FINSEQ_3:27;
set a =
f . (n + 1);
f . (n + 1) in rng g
by A5, A6, FUNCT_1:def 5;
then consider m being
Nat such that A7:
(
m in dom g &
g . m = f . (n + 1) )
by FINSEQ_2:11;
A8:
g = (g | m) ^ (g /^ m)
by Th21;
A9:
( 1
<= m &
m <= len g )
by A7, FINSEQ_3:27;
then
max 0 ,
(m - 1) = m - 1
by FINSEQ_2:4;
then reconsider m1 =
m - 1 as
Element of
NAT by FINSEQ_2:5;
set gg =
g /^ m;
set gm =
g | m;
A10:
len (g | m) = m
by A9, FINSEQ_1:80;
A11:
m = m1 + 1
;
m in Seg m
by A9, FINSEQ_1:3;
then
(
(g | m) . m = f . (n + 1) &
m in dom g )
by A7, Th19;
then A12:
g | m = ((g | m) | m1) ^ <*(f . (n + 1))*>
by A10, A11, Th20;
m1 <= m
by A11, NAT_1:11;
then A13:
Seg m1 c= Seg m
by FINSEQ_1:7;
A14:
(g | m) | m1 =
(g | m) | (Seg m1)
by FINSEQ_1:def 15
.=
(g | (Seg m)) | (Seg m1)
by FINSEQ_1:def 15
.=
g | ((Seg m) /\ (Seg m1))
by RELAT_1:100
.=
g | (Seg m1)
by A13, XBOOLE_1:28
.=
g | m1
by FINSEQ_1:def 15
;
set fn =
f | n;
A15:
len (f | n) = n
by A4, FINSEQ_1:80, NAT_1:11;
A16:
f = (f | n) ^ <*(f . (n + 1))*>
by A4, Th20;
now let x be
set ;
:: thesis: card (Coim (f | n),x) = card (Coim ((g | m1) ^ (g /^ m)),x)
card (Coim f,x) = card (Coim g,x)
by A4, CLASSES1:def 9;
then (card ((f | n) " {x})) + (card (<*(f . (n + 1))*> " {x})) =
card ((((g | m1) ^ <*(f . (n + 1))*>) ^ (g /^ m)) " {x})
by A8, A12, A14, A16, FINSEQ_3:63
.=
(card (((g | m1) ^ <*(f . (n + 1))*>) " {x})) + (card ((g /^ m) " {x}))
by FINSEQ_3:63
.=
((card ((g | m1) " {x})) + (card (<*(f . (n + 1))*> " {x}))) + (card ((g /^ m) " {x}))
by FINSEQ_3:63
.=
((card ((g | m1) " {x})) + (card ((g /^ m) " {x}))) + (card (<*(f . (n + 1))*> " {x}))
.=
(card (((g | m1) ^ (g /^ m)) " {x})) + (card (<*(f . (n + 1))*> " {x}))
by FINSEQ_3:63
;
hence
card (Coim (f | n),x) = card (Coim ((g | m1) ^ (g /^ m)),x)
;
:: thesis: verum end;
then
f | n,
(g | m1) ^ (g /^ m) are_fiberwise_equipotent
by CLASSES1:def 9;
then
Sum (f | n) = Sum ((g | m1) ^ (g /^ m))
by A3, A15;
hence Sum f =
(Sum ((g | m1) ^ (g /^ m))) + (Sum <*(f . (n + 1))*>)
by A16, RVSUM_1:105
.=
((Sum (g | m1)) + (Sum (g /^ m))) + (Sum <*(f . (n + 1))*>)
by RVSUM_1:105
.=
((Sum (g | m1)) + (Sum <*(f . (n + 1))*>)) + (Sum (g /^ m))
.=
(Sum (g | m)) + (Sum (g /^ m))
by A12, A14, RVSUM_1:105
.=
Sum g
by A8, RVSUM_1:105
;
:: thesis: verum
end;
A17:
for n being Element of NAT holds S2[n]
from NAT_1:sch 1(A1, A2);
let R1, R2 be FinSequence of REAL ; :: thesis: ( R1,R2 are_fiberwise_equipotent implies Sum R1 = Sum R2 )
assume A18:
R1,R2 are_fiberwise_equipotent
; :: thesis: Sum R1 = Sum R2
len R1 = len R1
;
hence
Sum R1 = Sum R2
by A17, A18; :: thesis: verum