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, Def1;
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

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:3;
then 1 < n by A19, XXREAL_0:1;
then 1 + 1 < n + 1 by XREAL_1:10;
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:12, FUNCT_1:23;
hence 0. <= (M * F2) . n by SUPINF_2:58; :: thesis: verum

end;

A21: for n being Nat st n in dom x2 holds
0. <= x2 . n

proof

let n be Nat; :: thesis: ( n in dom x2 implies 0. <= x2 . n )
assume A22: n in dom x2 ; :: thesis: 0. <= x2 . n
then ( 0. <= a2 . n & 0. <= (M * F2) . n ) by A13, A16, A20, A17;
then 0. <= (a2 . n) * ((M * F2) . n) ;
hence 0. <= x2 . n by A14, A22; :: thesis: verum

end;

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

now

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

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

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

end;

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

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

end;

end;

end;

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

end;

A33: 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:12, FUNCT_1:23;
hence 0. <= (M * F1) . n by SUPINF_2:58; :: thesis: verum

end;

A34: for n being Nat st n in dom x1 holds
0. <= x1 . n

proof

let n be Nat; :: thesis: ( n in dom x1 implies 0. <= x1 . n )
assume A35: n in dom x1 ; :: thesis: 0. <= x1 . n
then ( 0. <= a1 . n & 0. <= (M * F1) . n ) by A26, A29, A33, A30;
then 0. <= (a1 . n) * ((M * F1) . n) ;
hence 0. <= x1 . n by A27, A35; :: thesis: verum

end;

now

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
A36: i in dom F1 and
A37: j in dom F2 and
A38: 2 <= i and
A39: 2 <= j and
A40: M . ((F1 . i) /\ (F2 . j)) = +infty ;
A41: F2 . j in rng F2 by A37, FUNCT_1:12;
A42: F1 . i in rng F1 by A36, FUNCT_1:12;
then A43: (F1 . i) /\ (F2 . j) in S by A41, MEASURE1:66;
(F1 . i) /\ (F2 . j) c= F1 . i by XBOOLE_1:17;
then M . (F1 . i) = +infty by A40, A42, A43, MEASURE1:62, XXREAL_0:4;
then A44: (M * F1) . i = +infty by A36, FUNCT_1:23;
0. < a1 . i by A25, A29, A36, A38;
then +infty = (a1 . i) * ((M * F1) . i) by A44, XXREAL_3:def 5;
then x1 . i = +infty by A26, A27, A36;
then A45: Sum x1 = +infty by A26, A34, A36, Th17;
(F1 . i) /\ (F2 . j) c= F2 . j by XBOOLE_1:17;
then M . (F2 . j) = +infty by A40, A41, A43, MEASURE1:62, XXREAL_0:4;
then A46: (M * F2) . j = +infty by A37, FUNCT_1:23;
0. < a2 . j by A12, A16, A37, A39;
then +infty = (a2 . j) * ((M * F2) . j) by A46, XXREAL_3:def 5;
then x2 . j = +infty by A13, A14, A37;
hence s1 = s2 by A28, A13, A15, A21, A37, A45, Th17; :: thesis: verum

end;

case A47: 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₁( set , set ) -> Element of ExtREAL = (a1 . $1) * (M . ((F1 . $1) /\ (F2 . $2)));
A48: for x, y being set st x in Seg (len x1) & y in Seg (len x2) holds
H₁(x,y) in REAL

proof

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

now

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

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

now

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

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

then kx <= 1 + 1 ;
then kx <= 1 by A60, NAT_1:8;
then H₁(kx,ky) = 0. * (M . ((F1 . kx) /\ (F2 . ky))) by A24, A52, XXREAL_0:1
.= 0 ;
hence H₁(kx,ky) in REAL ; :: thesis: verum

end;

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

then ky <= 1 + 1 ;
then A62: ky <= 1 by A61, NAT_1:8;

now

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 set such that
A63: x in (F1 . kx) /\ (F2 . ky) by XBOOLE_0:def 1;
A64: x in F2 . ky by A63, XBOOLE_0:def 4;
x in F1 . kx by A63, XBOOLE_0:def 4;
then a1 . kx = f . x by A23, A57, Def1
.= a2 . ky by A10, A55, A64, Def1
.= 0. by A11, A54, A62, XXREAL_0:1 ;
hence H₁(kx,ky) = 0 ; :: thesis: verum

end;

end;

end;

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

end;

end;

end;

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

end;

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

A66: 0. <= a1 . kx by A29, A30, A57;
a1 . kx <> +infty by A25, A29, A57, A65;
then reconsider r2 = a1 . kx as Real by A66, XXREAL_0:14;
0. <= M . ((F1 . kx) /\ (F2 . ky)) by A58, SUPINF_2:58;
then reconsider r3 = M . ((F1 . kx) /\ (F2 . ky)) as Real by A47, A57, A55, A65, XXREAL_0:14;
(a1 . kx) * (M . ((F1 . kx) /\ (F2 . ky))) = r2 * r3 by EXTREAL1:13;
hence H₁(kx,ky) in REAL ; :: thesis: verum

end;

end;

end;

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

end;

consider f being Function of [:(Seg (len x1)),(Seg (len x2)):],REAL such that
A67: for x, y being set st x in Seg (len x1) & y in Seg (len x2) holds
f . x,y = H₁(x,y) from BINOP_1:sch 2(A48);
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 A67; :: thesis: verum

end;

then consider a being Function of [:(Seg (len x1)),(Seg (len x2)):],REAL such that
A68: 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, set ] 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] ) );
A69: for k being Nat st k in Seg (len x1) holds
ex x being set st S₁[k,x]

proof

let k be Nat; :: thesis: ( k in Seg (len x1) implies ex x being set st S₁[k,x] )
assume k in Seg (len x1) ; :: thesis: ex x being set st S₁[k,x]
deffunc H₁( set ) -> Element of REAL = a . [k,$1];
consider r being FinSequence such that
A70: len r = len x2 and
A71: for i being Nat st i in dom r holds
r . i = H₁(i) from FINSEQ_1:sch 2();
A72: dom r = Seg (len x2) by A70, 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 )
A73: a . [k,i] in REAL ;
assume i in dom r ; :: thesis: r . i in REAL
hence r . i in REAL by A71, A73; :: thesis: verum

end;

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

end;

consider p being FinSequence such that
A74: ( 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(A69);
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 A74;
hence p . i in REAL ; :: thesis: verum

end;

then reconsider p = p as FinSequence of REAL by FINSEQ_2:14;
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 A74; :: thesis: verum

end;

then consider p being FinSequence of REAL such that
A75: dom p = Seg (len x1) and
A76: 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] ) ) ;
A77: dom p = dom x1 by A75, 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 A78: k in dom p ; :: thesis: p . k = x1 . k
then consider r being FinSequence of REAL such that
A79: dom r = Seg (len x2) and
A80: p . k = Sum r and
A81: for j being Nat st j in dom r holds
r . j = a . [k,j] by A76;
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
A82: len F = len x2 and
A83: for i being Nat st i in dom F holds
F . i = H₁(i) from FINSEQ_1:sch 2();
A84: dom F = Seg (len x2) by A82, FINSEQ_1:def 3;
A85: 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 A86: i in dom F ; :: thesis: F . i in S
then i in Seg (len x2) by A82, FINSEQ_1:def 3;
then i in dom F2 by A13, FINSEQ_1:def 3;
then A87: F2 . i in rng F2 by FUNCT_1:12;
F1 . k in rng F1 by A26, A77, A78, FUNCT_1:12;
then (F1 . k) /\ (F2 . i) in S by A87, MEASURE1:66;
hence F . i in S by A83, A86; :: thesis: verum

end;

A88: dom F = Seg (len x2) by A82, FINSEQ_1:def 3;
reconsider F = F as FinSequence of S by A85, FINSEQ_2:14;
A89: dom F = dom F2 by A13, A88, FINSEQ_1:def 3;
then reconsider F = F as Finite_Sep_Sequence of S by A83, 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 A83, A89, Th6
.= (F1 . k) /\ (dom f) by A10, Def1
.= (F1 . k) /\ (union (rng F1)) by A23, Def1
.= F1 . k by A26, A77, A78, 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 A79, A83, A84; :: thesis: verum

end;

then consider F11 being Finite_Sep_Sequence of S such that
A90: union (rng F11) = F1 . k and
A91: dom F11 = dom r and
A92: for j being Nat st j in dom r holds
F11 . j = (F1 . k) /\ (F2 . j) ;
A93: Sum (M * F11) = M . (F1 . k) by A90, Th9;
k in Seg (len a1) by A26, A29, A77, A78, FINSEQ_1:def 3;
then A94: 1 <= k by FINSEQ_1:3;
( 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 A24; :: thesis: verum

end;

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

then 1 < k by A94, XXREAL_0:1;
then 1 + 1 <= k by NAT_1:13;
hence ( a1 . k <> -infty & a1 . k <> +infty ) by A25, A26, A29, A77, A78; :: thesis: verum

end;

end;

end;

then A95: a1 . k is Element of REAL by XXREAL_0:14;
reconsider rr = r as FinSequence of ExtREAL by Th11;
A96: 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 A97: j in dom r ; :: thesis: r . j = (a1 . k) * (M . ((F1 . k) /\ (F2 . j)))
hence r . j = a . k,j by A81
.= (a1 . k) * (M . ((F1 . k) /\ (F2 . j))) by A68, A75, A78, A79, A97 ;
:: thesis: verum

end;

A98: 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 A99: j in dom rr ; :: thesis: rr . j = (a1 . k) * ((M * F11) . j)
hence rr . j = (a1 . k) * (M . ((F1 . k) /\ (F2 . j))) by A96
.= (a1 . k) * (M . (F11 . j)) by A92, A99
.= (a1 . k) * ((M * F11) . j) by A91, A99, FUNCT_1:23 ;
:: thesis: verum

end;

dom rr = dom (M * F11) by A91, Th8;
then Sum rr = (a1 . k) * (Sum (M * F11)) by A98, A95, Th10;
then Sum r = (a1 . k) * (M . (F1 . k)) by A93, Th2
.= (a1 . k) * ((M * F1) . k) by A26, A77, A78, FUNCT_1:23 ;
hence p . k = x1 . k by A27, A77, A78, A80; :: thesis: verum

end;

then A100: Sum p = Sum x1 by A77, Th2, FINSEQ_1:17;
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, set ] 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] ) );
A101: for k being Nat st k in Seg (len x2) holds
ex x being set st S₁[k,x]

proof

let k be Nat; :: thesis: ( k in Seg (len x2) implies ex x being set st S₁[k,x] )
assume k in Seg (len x2) ; :: thesis: ex x being set st S₁[k,x]
deffunc H₁( set ) -> Element of REAL = a . [$1,k];
consider s being FinSequence such that
A102: len s = len x1 and
A103: for i being Nat st i in dom s holds
s . i = H₁(i) from FINSEQ_1:sch 2();
A104: dom s = Seg (len x1) by A102, 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 )
A105: a . [i,k] in REAL ;
assume i in dom s ; :: thesis: s . i in REAL
hence s . i in REAL by A103, A105; :: thesis: verum

end;

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

end;

consider p being FinSequence such that
A106: ( 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(A101);
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 A106;
hence p . i in REAL ; :: thesis: verum

end;

then reconsider p = p as FinSequence of REAL by FINSEQ_2:14;
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 A106; :: thesis: verum

end;

then consider q being FinSequence of REAL such that
A107: dom q = Seg (len x2) and
A108: 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] ) ) ;
A109: dom q = dom x2 by A107, FINSEQ_1:def 3;
A110: 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 A111: k in dom q ; :: thesis: q . k = x2 . k
then consider s being FinSequence of REAL such that
A112: dom s = Seg (len x1) and
A113: q . k = Sum s and
A114: for i being Nat st i in dom s holds
s . i = a . [i,k] by A108;
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
A115: len F = len x1 and
A116: for i being Nat st i in dom F holds
F . i = H₁(i) from FINSEQ_1:sch 2();
A117: dom F = Seg (len x1) by A115, FINSEQ_1:def 3;
A118: 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 A119: i in dom F ; :: thesis: F . i in S
then i in Seg (len x1) by A115, FINSEQ_1:def 3;
then i in dom F1 by A26, FINSEQ_1:def 3;
then A120: F1 . i in rng F1 by FUNCT_1:12;
F2 . k in rng F2 by A13, A109, A111, FUNCT_1:12;
then (F1 . i) /\ (F2 . k) in S by A120, MEASURE1:66;
hence F . i in S by A116, A119; :: thesis: verum

end;

A121: dom F = Seg (len x1) by A115, FINSEQ_1:def 3;
reconsider F = F as FinSequence of S by A118, FINSEQ_2:14;
A122: dom F = dom F1 by A26, A121, FINSEQ_1:def 3;
then reconsider F = F as Finite_Sep_Sequence of S by A116, 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 A116, A122, Th6
.= (F2 . k) /\ (dom f) by A23, Def1
.= (F2 . k) /\ (union (rng F2)) by A10, Def1
.= F2 . k by A13, A109, A111, 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 A112, A116, A117; :: thesis: verum

end;

then consider F21 being Finite_Sep_Sequence of S such that
A123: union (rng F21) = F2 . k and
A124: dom F21 = dom s and
A125: for i being Nat st i in dom s holds
F21 . i = (F1 . i) /\ (F2 . k) ;
A126: Sum (M * F21) = M . (F2 . k) by A123, Th9;
A127: 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 A128: i in dom s ; :: thesis: s . i = (a1 . i) * (M . ((F1 . i) /\ (F2 . k)))
hence s . i = a . i,k by A114
.= (a1 . i) * (M . ((F1 . i) /\ (F2 . k))) by A68, A107, A111, A112, A128 ;
:: thesis: verum

end;

A129: 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 A130: i in dom s ; :: thesis: s . i = (a2 . k) * (M . ((F1 . i) /\ (F2 . k)))

now

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

case A131: (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 A127, A130
.= 0.
.= (a2 . k) * 0.
.= (a2 . k) * (M . ((F1 . i) /\ (F2 . k))) by A131, 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 set such that
A132: x in (F1 . i) /\ (F2 . k) by XBOOLE_0:def 1;
A133: x in F2 . k by A132, XBOOLE_0:def 4;
A134: dom p = dom x1 by A75, FINSEQ_1:def 3;
x in F1 . i by A132, XBOOLE_0:def 4;
then a1 . i = f . x by A23, A26, A75, A112, A130, A134, Def1
.= a2 . k by A10, A13, A109, A111, A133, Def1 ;
hence s . i = (a2 . k) * (M . ((F1 . i) /\ (F2 . k))) by A127, A130; :: thesis: verum

end;

end;

end;

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

end;

A135: 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 A136: j in dom ss ; :: thesis: ss . j = (a2 . k) * ((M * F21) . j)
hence ss . j = (a2 . k) * (M . ((F1 . j) /\ (F2 . k))) by A129
.= (a2 . k) * (M . (F21 . j)) by A125, A136
.= (a2 . k) * ((M * F21) . j) by A124, A136, FUNCT_1:23 ;
:: thesis: verum

end;

k in Seg (len a2) by A13, A16, A109, A111, FINSEQ_1:def 3;
then A137: 1 <= k by FINSEQ_1:3;
( 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 A137, XXREAL_0:1;
then 1 + 1 <= k by NAT_1:13;
hence ( a2 . k <> -infty & a2 . k <> +infty ) by A12, A13, A16, A109, A111; :: thesis: verum

end;

end;

end;

then A138: a2 . k is Element of REAL by XXREAL_0:14;
dom ss = dom (M * F21) by A124, Th8;
then Sum ss = (a2 . k) * (Sum (M * F21)) by A135, A138, Th10;
then Sum s = (a2 . k) * (M . (F2 . k)) by A126, Th2
.= (a2 . k) * ((M * F2) . k) by A13, A109, A111, FUNCT_1:23 ;
hence q . k = x2 . k by A14, A109, A111, A113; :: thesis: verum

end;

Sum p = Sum q by A75, A76, A107, A108, Th1;
hence s1 = s2 by A28, A15, A100, A109, A110, Th2, FINSEQ_1:17; :: thesis: verum

end;

end;

end;

hence s1 = s2 ; :: thesis: verum

end;