let n, m be Nat; :: thesis: 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; :: thesis: 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 ; :: thesis: ( 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) ) ) ; :: thesis: 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] ) )

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] ) )

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; :: thesis: 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 ; :: thesis: ( 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) ) ) ; :: thesis: 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] ) )

proof

for j being Nat st j in dom q holds
let i be Nat; :: thesis: ( i in dom p implies 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] ) ) )

assume B0: i in dom p ; :: thesis: 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] ) )

consider r being FinSequence of REAL such that

B2: ( dom r = Seg m & p . i = Sum r & ( for j being Nat st j in dom r holds

r . j = a . (i,j) ) ) by B0, A2;

B3: for j being Nat st j in dom r holds

r . j = a . [i,j]

r . j = a . [i,j] ) )

thus ( dom r = Seg m & p . i = Sum r & ( for j being Nat st j in dom r holds

r . j = a . [i,j] ) ) by B2, B3; :: thesis: verum

end;( dom r = Seg m & p . i = Sum r & ( for j being Nat st j in dom r holds

r . j = a . [i,j] ) ) )

assume B0: i in dom p ; :: thesis: 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] ) )

consider r being FinSequence of REAL such that

B2: ( dom r = Seg m & p . i = Sum r & ( for j being Nat st j in dom r holds

r . j = a . (i,j) ) ) by B0, A2;

B3: for j being Nat st j in dom r holds

r . j = a . [i,j]

proof

take
r
; :: thesis: ( dom r = Seg m & p . i = Sum r & ( for j being Nat st j in dom r holds
let j be Nat; :: thesis: ( j in dom r implies r . j = a . [i,j] )

assume j in dom r ; :: thesis: r . j = a . [i,j]

then r . j = a . (i,j) by B2;

hence r . j = a . [i,j] ; :: thesis: verum

end;assume j in dom r ; :: thesis: r . j = a . [i,j]

then r . j = a . (i,j) by B2;

hence r . j = a . [i,j] ; :: thesis: verum

r . j = a . [i,j] ) )

thus ( dom r = Seg m & p . i = Sum r & ( for j being Nat st j in dom r holds

r . j = a . [i,j] ) ) by B2, B3; :: thesis: verum

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] ) )

proof

hence
Sum p = Sum q
by MESFUNC3:1, A1, A5, A3; :: thesis: verum
let j be Nat; :: thesis: ( j in dom q implies 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] ) ) )

assume C0: j in dom q ; :: thesis: 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] ) )

consider s being FinSequence of REAL such that

C2: ( dom s = Seg n & q . j = Sum s & ( for i being Nat st i in dom s holds

s . i = a . (i,j) ) ) by C0, A4;

C3: for i being Nat st i in dom s holds

s . i = a . [i,j]

s . i = a . [i,j] ) )

thus ( dom s = Seg n & q . j = Sum s & ( for i being Nat st i in dom s holds

s . i = a . [i,j] ) ) by C2, C3; :: thesis: verum

end;( dom s = Seg n & q . j = Sum s & ( for i being Nat st i in dom s holds

s . i = a . [i,j] ) ) )

assume C0: j in dom q ; :: thesis: 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] ) )

consider s being FinSequence of REAL such that

C2: ( dom s = Seg n & q . j = Sum s & ( for i being Nat st i in dom s holds

s . i = a . (i,j) ) ) by C0, A4;

C3: for i being Nat st i in dom s holds

s . i = a . [i,j]

proof

take
s
; :: thesis: ( dom s = Seg n & q . j = Sum s & ( for i being Nat st i in dom s holds
let i be Nat; :: thesis: ( i in dom s implies s . i = a . [i,j] )

assume i in dom s ; :: thesis: s . i = a . [i,j]

then s . i = a . (i,j) by C2;

hence s . i = a . [i,j] ; :: thesis: verum

end;assume i in dom s ; :: thesis: s . i = a . [i,j]

then s . i = a . (i,j) by C2;

hence s . i = a . [i,j] ; :: thesis: verum

s . i = a . [i,j] ) )

thus ( dom s = Seg n & q . j = Sum s & ( for i being Nat st i in dom s holds

s . i = a . [i,j] ) ) by C2, C3; :: thesis: verum