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] ) )
proof
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]
proof
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;
take r ; :: thesis: ( dom r = Seg m & p . i = Sum r & ( for j being Nat st j in dom r holds
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;
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] ) )
proof
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]
proof
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;
take s ; :: thesis: ( dom s = Seg n & q . j = Sum s & ( for i being Nat st i in dom s holds
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;
hence Sum p = Sum q by MESFUNC3:1, A1, A5, A3; :: thesis: verum