let R1, R2 be without-infty FinSequence of ExtREAL ; :: thesis: ( R1,R2 are_fiberwise_equipotent implies Sum R1 = Sum R2 )
defpred S₁[ Nat] means for f, g being without-infty FinSequence of ExtREAL st f,g are_fiberwise_equipotent & len f = $1 holds
Sum f = Sum g;
assume A1: R1,R2 are_fiberwise_equipotent ; :: thesis: Sum R1 = Sum R2
A2: len R1 = len R1 ;
A3: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A4: S₁[n] ; :: thesis: S₁[n + 1]
let f, g be without-infty FinSequence of ExtREAL ; :: thesis: ( 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 ; :: thesis: 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 16
.= (g | (Seg m)) | (Seg m1) by FINSEQ_1:def 16
.= g | ((Seg m) /\ (Seg m1)) by RELAT_1:71
.= g | (Seg m1) by A14, XBOOLE_1:28
.= g | m1 by FINSEQ_1:def 16 ;
A18: f = (f | n) ^ <*(f . (n + 1))*> by A6, RFINSEQ:7;
A19: ( f | n is without-infty & g | m1 is without-infty & g /^ m is without-infty & g | m is without-infty & g /^ m is without-infty ) by MEASURE9:36, Th65;
then A20: ( (g | m1) ^ (g /^ m) is without-infty & (g | m1) ^ (g /^ m) is without-infty ) 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 without-infty 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 :: thesis: for x being object holds card (Coim ((f | n),x)) = card (Coim (((g | m1) ^ (g /^ m)),x))

let x be object ; :: thesis: 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; :: thesis: 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 ;
:: thesis: verum

end;

A26: S₁[ 0 ]

proof

let f, g be without-infty FinSequence of ExtREAL ; :: thesis: ( f,g are_fiberwise_equipotent & len f = 0 implies Sum f = Sum g )
assume ( f,g are_fiberwise_equipotent & len f = 0 ) ; :: thesis: Sum f = Sum g
then A27: ( len g = 0 & f = <*> ExtREAL ) by RFINSEQ:3;
then g = <*> ExtREAL ;
hence Sum f = Sum g by A27; :: thesis: verum

end;

for n being Nat holds S₁[n] from NAT_1:sch 2(A26, A3);
hence Sum R1 = Sum R2 by A1, A2; :: thesis: verum