let D be non empty set ; :: thesis: for f, g being FinSequence of PFuncs D,REAL st f,g are_fiberwise_equipotent holds
Sum f = Sum g
defpred S₁[ Element of NAT ] means for f, g being FinSequence of PFuncs D,REAL st f,g are_fiberwise_equipotent & len f = $1 holds
Sum f = Sum g;
let f, g be FinSequence of PFuncs D,REAL ; :: thesis: ( f,g are_fiberwise_equipotent implies Sum f = Sum g )
assume A1: f,g are_fiberwise_equipotent ; :: thesis: Sum f = Sum g
A2: len f = len f ;
A3: for n being Element of NAT st S₁[n] holds
S₁[n + 1]

proof

let n be Element of NAT ; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A4: S₁[n] ; :: thesis: S₁[n + 1]
let f, g be FinSequence of PFuncs D,REAL ; :: 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
0 + 1 <= n + 1 by NAT_1:13;
then A7: n + 1 in dom f by A6, FINSEQ_3:27;
then reconsider a = f . (n + 1) as Element of PFuncs D,REAL by FINSEQ_2:13;
rng f = rng g by A5, CLASSES1:83;
then a in rng g by A7, FUNCT_1:def 5;
then consider m being Nat such that
A8: m in dom g and
A9: g . m = a by FINSEQ_2:11;
A10: g = (g | m) ^ (g /^ m) by RFINSEQ:21;
set gg = g /^ m;
set gm = g | m;
m <= len g by A8, FINSEQ_3:27;
then A11: len (g | m) = m by FINSEQ_1:80;
set fn = f | n;
A12: f = (f | n) ^ <*a*> by A6, RFINSEQ:20;
A13: 1 <= m by A8, 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;
A14: m = m1 + 1 ;
then m1 <= m by NAT_1:11;
then A15: Seg m1 c= Seg m by FINSEQ_1:7;
m in Seg m by A13, FINSEQ_1:3;
then (g | m) . m = a by A8, A9, RFINSEQ:19;
then A16: g | m = ((g | m) | m1) ^ <*a*> by A11, A14, RFINSEQ:20;
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:100
.= g | (Seg m1) by A15, XBOOLE_1:28
.= g | m1 by FINSEQ_1:def 15 ;

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 A5, CLASSES1:def 9;
then (card ((f | n) " {x})) + (card (<*a*> " {x})) = card ((((g | m1) ^ <*a*>) ^ (g /^ m)) " {x}) by A10, A16, A17, A12, FINSEQ_3:63
.= (card (((g | m1) ^ <*a*>) " {x})) + (card ((g /^ m) " {x})) by FINSEQ_3:63
.= ((card ((g | m1) " {x})) + (card (<*a*> " {x}))) + (card ((g /^ m) " {x})) by FINSEQ_3:63
.= ((card ((g | m1) " {x})) + (card ((g /^ m) " {x}))) + (card (<*a*> " {x}))
.= (card (((g | m1) ^ (g /^ m)) " {x})) + (card (<*a*> " {x})) by FINSEQ_3:63 ;
hence card (Coim (f | n),x) = card (Coim ((g | m1) ^ (g /^ m)),x) ; :: thesis: verum

end;

then A18: f | n,(g | m1) ^ (g /^ m) are_fiberwise_equipotent by CLASSES1:def 9;
len (f | n) = n by A6, FINSEQ_1:80, NAT_1:11;
then Sum (f | n) = Sum ((g | m1) ^ (g /^ m)) by A4, A18;
hence Sum f = (Sum ((g | m1) ^ (g /^ m))) + (Sum <*a*>) by A12, Th24
.= ((Sum (g | m1)) + (Sum (g /^ m))) + (Sum <*a*>) by Th24
.= ((Sum (g | m1)) + (Sum <*a*>)) + (Sum (g /^ m)) by RFUNCT_1:19
.= (Sum (g | m)) + (Sum (g /^ m)) by A16, A17, Th24
.= Sum g by A10, Th24 ;
:: thesis: verum

end;

A19: S₁[ 0 ]

proof

let f, g be FinSequence of PFuncs D,REAL ; :: 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 X: ( len g = 0 & f = <*> (PFuncs D,REAL ) ) by RFINSEQ:16;
then g = <*> (PFuncs D,REAL ) ;
hence Sum f = Sum g by X; :: thesis: verum

end;

for n being Element of NAT holds S₁[n] from NAT_1:sch 1(A19, A3);
hence Sum f = Sum g by A1, A2; :: thesis: verum