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: M1 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 E1 = {} as Element of S1 by MEASURE1:7;
reconsider E = {} as Element of S2 by MEASURE1:7;
reconsider I1 = chi (E,X2) as Function of X2,ExtREAL ;
take I1 ; :: thesis:
thus for y being Element of X2 holds I1 . y = Integral (M1,(ProjPMap2 (f,y))) :: thesis:

proof

let y be Element of X2; :: thesis:
dom (ProjPMap2 (f,y)) = Y-section ((dom f),y) by Def4;
then A6: dom (ProjPMap2 (f,y)) = E1 by A5, MEASUR11:24;
A7: ProjPMap2 (f,y) is E1 -measurable by A4, Th31, MESFUNC2:34;
M1 . E1 = 0 by VALUED_0:def 19;
then Integral (M1,((ProjPMap2 (f,y)) | E1)) = 0 by A6, A7, MESFUNC5:94;
hence I1 . y = Integral (M1,(ProjPMap2 (f,y))) by A6, FUNCT_3:def 3; :: thesis:

end;

thus for V being Element of S2 holds I1 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) (#) (X-vol ((E . $1),M1));
A10: for k being Nat st k in Seg (len E) holds
ex x being Element of Funcs (X2,ExtREAL) st S₁[k,x]

proof

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

end;

consider H being FinSequence of Funcs (X2,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) (#) (X-vol ((E . n),M1)) by A11, A12;
then H . n is nonnegative by A6, A14, MESFUNC5:20;
then H /. n is V112() Function of X2,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) (#) (X-vol ((E . n),M1)) by A11, A12;
then H . n is nonpositive by A6, A18, MESFUNC5:20;
then H /. n is nonpositive Function of X2,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 (X2,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 y being Element of X2
for n being Nat st n in dom E holds
( (H . n) . y = Integral (M1,(ProjPMap2 ((chi ((r . n),(E . n),[:X1,X2:])),y))) & (H . n) . y = Integral (M1,((r . n) (#) (ProjPMap2 ((chi ((E . n),[:X1,X2:])),y)))) )

proof

let y be Element of X2; :: 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) (#) (X-vol ((E . n),M1)) by A12;
hence (H . n) . y = Integral (M1,(ProjPMap2 ((chi ((r . n),(E . n),[:X1,X2:])),y))) by A1, Th55; :: thesis:
then (H . n) . y = Integral (M1,(ProjPMap2 (((r . n) (#) (chi ((E . n),[:X1,X2:]))),y))) by Th1;
hence (H . n) . y = Integral (M1,((r . n) (#) (ProjPMap2 ((chi ((E . n),[:X1,X2:])),y)))) by Th29; :: thesis:

end;

reconsider I1 = (Partial_Sums H) /. (len H) as Function of X2,ExtREAL ;
take I1 ; :: thesis:
for y being Element of X2 holds ((Partial_Sums H) /. (len H)) . y = Integral (M1,(ProjPMap2 (f,y)))

proof

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

proof

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

proof

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

end;

end;

defpred S₂[ Nat] means ( $1 <= len H implies ((Partial_Sums H) /. $1) . y = Integral (M1,(ProjPMap2 ((f | (union (rng (E | $1)))),y))) );
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) . y = Integral (M1,(ProjPMap2 ((chi ((r . 1),(E . 1),[:X1,X2:])),y))) 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 ProjPMap2 ((f | (union (rng (E | 1)))),y) = ProjPMap2 (((chi ((r . 1),(E . 1),[:X1,X2:])) | (E . 1)),y) by A9;
then ProjPMap2 ((f | (union (rng (E | 1)))),y) = (ProjPMap2 ((chi ((r . 1),(E . 1),[:X1,X2:])),y)) | (Y-section ((E . 1),y)) by Th34;
then A48: Integral (M1,(ProjPMap2 ((f | (union (rng (E | 1)))),y))) = Integral (M1,((ProjPMap2 ((chi ((r . 1),(E . 1),[:X1,X2:])),y)) | (Measurable-Y-section ((E . 1),y)))) by MEASUR11:def 7;
set p1 = ProjPMap2 ((chi ((r . 1),(E . 1),[:X1,X2:])),y);
set d1 = XX1 \ (Measurable-Y-section ((E . 1),y));
set f1 = (ProjPMap2 ((chi ((r . 1),(E . 1),[:X1,X2:])),y)) | (XX1 \ (Measurable-Y-section ((E . 1),y)));
A49: ( dom ((ProjPMap2 ((chi ((r . 1),(E . 1),[:X1,X2:])),y)) | (XX1 \ (Measurable-Y-section ((E . 1),y)))) = XX1 \ (Measurable-Y-section ((E . 1),y)) & ( ProjPMap2 ((chi ((r . 1),(E . 1),[:X1,X2:])),y) is nonnegative or ProjPMap2 ((chi ((r . 1),(E . 1),[:X1,X2:])),y) is nonpositive ) ) by A35;
ProjPMap2 ((chi ((r . 1),(E . 1),[:X1,X2:])),y) = ProjMap2 ((chi ((r . 1),(E . 1),[:X1,X2:])),y) by Th27;
then A50: dom (ProjPMap2 ((chi ((r . 1),(E . 1),[:X1,X2:])),y)) = X1 by FUNCT_2:def 1;
A51: XX1 \ (Measurable-Y-section ((E . 1),y)) misses Measurable-Y-section ((E . 1),y) by XBOOLE_1:79;
A52: (XX1 \ (Measurable-Y-section ((E . 1),y))) \/ (Measurable-Y-section ((E . 1),y)) = XX1 by XBOOLE_1:45;
for x being Element of X1 st x in dom ((ProjPMap2 ((chi ((r . 1),(E . 1),[:X1,X2:])),y)) | (XX1 \ (Measurable-Y-section ((E . 1),y)))) holds
((ProjPMap2 ((chi ((r . 1),(E . 1),[:X1,X2:])),y)) | (XX1 \ (Measurable-Y-section ((E . 1),y)))) . x = 0 by A35;
then Integral (M1,((ProjPMap2 ((chi ((r . 1),(E . 1),[:X1,X2:])),y)) | (XX1 \ (Measurable-Y-section ((E . 1),y))))) = 0 by A49, Th57;
then Integral (M1,((ProjPMap2 ((chi ((r . 1),(E . 1),[:X1,X2:])),y)) | ((XX1 \ (Measurable-Y-section ((E . 1),y))) \/ (Measurable-Y-section ((E . 1),y))))) = (Integral (M1,((ProjPMap2 ((chi ((r . 1),(E . 1),[:X1,X2:])),y)) | (Measurable-Y-section ((E . 1),y))))) + 0 by A35, A49, A50, A51, MESFUNC5:91, MESFUN11:62;
hence ((Partial_Sums H) /. 1) . y = Integral (M1,(ProjPMap2 ((f | (union (rng (E | 1)))),y))) 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 V120() & H /. (n + 1) is V120() ) or ( (Partial_Sums H) /. n is V121() & H /. (n + 1) is V121() ) )

proof

per cases by A2;

suppose f is nonnegative ; :: thesis:

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

end;

suppose f is nonpositive ; :: thesis:

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

end;

A63: Y-section ((Union (E | n)),y) = Measurable-Y-section ((Union (E | n)),y) by MEASUR11:def 7;
(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)) . y = (((Partial_Sums H) /. n) . y) + ((H /. (n + 1)) . y) by A62, DBLSEQ_3:7;
then ((Partial_Sums H) . (n + 1)) . y = (Integral (M1,(ProjPMap2 ((f | (union (rng (E | n)))),y)))) + (Integral (M1,(ProjPMap2 ((chi ((r . (n + 1)),(E . (n + 1)),[:X1,X2:])),y)))) by A13, A55, A56, A60, A61, A31, NAT_1:13;
then ((Partial_Sums H) . (n + 1)) . y = (Integral (M1,(ProjPMap2 ((f | (Union (E | n))),y)))) + (Integral (M1,(ProjPMap2 ((chi ((r . (n + 1)),(E . (n + 1)),[:X1,X2:])),y)))) by CARD_3:def 4;
then ((Partial_Sums H) . (n + 1)) . y = (Integral (M1,((ProjPMap2 (f,y)) | (Y-section ((Union (E | n)),y))))) + (Integral (M1,(ProjPMap2 ((chi ((r . (n + 1)),(E . (n + 1)),[:X1,X2:])),y)))) by Th34;
then ((Partial_Sums H) . (n + 1)) . y = (Integral (M1,((ProjPMap2 (f,y)) | (Y-section ((Union (E | n)),y))))) + (Integral (M1,((ProjPMap2 (f,y)) | (Measurable-Y-section ((E . (n + 1)),y))))) by A35;
then ((Partial_Sums H) . (n + 1)) . y = Integral (M1,((ProjPMap2 (f,y)) | ((Measurable-Y-section ((Union (E | n)),y)) \/ (Measurable-Y-section ((E . (n + 1)),y))))) by A32, A33, A34, A35, A63, MESFUNC5:91, MESFUN11:62;
then ((Partial_Sums H) . (n + 1)) . y = Integral (M1,((ProjPMap2 (f,y)) | (Measurable-Y-section ((Union (E | (n + 1))),y)))) by A35;
then ((Partial_Sums H) . (n + 1)) . y = Integral (M1,((ProjPMap2 (f,y)) | (Y-section ((Union (E | (n + 1))),y)))) by MEASUR11:def 7;
then ((Partial_Sums H) . (n + 1)) . y = Integral (M1,(ProjPMap2 ((f | (Union (E | (n + 1)))),y))) by Th34;
then ((Partial_Sums H) . (n + 1)) . y = Integral (M1,(ProjPMap2 ((f | (union (rng (E | (n + 1))))),y))) by CARD_3:def 4;
hence ((Partial_Sums H) /. (n + 1)) . y = Integral (M1,(ProjPMap2 ((f | (union (rng (E | (n + 1))))),y))) 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)) . y = Integral (M1,(ProjPMap2 (f,y))) by A29, A64; :: thesis:

end;

hence for y being Element of X2 holds I1 . y = Integral (M1,(ProjPMap2 (f,y))) ; :: thesis:
thus for V being Element of S2 holds I1 is V -measurable :: thesis:

proof

let V be Element of S2; :: 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) (#) (X-vol ((E . n),M1)) ) by A11, A12, PARTFUN1:def 6;
A67: dom (X-vol ((E . n),M1)) = XX2 by FUNCT_2:def 1;
X-vol ((E . n),M1) is V -measurable by A1, MEASUR11:def 14;
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)) = XX2 & dom ((Partial_Sums H) /. n) = XX2 ) 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 V120() & (Partial_Sums H) /. n is V120() ) 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 V121() & (Partial_Sums H) /. n is V121() ) 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 I1 is V -measurable by A29; :: thesis:

end;