let n be non zero Nat; :: thesis: for X being non-empty n + 1 -element FinSequence
for S being sigmaFieldFamily of X
for M being sigmaMeasureFamily of S
for f being PartFunc of (CarProduct X),ExtREAL st M is sigma_finite & f is_Sequentially_integrable_on M & f is_integrable_on Prod_Measure M holds
for k being non zero Nat st k < n + 1 holds
ex g being PartFunc of (CarProduct (SubFin (X,(k + 1)))),ExtREAL st
( g = (FSqIntg (M,f)) . ((n + 1) - k) & g is_integrable_on Prod_Measure (SubFin (M,(k + 1))) )
let X be non-empty n + 1 -element FinSequence; :: thesis: for S being sigmaFieldFamily of X
for M being sigmaMeasureFamily of S
for f being PartFunc of (CarProduct X),ExtREAL st M is sigma_finite & f is_Sequentially_integrable_on M & f is_integrable_on Prod_Measure M holds
for k being non zero Nat st k < n + 1 holds
ex g being PartFunc of (CarProduct (SubFin (X,(k + 1)))),ExtREAL st
( g = (FSqIntg (M,f)) . ((n + 1) - k) & g is_integrable_on Prod_Measure (SubFin (M,(k + 1))) )
let S be sigmaFieldFamily of X; :: thesis: for M being sigmaMeasureFamily of S
for f being PartFunc of (CarProduct X),ExtREAL st M is sigma_finite & f is_Sequentially_integrable_on M & f is_integrable_on Prod_Measure M holds
for k being non zero Nat st k < n + 1 holds
ex g being PartFunc of (CarProduct (SubFin (X,(k + 1)))),ExtREAL st
( g = (FSqIntg (M,f)) . ((n + 1) - k) & g is_integrable_on Prod_Measure (SubFin (M,(k + 1))) )
let M be sigmaMeasureFamily of S; :: thesis: for f being PartFunc of (CarProduct X),ExtREAL st M is sigma_finite & f is_Sequentially_integrable_on M & f is_integrable_on Prod_Measure M holds
for k being non zero Nat st k < n + 1 holds
ex g being PartFunc of (CarProduct (SubFin (X,(k + 1)))),ExtREAL st
( g = (FSqIntg (M,f)) . ((n + 1) - k) & g is_integrable_on Prod_Measure (SubFin (M,(k + 1))) )
let f be PartFunc of (CarProduct X),ExtREAL; :: thesis: ( M is sigma_finite & f is_Sequentially_integrable_on M & f is_integrable_on Prod_Measure M implies for k being non zero Nat st k < n + 1 holds
ex g being PartFunc of (CarProduct (SubFin (X,(k + 1)))),ExtREAL st
( g = (FSqIntg (M,f)) . ((n + 1) - k) & g is_integrable_on Prod_Measure (SubFin (M,(k + 1))) ) )
assume that
A1: M is sigma_finite and
A2: f is_Sequentially_integrable_on M and
A3: f is_integrable_on Prod_Measure M ; :: thesis: for k being non zero Nat st k < n + 1 holds
ex g being PartFunc of (CarProduct (SubFin (X,(k + 1)))),ExtREAL st
( g = (FSqIntg (M,f)) . ((n + 1) - k) & g is_integrable_on Prod_Measure (SubFin (M,(k + 1))) )
defpred S1[ Nat] means ( 1 <= $1 & $1 < n + 1 implies ex j being non zero Nat ex g being PartFunc of (CarProduct (SubFin (X,(j + 1)))),ExtREAL st
( j = (n + 1) - $1 & g = (FSqIntg (M,f)) . $1 & g is_integrable_on Prod_Measure (SubFin (M,(j + 1))) ) );
A4: ( len X = n + 1 & len S = n + 1 & len M = n + 1 ) by CARD_1:def 7;
A5: S1[1]
proof
assume ( 1 <= 1 & 1 < n + 1 ) ; :: thesis: ex j being non zero Nat ex g being PartFunc of (CarProduct (SubFin (X,(j + 1)))),ExtREAL st
( j = (n + 1) - 1 & g = (FSqIntg (M,f)) . 1 & g is_integrable_on Prod_Measure (SubFin (M,(j + 1))) )
A6: (FSqIntg (M,f)) . 1 = f by Def17;
SubFin (X,(n + 1)) = X | (n + 1) by Def5;
then A7: SubFin (X,(n + 1)) = X by A4, FINSEQ_1:58;
SubFin (S,(n + 1)) = S | (n + 1) by Def6;
then A8: SubFin (S,(n + 1)) = S by A4, FINSEQ_1:58;
SubFin (M,(n + 1)) = M | (n + 1) by Def9;
then SubFin (M,(n + 1)) = M by A4, FINSEQ_1:58;
hence ex j being non zero Nat ex g being PartFunc of (CarProduct (SubFin (X,(j + 1)))),ExtREAL st
( j = (n + 1) - 1 & g = (FSqIntg (M,f)) . 1 & g is_integrable_on Prod_Measure (SubFin (M,(j + 1))) ) by A3, A6, A7, A8; :: thesis: verum
end;
A9: for k being non zero Nat st S1[k] holds
S1[k + 1]
proof
let k be non zero Nat; :: thesis: ( S1[k] implies S1[k + 1] )
assume A10: S1[k] ; :: thesis: S1[k + 1]
assume A11: ( 1 <= k + 1 & k + 1 < n + 1 ) ; :: thesis: ex j being non zero Nat ex g being PartFunc of (CarProduct (SubFin (X,(j + 1)))),ExtREAL st
( j = (n + 1) - (k + 1) & g = (FSqIntg (M,f)) . (k + 1) & g is_integrable_on Prod_Measure (SubFin (M,(j + 1))) )
then consider j being non zero Nat, h being PartFunc of (CarProduct (SubFin (X,(j + 1)))),ExtREAL such that
A12: ( j = (n + 1) - k & h = (FSqIntg (M,f)) . k & h is_integrable_on Prod_Measure (SubFin (M,(j + 1))) ) by A10, NAT_1:12, NAT_1:14;
k < n + 1 by A11, NAT_1:12;
then consider m being non zero Nat, g being PartFunc of [:(CarProduct (SubFin (X,m))),(ElmFin (X,(m + 1))):],ExtREAL such that
A13: ( m = (n + 1) - k & g = (FSqIntg (M,f)) . k & (FSqIntg (M,f)) . (k + 1) = Integral2 ((ElmFin (M,(m + 1))),g) ) by Def17, NAT_1:14;
set I = Integral2 ((ElmFin (M,(m + 1))),g);
set X1 = SubFin (X,(m + 1));
set S1 = SubFin (S,(m + 1));
set M1 = SubFin (M,(m + 1));
A14: (n + 1) - k < (n + 1) - 0 by XREAL_1:15;
then A15: m + 1 <= n + 1 by A13, NAT_1:13;
then ( SubFin (X,(m + 1)) = X | (m + 1) & SubFin (S,(m + 1)) = S | (m + 1) & SubFin (M,(m + 1)) = M | (m + 1) ) by Def5, Def6, Def9;
then A16: ( (SubFin (X,(m + 1))) | m = X | m & (SubFin (S,(m + 1))) | m = S | m & (SubFin (M,(m + 1))) | m = M | m ) by NAT_1:12, FINSEQ_1:82;
A17: ( 1 <= m & m < m + 1 ) by NAT_1:13, NAT_1:14;
then A18: SubFin ((SubFin (X,(m + 1))),m) = SubFin (X,m) by A15, Th7;
A19: SubFin ((SubFin (S,(m + 1))),m) = SubFin (S,m) by A17, A15, Th14;
A20: SubFin ((SubFin (M,(m + 1))),m) = SubFin (M,m) by A17, A15, Th18;
A21: SubFin ((SubFin (X,(m + 1))),m) = (SubFin (X,(m + 1))) | m by Def5, NAT_1:12;
A22: ElmFin ((SubFin (X,(m + 1))),(m + 1)) = ElmFin (X,(m + 1)) by A15, Th8;
then reconsider g0 = g as PartFunc of [:(CarProduct (SubFin ((SubFin (X,(m + 1))),m))),(ElmFin ((SubFin (X,(m + 1))),(m + 1))):],ExtREAL by A21, A16, Def5, A13, A14;
A23: ( CarProduct (SubFin (X,(m + 1))) = [:(CarProduct (SubFin ((SubFin (X,(m + 1))),m))),(ElmFin ((SubFin (X,(m + 1))),(m + 1))):] & Prod_Measure (SubFin (M,(m + 1))) = Prod_Measure ((Prod_Measure (SubFin ((SubFin (M,(m + 1))),m))),(ElmFin ((SubFin (M,(m + 1))),(m + 1)))) ) by Th6, Th28;
A24: Prod_Measure (SubFin ((SubFin (M,(m + 1))),m)) is sigma_finite by A1, A13, A14, A18, A19, A20, Th30, Th29;
A25: ElmFin ((SubFin (S,(m + 1))),(m + 1)) = ElmFin (S,(m + 1)) by A15, Th12;
A26: ElmFin ((SubFin (M,(m + 1))),(m + 1)) = ElmFin (M,(m + 1)) by A15, Th17;
then A27: ElmFin ((SubFin (M,(m + 1))),(m + 1)) is sigma_finite by A1, A15, A22, A25, Th31;
reconsider j1 = (n + 1) - (k + 1) as non zero Nat by A11, NAT_1:21;
reconsider H = Integral2 ((ElmFin (M,(m + 1))),g) as PartFunc of (CarProduct (SubFin (X,(j1 + 1)))),ExtREAL by A13;
consider G0 being PartFunc of (CarProduct (SubFin (X,(m + 1)))),ExtREAL, H0 being PartFunc of (CarProduct (SubFin (X,m))),ExtREAL such that
A28: ( G0 = (FSqIntg (M,f)) . ((n + 1) - m) & H0 = (FSqIntg ((SubFin (M,(m + 1))),|.G0.|)) . 2 & ( for x being Element of CarProduct (SubFin (X,m)) holds H0 . x < +infty ) ) by A13, A14, A2;
set FG0 = FSqIntg ((SubFin (M,(m + 1))),|.G0.|);
A29: (FSqIntg ((SubFin (M,(m + 1))),|.G0.|)) . 1 = |.G0.| by Def17;
1 < m + 1 by NAT_1:13, NAT_1:14;
then A30: ex k1 being non zero Nat ex g1 being PartFunc of [:(CarProduct (SubFin ((SubFin (X,(m + 1))),k1))),(ElmFin ((SubFin (X,(m + 1))),(k1 + 1))):],ExtREAL st
( k1 = (m + 1) - 1 & g1 = (FSqIntg ((SubFin (M,(m + 1))),|.G0.|)) . 1 & (FSqIntg ((SubFin (M,(m + 1))),|.G0.|)) . (1 + 1) = Integral2 ((ElmFin ((SubFin (M,(m + 1))),(k1 + 1))),g1) ) by Def17;
Prod_Field (SubFin (S,(j + 1))) = sigma (measurable_rectangles ((Prod_Field (SubFin (S,m))),(ElmFin (S,(m + 1))))) by A12, A13, A14, Th21;
then A31: Integral2 ((ElmFin ((SubFin (M,(m + 1))),(m + 1))),g0) is_integrable_on Prod_Measure (SubFin ((SubFin (M,(m + 1))),m)) by A12, A13, A19, A18, A25, A22, A23, A24, A27, A28, A29, A30, MESFUN13:32;
H = (FSqIntg (M,f)) . (k + 1) by A13;
hence ex j being non zero Nat ex g being PartFunc of (CarProduct (SubFin (X,(j + 1)))),ExtREAL st
( j = (n + 1) - (k + 1) & g = (FSqIntg (M,f)) . (k + 1) & g is_integrable_on Prod_Measure (SubFin (M,(j + 1))) ) by A13, A22, A25, A26, A18, A19, A20, A31; :: thesis: verum
end;
A32: for k being non zero Nat holds S1[k] from NAT_1:sch 10(A5, A9);
 let k be non zero Nat; :: thesis: ( k < n + 1 implies ex g being PartFunc of (CarProduct (SubFin (X,(k + 1)))),ExtREAL st
( g = (FSqIntg (M,f)) . ((n + 1) - k) & g is_integrable_on Prod_Measure (SubFin (M,(k + 1))) ) )
assume A33: k < n + 1 ; :: thesis: ex g being PartFunc of (CarProduct (SubFin (X,(k + 1)))),ExtREAL st
( g = (FSqIntg (M,f)) . ((n + 1) - k) & g is_integrable_on Prod_Measure (SubFin (M,(k + 1))) )
A34: 1 <= k by NAT_1:14;
set i = (n + 1) - k;
(k + 1) - 1 <= (n + 1) - 1 by A33, NAT_1:13;
then A35: ( (n + 1) - n <= (n + 1) - k & (n + 1) - k <= (n + 1) - 1 ) by A34, XREAL_1:13;
then reconsider i = (n + 1) - k as non zero Nat by INT_1:3, ORDINAL1:def 12;
( 1 <= i & i < n + 1 ) by A35, NAT_1:13;
then ex j being non zero Nat ex g being PartFunc of (CarProduct (SubFin (X,(j + 1)))),ExtREAL st
( j = (n + 1) - i & g = (FSqIntg (M,f)) . i & g is_integrable_on Prod_Measure (SubFin (M,(j + 1))) ) by A32;
hence ex g being PartFunc of (CarProduct (SubFin (X,(k + 1)))),ExtREAL st
( g = (FSqIntg (M,f)) . ((n + 1) - k) & g is_integrable_on Prod_Measure (SubFin (M,(k + 1))) ) ; :: thesis: verum