let s1, s2 be Element of ExtREAL ; :: thesis: ( ex F being Finite_Sep_Sequence of S ex a, x being FinSequence of ExtREAL st
( F,a are_Re-presentation_of f & a . 1 = 0. & ( for n being Nat st 2 <= n & n in dom a holds
( 0. < a . n & a . n < +infty ) ) & dom x = dom F & ( for n being Nat st n in dom x holds
x . n = (a . n) * ((M * F) . n) ) & s1 = Sum x ) & ex F being Finite_Sep_Sequence of S ex a, x being FinSequence of ExtREAL st
( F,a are_Re-presentation_of f & a . 1 = 0. & ( for n being Nat st 2 <= n & n in dom a holds
( 0. < a . n & a . n < +infty ) ) & dom x = dom F & ( for n being Nat st n in dom x holds
x . n = (a . n) * ((M * F) . n) ) & s2 = Sum x ) implies s1 = s2 )
assume that
A8: ex F1 being Finite_Sep_Sequence of S ex a1, x1 being FinSequence of ExtREAL st
( F1,a1 are_Re-presentation_of f & a1 . 1 = 0. & ( for n being Nat st 2 <= n & n in dom a1 holds
( 0. < a1 . n & a1 . n < +infty ) ) & dom x1 = dom F1 & ( for n being Nat st n in dom x1 holds
x1 . n = (a1 . n) * ((M * F1) . n) ) & s1 = Sum x1 ) and
A9: ex F2 being Finite_Sep_Sequence of S ex a2, x2 being FinSequence of ExtREAL st
( F2,a2 are_Re-presentation_of f & a2 . 1 = 0. & ( for n being Nat st 2 <= n & n in dom a2 holds
( 0. < a2 . n & a2 . n < +infty ) ) & dom x2 = dom F2 & ( for n being Nat st n in dom x2 holds
x2 . n = (a2 . n) * ((M * F2) . n) ) & s2 = Sum x2 ) ; :: thesis: s1 = s2
thus s1 = s2 :: thesis: verum

proof

consider F2 being Finite_Sep_Sequence of S, a2, x2 being FinSequence of ExtREAL such that
A10: F2,a2 are_Re-presentation_of f and
A11: a2 . 1 = 0. and
A12: for n being Nat st 2 <= n & n in dom a2 holds
( 0. < a2 . n & a2 . n < +infty ) and
A13: dom x2 = dom F2 and
A14: for n being Nat st n in dom x2 holds
x2 . n = (a2 . n) * ((M * F2) . n) and
A15: s2 = Sum x2 by A9;
A16: dom F2 = dom a2 by A10;
A17: for n being Nat st n in dom a2 holds
0. <= a2 . n

proof

let n be Nat; :: thesis: ( n in dom a2 implies 0. <= a2 . n )
assume A18: n in dom a2 ; :: thesis: 0. <= a2 . n

now :: thesis: ( ( n = 1 & a2 . 1 = 0. ) or ( n <> 1 & 0. <= a2 . n ) )

per cases ( n = 1 or n <> 1 ) ;

case n = 1 ; :: thesis: a2 . 1 = 0.

thus a2 . 1 = 0. by A11; :: thesis: verum

end;

case A19: n <> 1 ; :: thesis: 0. <= a2 . n

n in Seg (len a2) by A18, FINSEQ_1:def 3;
then 1 <= n by FINSEQ_1:1;
then 1 < n by A19, XXREAL_0:1;
then 1 + 1 < n + 1 by XREAL_1:8;
then 2 <= n by NAT_1:13;
hence 0. <= a2 . n by A12, A18; :: thesis: verum

end;

end;

end;

hence 0. <= a2 . n ; :: thesis: verum

end;

A20: for n being Nat st n in dom F2 holds
0. <= (M * F2) . n

proof

let n be Nat; :: thesis: ( n in dom F2 implies 0. <= (M * F2) . n )
assume n in dom F2 ; :: thesis: 0. <= (M * F2) . n
then ( (M * F2) . n = M . (F2 . n) & F2 . n in rng F2 ) by FUNCT_1:3, FUNCT_1:13;
hence 0. <= (M * F2) . n by SUPINF_2:39; :: thesis: verum

end;

A21: not -infty in rng x2

proof

assume -infty in rng x2 ; :: thesis: contradiction
then consider n being object such that
A22: n in dom x2 and
A23: x2 . n = -infty by FUNCT_1:def 3;
reconsider n = n as set by TARSKI:1;
( 0. <= a2 . n & 0. <= (M * F2) . n ) by A13, A16, A20, A17, A22;
then 0. <= (a2 . n) * ((M * F2) . n) ;
hence contradiction by A14, A22, A23; :: thesis: verum

end;

consider F1 being Finite_Sep_Sequence of S, a1, x1 being FinSequence of ExtREAL such that
A24: F1,a1 are_Re-presentation_of f and
A25: a1 . 1 = 0. and
A26: for n being Nat st 2 <= n & n in dom a1 holds
( 0. < a1 . n & a1 . n < +infty ) and
A27: dom x1 = dom F1 and
A28: for n being Nat st n in dom x1 holds
x1 . n = (a1 . n) * ((M * F1) . n) and
A29: s1 = Sum x1 by A8;
A30: dom F1 = dom a1 by A24;
A31: for n being Nat st n in dom a1 holds
0. <= a1 . n

proof

let n be Nat; :: thesis: ( n in dom a1 implies 0. <= a1 . n )
assume A32: n in dom a1 ; :: thesis: 0. <= a1 . n

now :: thesis: ( ( n = 1 & a1 . 1 = 0. ) or ( n <> 1 & 0. <= a1 . n ) )

per cases ( n = 1 or n <> 1 ) ;

case n = 1 ; :: thesis: a1 . 1 = 0.

thus a1 . 1 = 0. by A25; :: thesis: verum

end;

case A33: n <> 1 ; :: thesis: 0. <= a1 . n

n in Seg (len a1) by A32, FINSEQ_1:def 3;
then 1 <= n by FINSEQ_1:1;
then 1 < n by A33, XXREAL_0:1;
then 1 + 1 < n + 1 by XREAL_1:8;
then 2 <= n by NAT_1:13;
hence 0. <= a1 . n by A26, A32; :: thesis: verum

end;

end;

end;

hence 0. <= a1 . n ; :: thesis: verum

end;

A34: for n being Nat st n in dom F1 holds
0. <= (M * F1) . n

proof

let n be Nat; :: thesis: ( n in dom F1 implies 0. <= (M * F1) . n )
assume n in dom F1 ; :: thesis: 0. <= (M * F1) . n
then ( (M * F1) . n = M . (F1 . n) & F1 . n in rng F1 ) by FUNCT_1:3, FUNCT_1:13;
hence 0. <= (M * F1) . n by SUPINF_2:39; :: thesis: verum

end;

A35: not -infty in rng x1

proof

assume -infty in rng x1 ; :: thesis: contradiction
then consider n being object such that
A36: n in dom x1 and
A37: x1 . n = -infty by FUNCT_1:def 3;
reconsider n = n as set by TARSKI:1;
( 0. <= a1 . n & 0. <= (M * F1) . n ) by A27, A30, A34, A31, A36;
then 0. <= (a1 . n) * ((M * F1) . n) ;
hence contradiction by A28, A36, A37; :: thesis: verum

end;

now :: thesis: ( ( ex i, j being Nat st
( i in dom F1 & j in dom F2 & 2 <= i & 2 <= j & M . ((F1 . i) /\ (F2 . j)) = +infty ) & s1 = s2 ) or ( ( for i, j being Nat st i in dom F1 & j in dom F2 & 2 <= i & 2 <= j holds
M . ((F1 . i) /\ (F2 . j)) <> +infty ) & s1 = s2 ) )

per cases ( ex i, j being Nat st
( i in dom F1 & j in dom F2 & 2 <= i & 2 <= j & M . ((F1 . i) /\ (F2 . j)) = +infty ) or for i, j being Nat st i in dom F1 & j in dom F2 & 2 <= i & 2 <= j holds
M . ((F1 . i) /\ (F2 . j)) <> +infty ) ;

case ex i, j being Nat st
( i in dom F1 & j in dom F2 & 2 <= i & 2 <= j & M . ((F1 . i) /\ (F2 . j)) = +infty ) ; :: thesis: s1 = s2

then consider i, j being Nat such that
A38: i in dom F1 and
A39: j in dom F2 and
A40: 2 <= i and
A41: 2 <= j and
A42: M . ((F1 . i) /\ (F2 . j)) = +infty ;
A43: F2 . j in rng F2 by A39, FUNCT_1:3;
A44: F1 . i in rng F1 by A38, FUNCT_1:3;
then A45: (F1 . i) /\ (F2 . j) in S by A43, MEASURE1:34;
(F1 . i) /\ (F2 . j) c= F1 . i by XBOOLE_1:17;
then M . (F1 . i) = +infty by A42, A44, A45, MEASURE1:31, XXREAL_0:4;
then A46: (M * F1) . i = +infty by A38, FUNCT_1:13;
0. < a1 . i by A26, A30, A38, A40;
then +infty = (a1 . i) * ((M * F1) . i) by A46, XXREAL_3:def 5;
then x1 . i = +infty by A27, A28, A38;
then +infty in rng x1 by A27, A38, FUNCT_1:def 3;
then A47: Sum x1 = +infty by A35, Th17;
(F1 . i) /\ (F2 . j) c= F2 . j by XBOOLE_1:17;
then M . (F2 . j) = +infty by A42, A43, A45, MEASURE1:31, XXREAL_0:4;
then A48: (M * F2) . j = +infty by A39, FUNCT_1:13;
0. < a2 . j by A12, A16, A39, A41;
then +infty = (a2 . j) * ((M * F2) . j) by A48, XXREAL_3:def 5;
then x2 . j = +infty by A13, A14, A39;
then +infty in rng x2 by A13, A39, FUNCT_1:def 3;
hence s1 = s2 by A29, A15, A21, A47, Th17; :: thesis: verum

end;

case A49: for i, j being Nat st i in dom F1 & j in dom F2 & 2 <= i & 2 <= j holds
M . ((F1 . i) /\ (F2 . j)) <> +infty ; :: thesis: s1 = s2

set m = len x2;
set n = len x1;
ex a being Function of [:(Seg (len x1)),(Seg (len x2)):],REAL st
for i, j being Nat st i in Seg (len x1) & j in Seg (len x2) holds
a . (i,j) = (a1 . i) * (M . ((F1 . i) /\ (F2 . j)))

proof

deffunc H₁( object , object ) -> object = (a1 . $1) * (M . ((F1 . $1) /\ (F2 . $2)));
A50: for x, y being object st x in Seg (len x1) & y in Seg (len x2) holds
H₁(x,y) in REAL

proof

let x, y be object ; :: thesis: ( x in Seg (len x1) & y in Seg (len x2) implies H₁(x,y) in REAL )
assume that
A51: x in Seg (len x1) and
A52: y in Seg (len x2) ; :: thesis: H₁(x,y) in REAL
x in { k where k is Nat : ( 1 <= k & k <= len x1 ) } by A51, FINSEQ_1:def 1;
then consider kx being Nat such that
A53: x = kx and
A54: 1 <= kx and
kx <= len x1 ;
y in { k where k is Nat : ( 1 <= k & k <= len x2 ) } by A52, FINSEQ_1:def 1;
then consider ky being Nat such that
A55: y = ky and
A56: 1 <= ky and
ky <= len x2 ;
A57: ky in dom F2 by A13, A52, A55, FINSEQ_1:def 3;
then A58: F2 . ky in rng F2 by FUNCT_1:3;
A59: kx in dom F1 by A27, A51, A53, FINSEQ_1:def 3;
then F1 . kx in rng F1 by FUNCT_1:3;
then A60: (F1 . kx) /\ (F2 . ky) in S by A58, MEASURE1:34;

now :: thesis: ( ( ( not 2 <= kx or not 2 <= ky ) & H₁(kx,ky) in REAL ) or ( 2 <= kx & 2 <= ky & H₁(kx,ky) in REAL ) )

per cases ( not 2 <= kx or not 2 <= ky or ( 2 <= kx & 2 <= ky ) ) ;

case A61: ( not 2 <= kx or not 2 <= ky ) ; :: thesis: H₁(kx,ky) in REAL

now :: thesis: ( ( kx < 2 & H₁(kx,ky) in REAL ) or ( ky < 2 & H₁(kx,ky) in REAL ) )

per cases ( kx < 2 or ky < 2 ) by A61;

case A62: kx < 2 ; :: thesis: H₁(kx,ky) in REAL

then kx <= 1 + 1 ;
then kx <= 1 by A62, NAT_1:8;
then H₁(kx,ky) = 0. * (M . ((F1 . kx) /\ (F2 . ky))) by A25, A54, XXREAL_0:1
.= 0 ;
hence H₁(kx,ky) in REAL by XREAL_0:def 1; :: thesis: verum

end;

case A63: ky < 2 ; :: thesis: H₁(kx,ky) in REAL

then ky <= 1 + 1 ;
then A64: ky <= 1 by A63, NAT_1:8;

now :: thesis: ( ( (F1 . kx) /\ (F2 . ky) = {} & H₁(kx,ky) = 0 ) or ( (F1 . kx) /\ (F2 . ky) <> {} & H₁(kx,ky) = 0 ) )

per cases ( (F1 . kx) /\ (F2 . ky) = {} or (F1 . kx) /\ (F2 . ky) <> {} ) ;

case (F1 . kx) /\ (F2 . ky) = {} ; :: thesis: H₁(kx,ky) = 0

hence H₁(kx,ky) = (a1 . kx) * 0. by VALUED_0:def 19
.= 0 ;
:: thesis: verum

end;

case (F1 . kx) /\ (F2 . ky) <> {} ; :: thesis: H₁(kx,ky) = 0

then consider x being object such that
A65: x in (F1 . kx) /\ (F2 . ky) by XBOOLE_0:def 1;
A66: x in F2 . ky by A65, XBOOLE_0:def 4;
x in F1 . kx by A65, XBOOLE_0:def 4;
then a1 . kx = f . x by A24, A59
.= a2 . ky by A10, A57, A66
.= 0. by A11, A56, A64, XXREAL_0:1 ;
hence H₁(kx,ky) = 0 ; :: thesis: verum

end;

end;

end;

hence H₁(kx,ky) in REAL by XREAL_0:def 1; :: thesis: verum

end;

end;

end;

hence H₁(kx,ky) in REAL ; :: thesis: verum

end;

case A67: ( 2 <= kx & 2 <= ky ) ; :: thesis: H₁(kx,ky) in REAL

A68: 0. <= a1 . kx by A30, A31, A59;
a1 . kx <> +infty by A26, A30, A59, A67;
then reconsider r2 = a1 . kx as Element of REAL by A68, XXREAL_0:14;
0. <= M . ((F1 . kx) /\ (F2 . ky)) by A60, SUPINF_2:39;
then reconsider r3 = M . ((F1 . kx) /\ (F2 . ky)) as Element of REAL by A49, A59, A57, A67, XXREAL_0:14;
(a1 . kx) * (M . ((F1 . kx) /\ (F2 . ky))) = r2 * r3 by EXTREAL1:1;
hence H₁(kx,ky) in REAL by XREAL_0:def 1; :: thesis: verum

end;

end;

end;

hence H₁(x,y) in REAL by A53, A55; :: thesis: verum

end;

consider f being Function of [:(Seg (len x1)),(Seg (len x2)):],REAL such that
A69: for x, y being object st x in Seg (len x1) & y in Seg (len x2) holds
f . (x,y) = H₁(x,y) from BINOP_1:sch 2(A50);
take f ; :: thesis: for i, j being Nat st i in Seg (len x1) & j in Seg (len x2) holds
f . (i,j) = (a1 . i) * (M . ((F1 . i) /\ (F2 . j)))
thus for i, j being Nat st i in Seg (len x1) & j in Seg (len x2) holds
f . (i,j) = (a1 . i) * (M . ((F1 . i) /\ (F2 . j))) by A69; :: thesis: verum

end;

then consider a being Function of [:(Seg (len x1)),(Seg (len x2)):],REAL such that
A70: for i, j being Nat st i in Seg (len x1) & j in Seg (len x2) holds
a . (i,j) = (a1 . i) * (M . ((F1 . i) /\ (F2 . j))) ;
ex p being FinSequence of REAL st
( dom p = Seg (len x1) & ( for i being Nat st i in dom p holds
ex r being FinSequence of REAL st
( dom r = Seg (len x2) & p . i = Sum r & ( for j being Nat st j in dom r holds
r . j = a . [i,j] ) ) ) )

proof

defpred S₁[ Nat, object ] means ex r being FinSequence of REAL st
( dom r = Seg (len x2) & $2 = Sum r & ( for j being Nat st j in dom r holds
r . j = a . [$1,j] ) );
A71: for k being Nat st k in Seg (len x1) holds
ex x being object st S₁[k,x]

proof

let k be Nat; :: thesis: ( k in Seg (len x1) implies ex x being object st S₁[k,x] )
assume k in Seg (len x1) ; :: thesis: ex x being object st S₁[k,x]
deffunc H₁( set ) -> set = a . [k,$1];
consider r being FinSequence such that
A72: len r = len x2 and
A73: for i being Nat st i in dom r holds
r . i = H₁(i) from FINSEQ_1:sch 2();
A74: dom r = Seg (len x2) by A72, FINSEQ_1:def 3;
for i being Nat st i in dom r holds
r . i in REAL

proof

let i be Nat; :: thesis: ( i in dom r implies r . i in REAL )
A75: a . [k,i] in REAL by XREAL_0:def 1;
assume i in dom r ; :: thesis: r . i in REAL
hence r . i in REAL by A73, A75; :: thesis: verum

end;

then reconsider r = r as FinSequence of REAL by FINSEQ_2:12;
take x = Sum r; :: thesis: S₁[k,x]
thus S₁[k,x] by A73, A74; :: thesis: verum

end;

consider p being FinSequence such that
A76: ( dom p = Seg (len x1) & ( for k being Nat st k in Seg (len x1) holds
S₁[k,p . k] ) ) from FINSEQ_1:sch 1(A71);
for i being Nat st i in dom p holds
p . i in REAL

proof

let i be Nat; :: thesis: ( i in dom p implies p . i in REAL )
assume i in dom p ; :: thesis: p . i in REAL
then ex r being FinSequence of REAL st
( dom r = Seg (len x2) & p . i = Sum r & ( for j being Nat st j in dom r holds
r . j = a . [i,j] ) ) by A76;
hence p . i in REAL by XREAL_0:def 1; :: thesis: verum

end;

then reconsider p = p as FinSequence of REAL by FINSEQ_2:12;
take p ; :: thesis: ( dom p = Seg (len x1) & ( for i being Nat st i in dom p holds
ex r being FinSequence of REAL st
( dom r = Seg (len x2) & p . i = Sum r & ( for j being Nat st j in dom r holds
r . j = a . [i,j] ) ) ) )
thus ( dom p = Seg (len x1) & ( for i being Nat st i in dom p holds
ex r being FinSequence of REAL st
( dom r = Seg (len x2) & p . i = Sum r & ( for j being Nat st j in dom r holds
r . j = a . [i,j] ) ) ) ) by A76; :: thesis: verum

end;

then consider p being FinSequence of REAL such that
A77: dom p = Seg (len x1) and
A78: for i being Nat st i in dom p holds
ex r being FinSequence of REAL st
( dom r = Seg (len x2) & p . i = Sum r & ( for j being Nat st j in dom r holds
r . j = a . [i,j] ) ) ;
A79: dom p = dom x1 by A77, FINSEQ_1:def 3;
for k being Nat st k in dom p holds
p . k = x1 . k

proof

let k be Nat; :: thesis: ( k in dom p implies p . k = x1 . k )
assume A80: k in dom p ; :: thesis: p . k = x1 . k
then consider r being FinSequence of REAL such that
A81: dom r = Seg (len x2) and
A82: p . k = Sum r and
A83: for j being Nat st j in dom r holds
r . j = a . [k,j] by A78;
ex F11 being Finite_Sep_Sequence of S st
( union (rng F11) = F1 . k & dom F11 = dom r & ( for j being Nat st j in dom r holds
F11 . j = (F1 . k) /\ (F2 . j) ) )

proof

deffunc H₁( set ) -> set = (F1 . k) /\ (F2 . $1);
consider F being FinSequence such that
A84: len F = len x2 and
A85: for i being Nat st i in dom F holds
F . i = H₁(i) from FINSEQ_1:sch 2();
A86: dom F = Seg (len x2) by A84, FINSEQ_1:def 3;
A87: for i being Nat st i in dom F holds
F . i in S

proof

let i be Nat; :: thesis: ( i in dom F implies F . i in S )
assume A88: i in dom F ; :: thesis: F . i in S
then i in Seg (len x2) by A84, FINSEQ_1:def 3;
then i in dom F2 by A13, FINSEQ_1:def 3;
then A89: F2 . i in rng F2 by FUNCT_1:3;
F1 . k in rng F1 by A27, A79, A80, FUNCT_1:3;
then (F1 . k) /\ (F2 . i) in S by A89, MEASURE1:34;
hence F . i in S by A85, A88; :: thesis: verum

end;

A90: dom F = Seg (len x2) by A84, FINSEQ_1:def 3;
reconsider F = F as FinSequence of S by A87, FINSEQ_2:12;
A91: dom F = dom F2 by A13, A90, FINSEQ_1:def 3;
then reconsider F = F as Finite_Sep_Sequence of S by A85, Th5;
take F ; :: thesis: ( union (rng F) = F1 . k & dom F = dom r & ( for j being Nat st j in dom r holds
F . j = (F1 . k) /\ (F2 . j) ) )
union (rng F) = (F1 . k) /\ (union (rng F2)) by A85, A91, Th6
.= (F1 . k) /\ (dom f) by A10
.= (F1 . k) /\ (union (rng F1)) by A24
.= F1 . k by A27, A79, A80, Th7 ;
hence ( union (rng F) = F1 . k & dom F = dom r & ( for j being Nat st j in dom r holds
F . j = (F1 . k) /\ (F2 . j) ) ) by A81, A85, A86; :: thesis: verum

end;

then consider F11 being Finite_Sep_Sequence of S such that
A92: union (rng F11) = F1 . k and
A93: dom F11 = dom r and
A94: for j being Nat st j in dom r holds
F11 . j = (F1 . k) /\ (F2 . j) ;
A95: Sum (M * F11) = M . (F1 . k) by A92, Th9;
k in Seg (len a1) by A27, A30, A79, A80, FINSEQ_1:def 3;
then A96: 1 <= k by FINSEQ_1:1;
( a1 . k <> -infty & a1 . k <> +infty )

proof

per cases ( k = 1 or k <> 1 ) ;

suppose k = 1 ; :: thesis: ( a1 . k <> -infty & a1 . k <> +infty )

hence ( a1 . k <> -infty & a1 . k <> +infty ) by A25; :: thesis: verum

end;

suppose k <> 1 ; :: thesis: ( a1 . k <> -infty & a1 . k <> +infty )

then 1 < k by A96, XXREAL_0:1;
then 1 + 1 <= k by NAT_1:13;
hence ( a1 . k <> -infty & a1 . k <> +infty ) by A26, A27, A30, A79, A80; :: thesis: verum

end;

end;

end;

then A97: a1 . k is Element of REAL by XXREAL_0:14;
reconsider rr = r as FinSequence of ExtREAL by Th11;
A98: for j being Nat st j in dom r holds
r . j = (a1 . k) * (M . ((F1 . k) /\ (F2 . j)))

proof

let j be Nat; :: thesis: ( j in dom r implies r . j = (a1 . k) * (M . ((F1 . k) /\ (F2 . j))) )
assume A99: j in dom r ; :: thesis: r . j = (a1 . k) * (M . ((F1 . k) /\ (F2 . j)))
hence r . j = a . (k,j) by A83
.= (a1 . k) * (M . ((F1 . k) /\ (F2 . j))) by A70, A77, A80, A81, A99 ;
:: thesis: verum

end;

A100: for j being Nat st j in dom rr holds
rr . j = (a1 . k) * ((M * F11) . j)

proof

let j be Nat; :: thesis: ( j in dom rr implies rr . j = (a1 . k) * ((M * F11) . j) )
assume A101: j in dom rr ; :: thesis: rr . j = (a1 . k) * ((M * F11) . j)
hence rr . j = (a1 . k) * (M . ((F1 . k) /\ (F2 . j))) by A98
.= (a1 . k) * (M . (F11 . j)) by A94, A101
.= (a1 . k) * ((M * F11) . j) by A93, A101, FUNCT_1:13 ;
:: thesis: verum

end;

dom rr = dom (M * F11) by A93, Th8;
then Sum rr = (a1 . k) * (Sum (M * F11)) by A100, A97, Th10;
then Sum r = (a1 . k) * (M . (F1 . k)) by A95, Th2
.= (a1 . k) * ((M * F1) . k) by A27, A79, A80, FUNCT_1:13 ;
hence p . k = x1 . k by A28, A79, A80, A82; :: thesis: verum

end;

then A102: Sum p = Sum x1 by A79, Th2, FINSEQ_1:13;
ex q being FinSequence of REAL st
( dom q = Seg (len x2) & ( for j being Nat st j in dom q holds
ex s being FinSequence of REAL st
( dom s = Seg (len x1) & q . j = Sum s & ( for i being Nat st i in dom s holds
s . i = a . [i,j] ) ) ) )

proof

defpred S₁[ Nat, object ] means ex s being FinSequence of REAL st
( dom s = Seg (len x1) & $2 = Sum s & ( for i being Nat st i in dom s holds
s . i = a . [i,$1] ) );
A103: for k being Nat st k in Seg (len x2) holds
ex x being object st S₁[k,x]

proof

let k be Nat; :: thesis: ( k in Seg (len x2) implies ex x being object st S₁[k,x] )
assume k in Seg (len x2) ; :: thesis: ex x being object st S₁[k,x]
deffunc H₁( set ) -> set = a . [$1,k];
consider s being FinSequence such that
A104: len s = len x1 and
A105: for i being Nat st i in dom s holds
s . i = H₁(i) from FINSEQ_1:sch 2();
A106: dom s = Seg (len x1) by A104, FINSEQ_1:def 3;
for i being Nat st i in dom s holds
s . i in REAL

proof

let i be Nat; :: thesis: ( i in dom s implies s . i in REAL )
A107: a . [i,k] in REAL by XREAL_0:def 1;
assume i in dom s ; :: thesis: s . i in REAL
hence s . i in REAL by A105, A107; :: thesis: verum

end;

then reconsider s = s as FinSequence of REAL by FINSEQ_2:12;
take x = Sum s; :: thesis: S₁[k,x]
thus S₁[k,x] by A105, A106; :: thesis: verum

end;

consider p being FinSequence such that
A108: ( dom p = Seg (len x2) & ( for k being Nat st k in Seg (len x2) holds
S₁[k,p . k] ) ) from FINSEQ_1:sch 1(A103);
for i being Nat st i in dom p holds
p . i in REAL

proof

let i be Nat; :: thesis: ( i in dom p implies p . i in REAL )
assume i in dom p ; :: thesis: p . i in REAL
then ex s being FinSequence of REAL st
( dom s = Seg (len x1) & p . i = Sum s & ( for j being Nat st j in dom s holds
s . j = a . [j,i] ) ) by A108;
hence p . i in REAL by XREAL_0:def 1; :: thesis: verum

end;

then reconsider p = p as FinSequence of REAL by FINSEQ_2:12;
take p ; :: thesis: ( dom p = Seg (len x2) & ( for j being Nat st j in dom p holds
ex s being FinSequence of REAL st
( dom s = Seg (len x1) & p . j = Sum s & ( for i being Nat st i in dom s holds
s . i = a . [i,j] ) ) ) )
thus ( dom p = Seg (len x2) & ( for j being Nat st j in dom p holds
ex s being FinSequence of REAL st
( dom s = Seg (len x1) & p . j = Sum s & ( for i being Nat st i in dom s holds
s . i = a . [i,j] ) ) ) ) by A108; :: thesis: verum

end;

then consider q being FinSequence of REAL such that
A109: dom q = Seg (len x2) and
A110: for j being Nat st j in dom q holds
ex s being FinSequence of REAL st
( dom s = Seg (len x1) & q . j = Sum s & ( for i being Nat st i in dom s holds
s . i = a . [i,j] ) ) ;
A111: dom q = dom x2 by A109, FINSEQ_1:def 3;
A112: for k being Nat st k in dom q holds
q . k = x2 . k

proof

let k be Nat; :: thesis: ( k in dom q implies q . k = x2 . k )
assume A113: k in dom q ; :: thesis: q . k = x2 . k
then consider s being FinSequence of REAL such that
A114: dom s = Seg (len x1) and
A115: q . k = Sum s and
A116: for i being Nat st i in dom s holds
s . i = a . [i,k] by A110;
reconsider ss = s as FinSequence of ExtREAL by Th11;
ex F21 being Finite_Sep_Sequence of S st
( union (rng F21) = F2 . k & dom F21 = dom s & ( for j being Nat st j in dom s holds
F21 . j = (F1 . j) /\ (F2 . k) ) )

proof

deffunc H₁( set ) -> set = (F2 . k) /\ (F1 . $1);
consider F being FinSequence such that
A117: len F = len x1 and
A118: for i being Nat st i in dom F holds
F . i = H₁(i) from FINSEQ_1:sch 2();
A119: dom F = Seg (len x1) by A117, FINSEQ_1:def 3;
A120: for i being Nat st i in dom F holds
F . i in S

proof

let i be Nat; :: thesis: ( i in dom F implies F . i in S )
assume A121: i in dom F ; :: thesis: F . i in S
then i in Seg (len x1) by A117, FINSEQ_1:def 3;
then i in dom F1 by A27, FINSEQ_1:def 3;
then A122: F1 . i in rng F1 by FUNCT_1:3;
F2 . k in rng F2 by A13, A111, A113, FUNCT_1:3;
then (F1 . i) /\ (F2 . k) in S by A122, MEASURE1:34;
hence F . i in S by A118, A121; :: thesis: verum

end;

A123: dom F = Seg (len x1) by A117, FINSEQ_1:def 3;
reconsider F = F as FinSequence of S by A120, FINSEQ_2:12;
A124: dom F = dom F1 by A27, A123, FINSEQ_1:def 3;
then reconsider F = F as Finite_Sep_Sequence of S by A118, Th5;
take F ; :: thesis: ( union (rng F) = F2 . k & dom F = dom s & ( for j being Nat st j in dom s holds
F . j = (F1 . j) /\ (F2 . k) ) )
union (rng F) = (F2 . k) /\ (union (rng F1)) by A118, A124, Th6
.= (F2 . k) /\ (dom f) by A24
.= (F2 . k) /\ (union (rng F2)) by A10
.= F2 . k by A13, A111, A113, Th7 ;
hence ( union (rng F) = F2 . k & dom F = dom s & ( for j being Nat st j in dom s holds
F . j = (F1 . j) /\ (F2 . k) ) ) by A114, A118, A119; :: thesis: verum

end;

then consider F21 being Finite_Sep_Sequence of S such that
A125: union (rng F21) = F2 . k and
A126: dom F21 = dom s and
A127: for i being Nat st i in dom s holds
F21 . i = (F1 . i) /\ (F2 . k) ;
A128: Sum (M * F21) = M . (F2 . k) by A125, Th9;
A129: for i being Nat st i in dom s holds
s . i = (a1 . i) * (M . ((F1 . i) /\ (F2 . k)))

proof

let i be Nat; :: thesis: ( i in dom s implies s . i = (a1 . i) * (M . ((F1 . i) /\ (F2 . k))) )
assume A130: i in dom s ; :: thesis: s . i = (a1 . i) * (M . ((F1 . i) /\ (F2 . k)))
hence s . i = a . (i,k) by A116
.= (a1 . i) * (M . ((F1 . i) /\ (F2 . k))) by A70, A109, A113, A114, A130 ;
:: thesis: verum

end;

A131: for i being Nat st i in dom s holds
s . i = (a2 . k) * (M . ((F1 . i) /\ (F2 . k)))

proof

let i be Nat; :: thesis: ( i in dom s implies s . i = (a2 . k) * (M . ((F1 . i) /\ (F2 . k))) )
assume A132: i in dom s ; :: thesis: s . i = (a2 . k) * (M . ((F1 . i) /\ (F2 . k)))

now :: thesis: ( ( (F1 . i) /\ (F2 . k) = {} & s . i = (a2 . k) * (M . ((F1 . i) /\ (F2 . k))) ) or ( (F1 . i) /\ (F2 . k) <> {} & s . i = (a2 . k) * (M . ((F1 . i) /\ (F2 . k))) ) )

per cases ( (F1 . i) /\ (F2 . k) = {} or (F1 . i) /\ (F2 . k) <> {} ) ;

case A133: (F1 . i) /\ (F2 . k) = {} ; :: thesis: s . i = (a2 . k) * (M . ((F1 . i) /\ (F2 . k)))

then M . ((F1 . i) /\ (F2 . k)) = 0. by VALUED_0:def 19;
hence s . i = (a1 . i) * 0. by A129, A132
.= 0.
.= (a2 . k) * 0.
.= (a2 . k) * (M . ((F1 . i) /\ (F2 . k))) by A133, VALUED_0:def 19 ;
:: thesis: verum

end;

case (F1 . i) /\ (F2 . k) <> {} ; :: thesis: s . i = (a2 . k) * (M . ((F1 . i) /\ (F2 . k)))

then consider x being object such that
A134: x in (F1 . i) /\ (F2 . k) by XBOOLE_0:def 1;
A135: x in F2 . k by A134, XBOOLE_0:def 4;
A136: dom p = dom x1 by A77, FINSEQ_1:def 3;
x in F1 . i by A134, XBOOLE_0:def 4;
then a1 . i = f . x by A24, A27, A77, A114, A132, A136
.= a2 . k by A10, A13, A111, A113, A135 ;
hence s . i = (a2 . k) * (M . ((F1 . i) /\ (F2 . k))) by A129, A132; :: thesis: verum

end;

end;

end;

hence s . i = (a2 . k) * (M . ((F1 . i) /\ (F2 . k))) ; :: thesis: verum

end;

A137: for j being Nat st j in dom ss holds
ss . j = (a2 . k) * ((M * F21) . j)

proof

let j be Nat; :: thesis: ( j in dom ss implies ss . j = (a2 . k) * ((M * F21) . j) )
assume A138: j in dom ss ; :: thesis: ss . j = (a2 . k) * ((M * F21) . j)
hence ss . j = (a2 . k) * (M . ((F1 . j) /\ (F2 . k))) by A131
.= (a2 . k) * (M . (F21 . j)) by A127, A138
.= (a2 . k) * ((M * F21) . j) by A126, A138, FUNCT_1:13 ;
:: thesis: verum

end;

k in Seg (len a2) by A13, A16, A111, A113, FINSEQ_1:def 3;
then A139: 1 <= k by FINSEQ_1:1;
( a2 . k <> -infty & a2 . k <> +infty )

proof

per cases ( k = 1 or k <> 1 ) ;

suppose k = 1 ; :: thesis: ( a2 . k <> -infty & a2 . k <> +infty )

hence ( a2 . k <> -infty & a2 . k <> +infty ) by A11; :: thesis: verum

end;

suppose k <> 1 ; :: thesis: ( a2 . k <> -infty & a2 . k <> +infty )

then 1 < k by A139, XXREAL_0:1;
then 1 + 1 <= k by NAT_1:13;
hence ( a2 . k <> -infty & a2 . k <> +infty ) by A12, A13, A16, A111, A113; :: thesis: verum

end;

end;

end;

then A140: a2 . k is Element of REAL by XXREAL_0:14;
dom ss = dom (M * F21) by A126, Th8;
then Sum ss = (a2 . k) * (Sum (M * F21)) by A137, A140, Th10;
then Sum s = (a2 . k) * (M . (F2 . k)) by A128, Th2
.= (a2 . k) * ((M * F2) . k) by A13, A111, A113, FUNCT_1:13 ;
hence q . k = x2 . k by A14, A111, A113, A115; :: thesis: verum

end;

Sum p = Sum q by A77, A78, A109, A110, Th1;
hence s1 = s2 by A29, A15, A102, A111, A112, Th2, FINSEQ_1:13; :: thesis: verum

end;

end;

end;

hence s1 = s2 ; :: thesis: verum

end;