let X1, X2 be non empty set ; :: thesis:
let S1 be SigmaField of X1; :: thesis:
let S2 be SigmaField of X2; :: thesis:
let M1 be sigma_Measure of S1; :: thesis:
let M2 be sigma_Measure of S2; :: thesis:
let A be Element of sigma (measurable_rectangles (S1,S2)); :: thesis:
let f be PartFunc of [:X1,X2:],ExtREAL; :: thesis:
assume that
A1: M2 is sigma_finite and
A2: ( f is nonnegative or f is nonpositive ) and
A3: A = dom f and
A4: f is_simple_func_in sigma (measurable_rectangles (S1,S2)) ; :: thesis:
reconsider XX1 = X1 as Element of S1 by MEASURE1:7;
reconsider XX2 = X2 as Element of S2 by MEASURE1:7;
reconsider XX12 = [:X1,X2:] as Element of sigma (measurable_rectangles (S1,S2)) by MEASURE1:7;

per cases ;

suppose f = {} ; :: thesis:

then A5: dom f = {} [:X1,X2:] ;
reconsider E2 = {} as Element of S2 by MEASURE1:7;
reconsider E = {} as Element of S1 by MEASURE1:7;
reconsider I2 = chi (E,X1) as Function of X1,ExtREAL ;
take I2 ; :: thesis:
thus for x being Element of X1 holds I2 . x = Integral (M2,(ProjPMap1 (f,x))) :: thesis:

proof

let x be Element of X1; :: thesis:
dom (ProjPMap1 (f,x)) = X-section ((dom f),x) by Def3;
then A6: dom (ProjPMap1 (f,x)) = E2 by A5, MEASUR11:24;
A7: ProjPMap1 (f,x) is E2 -measurable by A4, Th31, MESFUNC2:34;
M2 . E2 = 0 by VALUED_0:def 19;
then Integral (M2,((ProjPMap1 (f,x)) | E2)) = 0 by A6, A7, MESFUNC5:94;
hence I2 . x = Integral (M2,(ProjPMap1 (f,x))) by A6, FUNCT_3:def 3; :: thesis:

end;

thus for V being Element of S1 holds I2 is V -measurable by MESFUNC2:29; :: thesis:

end;

suppose f <> {} ; :: thesis:

then consider E being non empty Finite_Sep_Sequence of sigma (measurable_rectangles (S1,S2)), a being FinSequence of ExtREAL , r being FinSequence of REAL such that
A8: E,a are_Re-presentation_of f and
A9: for n being Nat holds
( a . n = r . n & f | (E . n) = (chi ((r . n),(E . n),[:X1,X2:])) | (E . n) & ( E . n = {} implies r . n = 0 ) ) by A4, Th5;
defpred S₁[ Nat, object ] means $2 = (r . $1) (#) (Y-vol ((E . $1),M2));
A10: for k being Nat st k in Seg (len E) holds
ex x being Element of Funcs (X1,ExtREAL) st S₁[k,x]

proof

let k be Nat; :: thesis:
assume k in Seg (len E) ; :: thesis:
reconsider x = (r . k) (#) (Y-vol ((E . k),M2)) as Element of Funcs (X1,ExtREAL) by FUNCT_2:8;
take x ; :: thesis:
thus S₁[k,x] ; :: thesis:

end;

consider H being FinSequence of Funcs (X1,ExtREAL) such that
A11: dom H = Seg (len E) and
A12: for n being Nat st n in Seg (len E) holds
S₁[n,H . n] from FINSEQ_1:sch 5(A10);
A13: dom H = dom E by A11, FINSEQ_1:def 3;
A14: ( f is nonnegative implies for n being Nat holds r . n >= 0 )

proof

assume A15: f is nonnegative ; :: thesis:

hereby :: thesis:

let n be Nat; :: thesis:

now :: thesis:

assume A16: E . n <> {} ; :: thesis:
then consider x being object such that
A17: x in E . n by XBOOLE_0:def 1;
n in dom E by A16, FUNCT_1:def 2;
then a . n = f . x by A8, A17, MESFUNC3:def 1;
then a . n >= 0 by A15, SUPINF_2:51;
hence r . n >= 0 by A9; :: thesis:

end;

hence r . n >= 0 by A9; :: thesis:

end;

A18: ( f is nonpositive implies for n being Nat holds r . n <= 0 )

proof

assume A19: f is nonpositive ; :: thesis:

hereby :: thesis:

let n be Nat; :: thesis:

now :: thesis:

assume A20: E . n <> {} ; :: thesis:
then consider x being object such that
A21: x in E . n by XBOOLE_0:def 1;
n in dom E by A20, FUNCT_1:def 2;
then a . n = f . x by A8, A21, MESFUNC3:def 1;
then a . n <= 0 by A19, MESFUNC5:8;
hence r . n <= 0 by A9; :: thesis:

end;

hence r . n <= 0 by A9; :: thesis:

end;

A22: ( f is nonnegative implies H is without_-infty-valued )

proof

assume A6: f is nonnegative ; :: thesis:
for n being Nat st n in dom H holds
H . n is without-infty

proof

let n be Nat; :: thesis:
assume A23: n in dom H ; :: thesis:
then H . n = (r . n) (#) (Y-vol ((E . n),M2)) by A11, A12;
then H . n is nonnegative by A6, A14, MESFUNC5:20;
then H /. n is nonnegative Function of X1,ExtREAL by A23, PARTFUN1:def 6;
hence H . n is without-infty by A23, PARTFUN1:def 6; :: thesis:

end;

hence H is without_-infty-valued ; :: thesis:

end;

A24: ( f is nonpositive implies H is without_+infty-valued )

proof

assume A6: f is nonpositive ; :: thesis:
for n being Nat st n in dom H holds
H . n is without+infty

proof

let n be Nat; :: thesis:
assume A25: n in dom H ; :: thesis:
then H . n = (r . n) (#) (Y-vol ((E . n),M2)) by A11, A12;
then H . n is nonpositive by A6, A18, MESFUNC5:20;
then H /. n is nonpositive Function of X1,ExtREAL by A25, PARTFUN1:def 6;
hence H . n is without+infty by A25, PARTFUN1:def 6; :: thesis:

end;

hence H is without_+infty-valued ; :: thesis:

end;

then reconsider H = H as summable FinSequence of Funcs (X1,ExtREAL) by A2, A22;
A26: ( f is nonnegative implies Partial_Sums H is without_-infty-valued ) by A22, MEASUR11:61;
A27: ( f is nonpositive implies Partial_Sums H is without_+infty-valued ) by A24, MEASUR11:60;
len H = len (Partial_Sums H) by MEASUR11:def 11;
then A28: dom H = dom (Partial_Sums H) by FINSEQ_3:29;
A29: H <> {} by A11;
then A30: len H >= 1 by FINSEQ_1:20;
A31: for x being Element of X1
for n being Nat st n in dom E holds
( (H . n) . x = Integral (M2,(ProjPMap1 ((chi ((r . n),(E . n),[:X1,X2:])),x))) & (H . n) . x = Integral (M2,((r . n) (#) (ProjPMap1 ((chi ((E . n),[:X1,X2:])),x)))) )

proof

let x be Element of X1; :: thesis:
let n be Nat; :: thesis:
assume n in dom E ; :: thesis:
then n in Seg (len E) by FINSEQ_1:def 3;
then H . n = (r . n) (#) (Y-vol ((E . n),M2)) by A12;
hence (H . n) . x = Integral (M2,(ProjPMap1 ((chi ((r . n),(E . n),[:X1,X2:])),x))) by A1, Th56; :: thesis:
then (H . n) . x = Integral (M2,(ProjPMap1 (((r . n) (#) (chi ((E . n),[:X1,X2:]))),x))) by Th1;
hence (H . n) . x = Integral (M2,((r . n) (#) (ProjPMap1 ((chi ((E . n),[:X1,X2:])),x)))) by Th29; :: thesis:

end;

reconsider I2 = (Partial_Sums H) /. (len H) as Function of X1,ExtREAL ;
take I2 ; :: thesis:
for x being Element of X1 holds ((Partial_Sums H) /. (len H)) . x = Integral (M2,(ProjPMap1 (f,x)))

proof

let x be Element of X1; :: thesis:
f is A -measurable by A4, MESFUNC2:34;
then A32: ProjPMap1 (f,x) is Measurable-X-section (A,x) -measurable by A3, Th47;
dom (ProjPMap1 (f,x)) = X-section ((dom f),x) by Def3;
then A33: dom (ProjPMap1 (f,x)) = Measurable-X-section (A,x) by A3, MEASUR11:def 6;
A34: ( ProjPMap1 (f,x) is nonnegative or ProjPMap1 (f,x) is nonpositive ) by A2, Th32, Th33;
A35: for n being Nat holds
( dom ((ProjPMap1 ((chi ((r . n),(E . n),[:X1,X2:])),x)) | (XX2 \ (Measurable-X-section ((E . n),x)))) = XX2 \ (Measurable-X-section ((E . n),x)) & ( ProjPMap1 ((chi ((r . n),(E . n),[:X1,X2:])),x) is nonnegative or ProjPMap1 ((chi ((r . n),(E . n),[:X1,X2:])),x) is nonpositive ) & ProjPMap1 ((chi ((r . n),(E . n),[:X1,X2:])),x) is XX2 -measurable & ( for y being Element of X2 st y in dom ((ProjPMap1 ((chi ((r . n),(E . n),[:X1,X2:])),x)) | (XX2 \ (Measurable-X-section ((E . n),x)))) holds
((ProjPMap1 ((chi ((r . n),(E . n),[:X1,X2:])),x)) | (XX2 \ (Measurable-X-section ((E . n),x)))) . y = 0 ) & Integral (M2,(ProjPMap1 ((chi ((r . n),(E . n),[:X1,X2:])),x))) = Integral (M2,((ProjPMap1 (f,x)) | (Measurable-X-section ((E . n),x)))) & Measurable-X-section ((Union (E | n)),x) misses Measurable-X-section ((E . (n + 1)),x) & Measurable-X-section ((Union (E | (n + 1))),x) = (Measurable-X-section ((Union (E | n)),x)) \/ (Measurable-X-section ((E . (n + 1)),x)) )

proof

let n be Nat; :: thesis:
set pn = ProjPMap1 ((chi ((r . n),(E . n),[:X1,X2:])),x);
set dn = XX2 \ (Measurable-X-section ((E . n),x));
set fn = (ProjPMap1 ((chi ((r . n),(E . n),[:X1,X2:])),x)) | (XX2 \ (Measurable-X-section ((E . n),x)));
ProjPMap1 ((chi ((r . n),(E . n),[:X1,X2:])),x) = ProjMap1 ((chi ((r . n),(E . n),[:X1,X2:])),x) by Th27;
then A36: dom (ProjPMap1 ((chi ((r . n),(E . n),[:X1,X2:])),x)) = XX2 by FUNCT_2:def 1;
hence A37: dom ((ProjPMap1 ((chi ((r . n),(E . n),[:X1,X2:])),x)) | (XX2 \ (Measurable-X-section ((E . n),x)))) = XX2 \ (Measurable-X-section ((E . n),x)) by RELAT_1:62; :: thesis:
A38: chi ((r . n),(E . n),[:X1,X2:]) = (r . n) (#) (chi ((E . n),[:X1,X2:])) by Th1;
ProjPMap1 ((chi ((E . n),[:X1,X2:])),x) = chi ((X-section ((E . n),x)),X2) by Th48;
then ProjPMap1 ((chi ((E . n),[:X1,X2:])),x) = chi ((Measurable-X-section ((E . n),x)),X2) by MEASUR11:def 6;
then A39: ProjPMap1 ((chi ((r . n),(E . n),[:X1,X2:])),x) = (r . n) (#) (chi ((Measurable-X-section ((E . n),x)),X2)) by A38, Th29;
hence A40: ( ProjPMap1 ((chi ((r . n),(E . n),[:X1,X2:])),x) is nonnegative or ProjPMap1 ((chi ((r . n),(E . n),[:X1,X2:])),x) is nonpositive ) by A2, A14, A18, MESFUNC5:20; :: thesis:
dom (chi ((Measurable-X-section ((E . n),x)),X2)) = XX2 by FUNCT_2:def 1;
hence A41: ProjPMap1 ((chi ((r . n),(E . n),[:X1,X2:])),x) is XX2 -measurable by A39, MESFUNC1:37, MESFUNC2:29; :: thesis:
thus for y being Element of X2 st y in dom ((ProjPMap1 ((chi ((r . n),(E . n),[:X1,X2:])),x)) | (XX2 \ (Measurable-X-section ((E . n),x)))) holds
((ProjPMap1 ((chi ((r . n),(E . n),[:X1,X2:])),x)) | (XX2 \ (Measurable-X-section ((E . n),x)))) . y = 0 :: thesis:

proof

let y be Element of X2; :: thesis:
assume A42: y in dom ((ProjPMap1 ((chi ((r . n),(E . n),[:X1,X2:])),x)) | (XX2 \ (Measurable-X-section ((E . n),x)))) ; :: thesis:
then (chi ((Measurable-X-section ((E . n),x)),X2)) . y = 0 by A37, FUNCT_3:37;
then (ProjPMap1 ((chi ((r . n),(E . n),[:X1,X2:])),x)) . y = (r . n) * 0 by A36, A39, MESFUNC1:def 6;
hence ((ProjPMap1 ((chi ((r . n),(E . n),[:X1,X2:])),x)) | (XX2 \ (Measurable-X-section ((E . n),x)))) . y = 0 by A42, FUNCT_1:47; :: thesis:

end;

end;

defpred S₂[ Nat] means ( $1 <= len H implies ((Partial_Sums H) /. $1) . x = Integral (M2,(ProjPMap1 ((f | (union (rng (E | $1)))),x))) );
A44: S₂[1]

proof

assume A45: 1 <= len H ; :: thesis:
then A46: 1 in dom H by FINSEQ_3:25;
len H = len (Partial_Sums H) by MEASUR11:def 11;
then dom H = dom (Partial_Sums H) by FINSEQ_3:29;
then (Partial_Sums H) /. 1 = (Partial_Sums H) . 1 by A45, FINSEQ_3:25, PARTFUN1:def 6;
then (Partial_Sums H) /. 1 = H . 1 by MEASUR11:def 11;
then A47: ((Partial_Sums H) /. 1) . x = Integral (M2,(ProjPMap1 ((chi ((r . 1),(E . 1),[:X1,X2:])),x))) by A13, A31, A46;
E | 1 = <*(E . 1)*> by FINSEQ_5:20;
then rng (E | 1) = {(E . 1)} by FINSEQ_1:39;
then union (rng (E | 1)) = E . 1 by ZFMISC_1:25;
then ProjPMap1 ((f | (union (rng (E | 1)))),x) = ProjPMap1 (((chi ((r . 1),(E . 1),[:X1,X2:])) | (E . 1)),x) by A9;
then ProjPMap1 ((f | (union (rng (E | 1)))),x) = (ProjPMap1 ((chi ((r . 1),(E . 1),[:X1,X2:])),x)) | (X-section ((E . 1),x)) by Th34;
then A48: Integral (M2,(ProjPMap1 ((f | (union (rng (E | 1)))),x))) = Integral (M2,((ProjPMap1 ((chi ((r . 1),(E . 1),[:X1,X2:])),x)) | (Measurable-X-section ((E . 1),x)))) by MEASUR11:def 6;
set p1 = ProjPMap1 ((chi ((r . 1),(E . 1),[:X1,X2:])),x);
set d1 = XX2 \ (Measurable-X-section ((E . 1),x));
set f1 = (ProjPMap1 ((chi ((r . 1),(E . 1),[:X1,X2:])),x)) | (XX2 \ (Measurable-X-section ((E . 1),x)));
A49: ( dom ((ProjPMap1 ((chi ((r . 1),(E . 1),[:X1,X2:])),x)) | (XX2 \ (Measurable-X-section ((E . 1),x)))) = XX2 \ (Measurable-X-section ((E . 1),x)) & ( ProjPMap1 ((chi ((r . 1),(E . 1),[:X1,X2:])),x) is nonnegative or ProjPMap1 ((chi ((r . 1),(E . 1),[:X1,X2:])),x) is nonpositive ) ) by A35;
ProjPMap1 ((chi ((r . 1),(E . 1),[:X1,X2:])),x) = ProjMap1 ((chi ((r . 1),(E . 1),[:X1,X2:])),x) by Th27;
then A50: dom (ProjPMap1 ((chi ((r . 1),(E . 1),[:X1,X2:])),x)) = X2 by FUNCT_2:def 1;
A51: XX2 \ (Measurable-X-section ((E . 1),x)) misses Measurable-X-section ((E . 1),x) by XBOOLE_1:79;
A52: (XX2 \ (Measurable-X-section ((E . 1),x))) \/ (Measurable-X-section ((E . 1),x)) = XX2 by XBOOLE_1:45;
for y being Element of X2 st y in dom ((ProjPMap1 ((chi ((r . 1),(E . 1),[:X1,X2:])),x)) | (XX2 \ (Measurable-X-section ((E . 1),x)))) holds
((ProjPMap1 ((chi ((r . 1),(E . 1),[:X1,X2:])),x)) | (XX2 \ (Measurable-X-section ((E . 1),x)))) . y = 0 by A35;
then Integral (M2,((ProjPMap1 ((chi ((r . 1),(E . 1),[:X1,X2:])),x)) | (XX2 \ (Measurable-X-section ((E . 1),x))))) = 0 by A49, Th57;
then Integral (M2,((ProjPMap1 ((chi ((r . 1),(E . 1),[:X1,X2:])),x)) | ((XX2 \ (Measurable-X-section ((E . 1),x))) \/ (Measurable-X-section ((E . 1),x))))) = (Integral (M2,((ProjPMap1 ((chi ((r . 1),(E . 1),[:X1,X2:])),x)) | (Measurable-X-section ((E . 1),x))))) + 0 by A35, A49, A50, A51, MESFUNC5:91, MESFUN11:62;
hence ((Partial_Sums H) /. 1) . x = Integral (M2,(ProjPMap1 ((f | (union (rng (E | 1)))),x))) by A47, A48, A52, XXREAL_3:4; :: thesis:

end;

A54: for n being non zero Nat st S₂[n] holds
S₂[n + 1]

proof

let n be non zero Nat; :: thesis:
assume A55: S₂[n] ; :: thesis:
assume A56: n + 1 <= len H ; :: thesis:
then n < len H by NAT_1:13;
then A57: ( n <= len (Partial_Sums H) & n + 1 <= len (Partial_Sums H) ) by A56, MEASUR11:def 11;
A58: 1 <= n + 1 by NAT_1:12;
A59: n >= 1 by NAT_1:14;
then A60: ( n in dom (Partial_Sums H) & n + 1 in dom (Partial_Sums H) & n + 1 in dom H ) by A56, A57, NAT_1:12, FINSEQ_3:25;
then A61: ( (Partial_Sums H) /. (n + 1) = (Partial_Sums H) . (n + 1) & (Partial_Sums H) /. n = (Partial_Sums H) . n & H /. (n + 1) = H . (n + 1) ) by PARTFUN1:def 6;
A62: ( ( (Partial_Sums H) /. n is without-infty & H /. (n + 1) is without-infty ) or ( (Partial_Sums H) /. n is without+infty & H /. (n + 1) is without+infty ) )

proof

per cases by A2;

suppose f is nonnegative ; :: thesis:

hence ( ( (Partial_Sums H) /. n is without-infty & H /. (n + 1) is without-infty ) or ( (Partial_Sums H) /. n is without+infty & H /. (n + 1) is without+infty ) ) by A22, A26, A56, A57, A58, A59, A61, FINSEQ_3:25; :: thesis:

end;

suppose f is nonpositive ; :: thesis:

hence ( ( (Partial_Sums H) /. n is without-infty & H /. (n + 1) is without-infty ) or ( (Partial_Sums H) /. n is without+infty & H /. (n + 1) is without+infty ) ) by A24, A27, A56, A57, A58, A59, A61, FINSEQ_3:25; :: thesis:

end;

A63: X-section ((Union (E | n)),x) = Measurable-X-section ((Union (E | n)),x) by MEASUR11:def 6;
(Partial_Sums H) . (n + 1) = ((Partial_Sums H) /. n) + (H /. (n + 1)) by A56, A59, NAT_1:13, MEASUR11:def 11;
then ((Partial_Sums H) . (n + 1)) . x = (((Partial_Sums H) /. n) . x) + ((H /. (n + 1)) . x) by A62, DBLSEQ_3:7;
then ((Partial_Sums H) . (n + 1)) . x = (Integral (M2,(ProjPMap1 ((f | (union (rng (E | n)))),x)))) + (Integral (M2,(ProjPMap1 ((chi ((r . (n + 1)),(E . (n + 1)),[:X1,X2:])),x)))) by A13, A55, A56, A60, A61, A31, NAT_1:13;
then ((Partial_Sums H) . (n + 1)) . x = (Integral (M2,(ProjPMap1 ((f | (Union (E | n))),x)))) + (Integral (M2,(ProjPMap1 ((chi ((r . (n + 1)),(E . (n + 1)),[:X1,X2:])),x)))) by CARD_3:def 4;
then ((Partial_Sums H) . (n + 1)) . x = (Integral (M2,((ProjPMap1 (f,x)) | (X-section ((Union (E | n)),x))))) + (Integral (M2,(ProjPMap1 ((chi ((r . (n + 1)),(E . (n + 1)),[:X1,X2:])),x)))) by Th34;
then ((Partial_Sums H) . (n + 1)) . x = (Integral (M2,((ProjPMap1 (f,x)) | (X-section ((Union (E | n)),x))))) + (Integral (M2,((ProjPMap1 (f,x)) | (Measurable-X-section ((E . (n + 1)),x))))) by A35;
then ((Partial_Sums H) . (n + 1)) . x = Integral (M2,((ProjPMap1 (f,x)) | ((Measurable-X-section ((Union (E | n)),x)) \/ (Measurable-X-section ((E . (n + 1)),x))))) by A32, A33, A34, A35, A63, MESFUNC5:91, MESFUN11:62;
then ((Partial_Sums H) . (n + 1)) . x = Integral (M2,((ProjPMap1 (f,x)) | (Measurable-X-section ((Union (E | (n + 1))),x)))) by A35;
then ((Partial_Sums H) . (n + 1)) . x = Integral (M2,((ProjPMap1 (f,x)) | (X-section ((Union (E | (n + 1))),x)))) by MEASUR11:def 6;
then ((Partial_Sums H) . (n + 1)) . x = Integral (M2,(ProjPMap1 ((f | (Union (E | (n + 1)))),x))) by Th34;
then ((Partial_Sums H) . (n + 1)) . x = Integral (M2,(ProjPMap1 ((f | (union (rng (E | (n + 1))))),x))) by CARD_3:def 4;
hence ((Partial_Sums H) /. (n + 1)) . x = Integral (M2,(ProjPMap1 ((f | (union (rng (E | (n + 1))))),x))) by A60, PARTFUN1:def 6; :: thesis:

end;

len H = len E by A11, FINSEQ_1:def 3;
then E | (len H) = E | (dom E) by FINSEQ_1:def 3;
then union (rng (E | (len H))) = dom f by A8, MESFUNC3:def 1;
then A64: f | (union (rng (E | (len H)))) = f ;
for n being non zero Nat holds S₂[n] from NAT_1:sch 10(A44, A54);
hence ((Partial_Sums H) /. (len H)) . x = Integral (M2,(ProjPMap1 (f,x))) by A29, A64; :: thesis:

end;

hence for x being Element of X1 holds I2 . x = Integral (M2,(ProjPMap1 (f,x))) ; :: thesis:
thus for V being Element of S1 holds I2 is V -measurable :: thesis:

proof

let V be Element of S1; :: thesis:
A65: for n being Nat st n in dom H holds
H /. n is V -measurable

proof

let n be Nat; :: thesis:
assume n in dom H ; :: thesis:
then A66: ( H /. n = H . n & H . n = (r . n) (#) (Y-vol ((E . n),M2)) ) by A11, A12, PARTFUN1:def 6;
A67: dom (Y-vol ((E . n),M2)) = XX1 by FUNCT_2:def 1;
Y-vol ((E . n),M2) is V -measurable by A1, MEASUR11:def 13;
hence H /. n is V -measurable by A66, A67, MESFUNC1:37; :: thesis:

end;

defpred S₂[ Nat] means ( $1 <= len H implies (Partial_Sums H) /. $1 is V -measurable );
(Partial_Sums H) /. 1 = (Partial_Sums H) . 1 by A28, A30, FINSEQ_3:25, PARTFUN1:def 6;
then (Partial_Sums H) /. 1 = H . 1 by MEASUR11:def 11;
then (Partial_Sums H) /. 1 = H /. 1 by A30, A28, FINSEQ_3:25, PARTFUN1:def 6;
then A68: S₂[1] by A65, FINSEQ_3:25;
A69: for n being non zero Nat st S₂[n] holds
S₂[n + 1]

proof

let n be non zero Nat; :: thesis:
assume A70: S₂[n] ; :: thesis:
assume A71: n + 1 <= len H ; :: thesis:
then A72: ( 1 <= n & n < len H ) by NAT_1:13, NAT_1:14;
then A73: ( n in dom H & n + 1 in dom H ) by A71, NAT_1:11, FINSEQ_3:25;
then A74: ( (Partial_Sums H) /. n = (Partial_Sums H) . n & H . (n + 1) = H /. (n + 1) & (Partial_Sums H) /. (n + 1) = (Partial_Sums H) . (n + 1) ) by A28, PARTFUN1:def 6;
then A75: (Partial_Sums H) /. (n + 1) = ((Partial_Sums H) /. n) + (H /. (n + 1)) by A72, MEASUR11:def 11;
A76: ( dom (H /. (n + 1)) = XX1 & dom ((Partial_Sums H) /. n) = XX1 ) by FUNCT_2:def 1;
A77: H /. (n + 1) is V -measurable by A73, A65;

per cases by A2;

suppose f is nonnegative ; :: thesis:

then ( H /. (n + 1) is without-infty & (Partial_Sums H) /. n is without-infty ) by A22, A26, A28, A73, A74;
hence (Partial_Sums H) /. (n + 1) is V -measurable by A70, A71, A75, A77, NAT_1:13, MESFUNC5:31; :: thesis:

end;

suppose f is nonpositive ; :: thesis:

then A78: ( H /. (n + 1) is without+infty & (Partial_Sums H) /. n is without+infty ) by A24, A27, A28, A73, A74;
then dom (((Partial_Sums H) /. n) + (H /. (n + 1))) = (dom ((Partial_Sums H) /. n)) /\ (dom (H /. (n + 1))) by MESFUNC9:1;
hence (Partial_Sums H) /. (n + 1) is V -measurable by A70, A71, A75, A77, A76, A78, NAT_1:13, MEASUR11:65; :: thesis:

end;

for n being non zero Nat holds S₂[n] from NAT_1:sch 10(A68, A69);
hence I2 is V -measurable by A29; :: thesis:

end;