let n be non zero Nat; :: thesis:
let X be non-empty n + 1 -element FinSequence; :: thesis:
let S be sigmaFieldFamily of X; :: thesis:
let M be sigmaMeasureFamily of S; :: thesis:
let f be PartFunc of (CarProduct X),ExtREAL; :: thesis:
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:
let k be non zero Nat; :: thesis:
assume A4: k < n ; :: thesis:
then A5: ( 1 <= k & k < n + 1 ) by NAT_1:13, NAT_1:14;
then k - k < (n + 1) - k by XREAL_1:14;
then (n + 1) - k in NAT by INT_1:3;
then reconsider m = (n + 1) - k as non zero Nat by A4, NAT_1:12;
set Mk1 = SubFin (M,(k + 1));
set Sk1 = SubFin (S,(k + 1));
set Xk1 = SubFin (X,(k + 1));
set Xk = SubFin (X,k);
1 - k <= 0 by NAT_1:14, XREAL_1:47;
then n + (1 - k) <= n + 0 by XREAL_1:7;
then ( 1 <= m & m < n + 1 ) by NAT_1:13, NAT_1:14;
then ex j being non zero Nat ex g being PartFunc of [:(CarProduct (SubFin (X,j))),(ElmFin (X,(j + 1))):],ExtREAL st
( j = (n + 1) - m & g = (FSqIntg (M,f)) . m & (FSqIntg (M,f)) . (m + 1) = Integral2 ((ElmFin (M,(j + 1))),g) ) by Def17;
then consider Fk1 being PartFunc of [:(CarProduct (SubFin (X,k))),(ElmFin (X,(k + 1))):],ExtREAL such that
A6: ( k = (n + 1) - m & Fk1 = (FSqIntg (M,f)) . ((n + 1) - k) & (FSqIntg (M,f)) . (m + 1) = Integral2 ((ElmFin (M,(k + 1))),Fk1) ) ;
A7: k <= k + 1 by NAT_1:12;
A8: k + 1 <= n + 1 by A4, XREAL_1:7;
then A9: SubFin (X,k) = SubFin ((SubFin (X,(k + 1))),k) by A7, Th7;
A10: ElmFin (X,(k + 1)) = ElmFin ((SubFin (X,(k + 1))),(k + 1)) by A8, Th8;
A11: SubFin (S,k) = SubFin ((SubFin (S,(k + 1))),k) by A7, A8, Th14;
A12: ElmFin (S,(k + 1)) = ElmFin ((SubFin (S,(k + 1))),(k + 1)) by A8, Th12;
A13: SubFin (M,k) = SubFin ((SubFin (M,(k + 1))),k) by A7, A8, Th18;
A14: ElmFin (M,(k + 1)) = ElmFin ((SubFin (M,(k + 1))),(k + 1)) by A8, Th17;
A15: SubFin (X,(k + 1)) = SubFin ((SubFin (X,(k + 1))),(k + 1)) by A8, Th7;
A16: SubFin (S,(k + 1)) = SubFin ((SubFin (S,(k + 1))),(k + 1)) by A8, Th14;
A17: SubFin (M,(k + 1)) = SubFin ((SubFin (M,(k + 1))),(k + 1)) by A8, Th18;
reconsider F2k1 = Fk1 as PartFunc of [:(CarProduct (SubFin ((SubFin (X,(k + 1))),k))),(ElmFin ((SubFin (X,(k + 1))),(k + 1))):],ExtREAL by A9, A8, Th8;
reconsider Fk = Integral2 ((ElmFin (M,(k + 1))),Fk1) as Function of (CarProduct (SubFin (X,k))),ExtREAL ;
A18: SubFin (M,(k + 1)) is sigma_finite by A1, A4, Th30, XREAL_1:7;
consider Gk1 being PartFunc of (CarProduct (SubFin (X,(k + 1)))),ExtREAL, Hk being PartFunc of (CarProduct (SubFin (X,k))),ExtREAL such that
A19: ( Gk1 = (FSqIntg (M,f)) . ((n + 1) - k) & Hk = (FSqIntg ((SubFin (M,(k + 1))),|.Gk1.|)) . 2 & ( for x being Element of CarProduct (SubFin (X,k)) holds Hk . x < +infty ) ) by A2, A5;
A20: 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))) ) by Th38, A5, A1, A2, A3;
reconsider Gk2 = Gk1 as PartFunc of (CarProduct (SubFin ((SubFin (X,(k + 1))),(k + 1)))),ExtREAL by A8, Th7;
take Fk1 ; :: thesis:
take Gk1 ; :: thesis:
take Fk ; :: thesis:
thus Gk1 = Fk1 by A6, A19; :: thesis:
thus Gk1 = (FSqIntg (M,f)) . ((n + 1) - k) by A19; :: thesis:
thus Fk = (FSqIntg (M,f)) . ((n + 1) - (k - 1)) by A6; :: thesis:
thus Fk = Integral2 ((ElmFin (M,(k + 1))),Fk1) ; :: thesis:
thus Gk1 is_integrable_on Prod_Measure (SubFin (M,(k + 1))) by A20, A19; :: thesis:
reconsider G2k1 = Gk1 as PartFunc of [:(CarProduct (SubFin ((SubFin (X,(k + 1))),k))),(ElmFin ((SubFin (X,(k + 1))),(k + 1))):],ExtREAL by A9, A10, A5, Th9;
|.Gk1.| = |.G2k1.| by Th6;
then Hk = Integral2 ((ElmFin ((SubFin (M,(k + 1))),(k + 1))),|.G2k1.|) by A19, Th39;
hence ( Integral ((Prod_Measure (SubFin (M,(k + 1)))),Gk1) = Integral ((Prod_Measure ((Prod_Measure (SubFin (M,k))),(ElmFin (M,(k + 1))))),Fk1) & ( for x being Element of CarProduct (SubFin (X,k)) holds ProjPMap1 (Fk1,x) is_integrable_on ElmFin (M,(k + 1)) ) & ( for U being Element of Prod_Field (SubFin (S,k)) holds Fk is U -measurable ) & Fk is_integrable_on Prod_Measure (SubFin (M,k)) & Integral ((Prod_Measure ((Prod_Measure (SubFin (M,k))),(ElmFin (M,(k + 1))))),Fk1) = Integral ((Prod_Measure (SubFin (M,k))),Fk) & Fk in L1_Functions (Prod_Measure (SubFin (M,k))) & Integral ((Prod_Measure (SubFin (M,(k + 1)))),Gk1) = Integral ((Prod_Measure (SubFin (M,k))),Fk) ) by A9, A11, A13, A19, A10, A12, A14, A15, A16, A17, A6, A18, A20, Th35, Th36; :: thesis: