let R1, R2 be V339() FinSequence of ExtREAL ; ( R1,R2 are_fiberwise_equipotent implies Sum R1 = Sum R2 )
defpred S1[ Nat] means for f, g being V339() FinSequence of ExtREAL st f,g are_fiberwise_equipotent & len f = $1 holds
Sum f = Sum g;
assume A1:
R1,R2 are_fiberwise_equipotent
; Sum R1 = Sum R2
A2:
len R1 = len R1
;
A3:
for n being Nat st S1[n] holds
S1[n + 1]
proof
let n be
Nat;
( S1[n] implies S1[n + 1] )
assume A4:
S1[
n]
;
S1[n + 1]
let f,
g be
V339()
FinSequence of
ExtREAL ;
( f,g are_fiberwise_equipotent & len f = n + 1 implies Sum f = Sum g )
assume that A5:
f,
g are_fiberwise_equipotent
and A6:
len f = n + 1
;
Sum f = Sum g
set a =
f . (n + 1);
A7:
rng f = rng g
by A5, CLASSES1:75;
0 + 1
<= n + 1
by NAT_1:13;
then
n + 1
in dom f
by A6, FINSEQ_3:25;
then A8:
f . (n + 1) in rng g
by A7, FUNCT_1:def 3;
then consider m being
Nat such that A9:
m in dom g
and A10:
g . m = f . (n + 1)
by FINSEQ_2:10;
set gg =
g /^ m;
set gm =
g | m;
m <= len g
by A9, FINSEQ_3:25;
then A11:
len (g | m) = m
by FINSEQ_1:59;
A12:
1
<= m
by A9, FINSEQ_3:25;
max (
0,
(m - 1))
= m - 1
by A9, FINSEQ_3:25, FINSEQ_2:4;
then reconsider m1 =
m - 1 as
Element of
NAT by FINSEQ_2:5;
A13:
m = m1 + 1
;
then A14:
Seg m1 c= Seg m
by FINSEQ_1:5, NAT_1:11;
m in Seg m
by A12, FINSEQ_1:1;
then
(g | m) . m = f . (n + 1)
by A9, A10, RFINSEQ:6;
then A15:
g | m = ((g | m) | m1) ^ <*(f . (n + 1))*>
by A11, A13, RFINSEQ:7;
set fn =
f | n;
A16:
g = (g | m) ^ (g /^ m)
;
A17:
(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:71
.=
g | (Seg m1)
by A14, XBOOLE_1:28
.=
g | m1
by FINSEQ_1:def 15
;
A18:
f = (f | n) ^ <*(f . (n + 1))*>
by A6, RFINSEQ:7;
A19:
(
f | n is
V339() &
g | m1 is
V339() &
g /^ m is
V339() &
g | m is
V339() &
g /^ m is
V339() )
by MEASURE9:36, Th65;
then A20:
(
(g | m1) ^ (g /^ m) is
V339() &
(g | m1) ^ (g /^ m) is
V339() )
by Th64;
f . (n + 1) <> -infty
by A8, MESFUNC5:def 3;
then
not
-infty in {(f . (n + 1))}
by TARSKI:def 1;
then A21:
not
-infty in rng <*(f . (n + 1))*>
by FINSEQ_1:38;
then A22:
<*(f . (n + 1))*> is
V339()
FinSequence of
ExtREAL
by MESFUNC5:def 3;
A23:
( not
-infty in rng (f | n) & not
-infty in rng ((g | m1) ^ (g /^ m)) & not
-infty in rng (g | m1) & not
-infty in rng (g /^ m) & not
-infty in rng (g | m) )
by A19, A20, MESFUNC5:def 3;
A24:
(
Sum (g | m1) <> -infty &
Sum <*(f . (n + 1))*> <> -infty &
Sum (g /^ m) <> -infty )
by A22, Th66, MEASURE9:36, Th65;
A25:
now for x being object holds card (Coim ((f | n),x)) = card (Coim (((g | m1) ^ (g /^ m)),x))let x be
object ;
card (Coim ((f | n),x)) = card (Coim (((g | m1) ^ (g /^ m)),x))
card (Coim (f,x)) = card (Coim (g,x))
by A5, CLASSES1:def 10;
then
card (f " {x}) = card (Coim (g,x))
by RELAT_1:def 17;
then
card (f " {x}) = card (g " {x})
by RELAT_1:def 17;
then (card ((f | n) " {x})) + (card (<*(f . (n + 1))*> " {x})) =
card ((((g | m1) ^ <*(f . (n + 1))*>) ^ (g /^ m)) " {x})
by A15, A17, A18, FINSEQ_3:57
.=
(card (((g | m1) ^ <*(f . (n + 1))*>) " {x})) + (card ((g /^ m) " {x}))
by FINSEQ_3:57
.=
((card ((g | m1) " {x})) + (card (<*(f . (n + 1))*> " {x}))) + (card ((g /^ m) " {x}))
by FINSEQ_3:57
.=
((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:57
.=
(card (Coim (((g | m1) ^ (g /^ m)),x))) + (card (<*(f . (n + 1))*> " {x}))
by RELAT_1:def 17
;
hence
card (Coim ((f | n),x)) = card (Coim (((g | m1) ^ (g /^ m)),x))
by RELAT_1:def 17;
verum end;
len (f | n) = n
by A6, FINSEQ_1:59, NAT_1:11;
then
Sum (f | n) = Sum ((g | m1) ^ (g /^ m))
by A4, A19, A20, A25, CLASSES1:def 10;
hence Sum f =
(Sum ((g | m1) ^ (g /^ m))) + (Sum <*(f . (n + 1))*>)
by A18, A23, A21, EXTREAL1:10
.=
((Sum (g | m1)) + (Sum (g /^ m))) + (Sum <*(f . (n + 1))*>)
by A23, EXTREAL1:10
.=
((Sum (g | m1)) + (Sum <*(f . (n + 1))*>)) + (Sum (g /^ m))
by A24, XXREAL_3:29
.=
(Sum (g | m)) + (Sum (g /^ m))
by A15, A17, A23, A21, EXTREAL1:10
.=
Sum g
by A16, A23, EXTREAL1:10
;
verum
end;
A26:
S1[ 0 ]
for n being Nat holds S1[n]
from NAT_1:sch 2(A26, A3);
hence
Sum R1 = Sum R2
by A1, A2; verum