let n, m be Nat; for a being Function of [:(Seg n),(Seg m):],REAL
for p, q being FinSequence of REAL st dom p = Seg n & ( for i being Nat st i in dom p holds
ex r being FinSequence of REAL st
( dom r = Seg m & p . i = Sum r & ( for j being Nat st j in dom r holds
r . j = a . (i,j) ) ) ) & dom q = Seg m & ( for j being Nat st j in dom q holds
ex s being FinSequence of REAL st
( dom s = Seg n & q . j = Sum s & ( for i being Nat st i in dom s holds
s . i = a . (i,j) ) ) ) holds
Sum p = Sum q
let a be Function of [:(Seg n),(Seg m):],REAL; for p, q being FinSequence of REAL st dom p = Seg n & ( for i being Nat st i in dom p holds
ex r being FinSequence of REAL st
( dom r = Seg m & p . i = Sum r & ( for j being Nat st j in dom r holds
r . j = a . (i,j) ) ) ) & dom q = Seg m & ( for j being Nat st j in dom q holds
ex s being FinSequence of REAL st
( dom s = Seg n & q . j = Sum s & ( for i being Nat st i in dom s holds
s . i = a . (i,j) ) ) ) holds
Sum p = Sum q
let p, q be FinSequence of REAL ; ( dom p = Seg n & ( for i being Nat st i in dom p holds
ex r being FinSequence of REAL st
( dom r = Seg m & p . i = Sum r & ( for j being Nat st j in dom r holds
r . j = a . (i,j) ) ) ) & dom q = Seg m & ( for j being Nat st j in dom q holds
ex s being FinSequence of REAL st
( dom s = Seg n & q . j = Sum s & ( for i being Nat st i in dom s holds
s . i = a . (i,j) ) ) ) implies Sum p = Sum q )
assume that
A1:
dom p = Seg n
and
A2:
for i being Nat st i in dom p holds
ex r being FinSequence of REAL st
( dom r = Seg m & p . i = Sum r & ( for j being Nat st j in dom r holds
r . j = a . (i,j) ) )
and
A3:
dom q = Seg m
and
A4:
for j being Nat st j in dom q holds
ex s being FinSequence of REAL st
( dom s = Seg n & q . j = Sum s & ( for i being Nat st i in dom s holds
s . i = a . (i,j) ) )
; Sum p = Sum q
A5:
for i being Nat st i in dom p holds
ex r being FinSequence of REAL st
( dom r = Seg m & p . i = Sum r & ( for j being Nat st j in dom r holds
r . j = a . [i,j] ) )
for j being Nat st j in dom q holds
ex s being FinSequence of REAL st
( dom s = Seg n & q . j = Sum s & ( for i being Nat st i in dom s holds
s . i = a . [i,j] ) )
hence
Sum p = Sum q
by MESFUNC3:1, A1, A5, A3; verum