let K be Ring; :: thesis: for R1, R2 being FinSequence of K st R1,R2 are_fiberwise_equipotent holds

Sum R1 = Sum R2

let R1, R2 be FinSequence of K; :: thesis: ( R1,R2 are_fiberwise_equipotent implies Sum R1 = Sum R2 )

defpred S_{1}[ Nat] means for f, g being FinSequence of K 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_{1}[n] holds

S_{1}[n + 1]
_{1}[ 0 ]
_{1}[n]
from NAT_1:sch 2(A19, A3);

hence Sum R1 = Sum R2 by A1, A2; :: thesis: verum

Sum R1 = Sum R2

let R1, R2 be FinSequence of K; :: thesis: ( R1,R2 are_fiberwise_equipotent implies Sum R1 = Sum R2 )

defpred S

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

S

proof

A19:
S
let n be Nat; :: thesis: ( S_{1}[n] implies S_{1}[n + 1] )

assume A4: S_{1}[n]
; :: thesis: S_{1}[n + 1]

let f, g be FinSequence of K; :: 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 Z: n + 1 in dom f by A6, FINSEQ_3:25;

then X: f /. (n + 1) = f . (n + 1) by PARTFUN1:def 6;

then f /. (n + 1) in rng g by A7, FUNCT_1:def 3, Z;

then consider m being Nat such that

A8: m in dom g and

A9: g . m = f /. (n + 1) by FINSEQ_2:10;

set gg = g /^ m;

set gm = g | m;

m <= len g by A8, FINSEQ_3:25;

then A10: len (g | m) = m by FINSEQ_1:59;

A11: 1 <= m by A8, FINSEQ_3:25;

then max (0,(m - 1)) = m - 1 by FINSEQ_2:4;

then reconsider m1 = m - 1 as Element of NAT by FINSEQ_2:5;

A12: m = m1 + 1 ;

then A13: Seg m1 c= Seg m by FINSEQ_1:5, NAT_1:11;

m in Seg m by A11;

then (g | m) . m = f /. (n + 1) by A8, A9, RFINSEQ:6;

then A14: g | m = ((g | m) | m1) ^ <*(f /. (n + 1))*> by A10, A12, RFINSEQ:7;

set fn = f | n;

A15: g = (g | m) ^ (g /^ m) by RFINSEQ:8;

A16: (g | m) | m1 = (g | m) | (Seg m1)

.= (g | (Seg m)) | (Seg m1)

.= g | ((Seg m) /\ (Seg m1)) by RELAT_1:71

.= g | (Seg m1) by A13, XBOOLE_1:28

.= g | m1 ;

A17: f = (f | n) ^ <*(f /. (n + 1))*> by A6, RFINSEQ:7, X;

len (f | n) = n by A6, FINSEQ_1:59, NAT_1:11;

then Sum (f | n) = Sum ((g | m1) ^ (g /^ m)) by A4, A18;

hence Sum f = (Sum ((g | m1) ^ (g /^ m))) + (Sum <*(f /. (n + 1))*>) by A17, RLVECT_1:41

.= ((Sum (g | m1)) + (Sum (g /^ m))) + (Sum <*(f /. (n + 1))*>) by RLVECT_1:41

.= (Sum (g | m1)) + ((Sum (g /^ m)) + (Sum <*(f /. (n + 1))*>)) by RLVECT_1:def 3

.= (Sum (g | m1)) + ((Sum <*(f /. (n + 1))*>) + (Sum (g /^ m)))

.= ((Sum (g | m1)) + (Sum <*(f /. (n + 1))*>)) + (Sum (g /^ m)) by RLVECT_1:def 3

.= (Sum (g | m)) + (Sum (g /^ m)) by A14, A16, RLVECT_1:41

.= Sum g by A15, RLVECT_1:41 ;

:: thesis: verum

end;assume A4: S

let f, g be FinSequence of K; :: 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 Z: n + 1 in dom f by A6, FINSEQ_3:25;

then X: f /. (n + 1) = f . (n + 1) by PARTFUN1:def 6;

then f /. (n + 1) in rng g by A7, FUNCT_1:def 3, Z;

then consider m being Nat such that

A8: m in dom g and

A9: g . m = f /. (n + 1) by FINSEQ_2:10;

set gg = g /^ m;

set gm = g | m;

m <= len g by A8, FINSEQ_3:25;

then A10: len (g | m) = m by FINSEQ_1:59;

A11: 1 <= m by A8, FINSEQ_3:25;

then max (0,(m - 1)) = m - 1 by FINSEQ_2:4;

then reconsider m1 = m - 1 as Element of NAT by FINSEQ_2:5;

A12: m = m1 + 1 ;

then A13: Seg m1 c= Seg m by FINSEQ_1:5, NAT_1:11;

m in Seg m by A11;

then (g | m) . m = f /. (n + 1) by A8, A9, RFINSEQ:6;

then A14: g | m = ((g | m) | m1) ^ <*(f /. (n + 1))*> by A10, A12, RFINSEQ:7;

set fn = f | n;

A15: g = (g | m) ^ (g /^ m) by RFINSEQ:8;

A16: (g | m) | m1 = (g | m) | (Seg m1)

.= (g | (Seg m)) | (Seg m1)

.= g | ((Seg m) /\ (Seg m1)) by RELAT_1:71

.= g | (Seg m1) by A13, XBOOLE_1:28

.= g | m1 ;

A17: f = (f | n) ^ <*(f /. (n + 1))*> by A6, RFINSEQ:7, X;

now :: thesis: for x being object holds card (Coim ((f | n),x)) = card (Coim (((g | m1) ^ (g /^ m)),x))

then A18:
f | n,(g | m1) ^ (g /^ m) are_fiberwise_equipotent
;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;

then (card ((f | n) " {x})) + (card (<*(f /. (n + 1))*> " {x})) = card ((((g | m1) ^ <*(f /. (n + 1))*>) ^ (g /^ m)) " {x}) by A15, A14, A16, A17, 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 ;

hence card (Coim ((f | n),x)) = card (Coim (((g | m1) ^ (g /^ m)),x)) ; :: thesis: verum

end;card (Coim (f,x)) = card (Coim (g,x)) by A5;

then (card ((f | n) " {x})) + (card (<*(f /. (n + 1))*> " {x})) = card ((((g | m1) ^ <*(f /. (n + 1))*>) ^ (g /^ m)) " {x}) by A15, A14, A16, A17, 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 ;

hence card (Coim ((f | n),x)) = card (Coim (((g | m1) ^ (g /^ m)),x)) ; :: thesis: verum

len (f | n) = n by A6, FINSEQ_1:59, NAT_1:11;

then Sum (f | n) = Sum ((g | m1) ^ (g /^ m)) by A4, A18;

hence Sum f = (Sum ((g | m1) ^ (g /^ m))) + (Sum <*(f /. (n + 1))*>) by A17, RLVECT_1:41

.= ((Sum (g | m1)) + (Sum (g /^ m))) + (Sum <*(f /. (n + 1))*>) by RLVECT_1:41

.= (Sum (g | m1)) + ((Sum (g /^ m)) + (Sum <*(f /. (n + 1))*>)) by RLVECT_1:def 3

.= (Sum (g | m1)) + ((Sum <*(f /. (n + 1))*>) + (Sum (g /^ m)))

.= ((Sum (g | m1)) + (Sum <*(f /. (n + 1))*>)) + (Sum (g /^ m)) by RLVECT_1:def 3

.= (Sum (g | m)) + (Sum (g /^ m)) by A14, A16, RLVECT_1:41

.= Sum g by A15, RLVECT_1:41 ;

:: thesis: verum

proof

for n being Nat holds S
let f, g be FinSequence of K; :: 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 A20: ( len g = 0 & f = <*> the carrier of INT.Ring ) by RFINSEQ:3;

then g = <*> the carrier of INT.Ring ;

hence Sum f = Sum g by A20; :: thesis: verum

end;assume ( f,g are_fiberwise_equipotent & len f = 0 ) ; :: thesis: Sum f = Sum g

then A20: ( len g = 0 & f = <*> the carrier of INT.Ring ) by RFINSEQ:3;

then g = <*> the carrier of INT.Ring ;

hence Sum f = Sum g by A20; :: thesis: verum

hence Sum R1 = Sum R2 by A1, A2; :: thesis: verum