:: deftheorem defines is_Sequentially_integrable_on MEASUR13:def 18 :
for n being non zero Nat
for X being non-empty b₁ + 1 -element FinSequence
for S being sigmaFieldFamily of X
for M being sigmaMeasureFamily of S
for f being PartFunc of (CarProduct X),ExtREAL holds
( f is_Sequentially_integrable_on M iff for k being non zero Nat st k < n + 1 holds
ex G being PartFunc of (CarProduct (SubFin (X,(k + 1)))),ExtREAL ex H being PartFunc of (CarProduct (SubFin (X,k))),ExtREAL st
( G = (FSqIntg (M,f)) . ((n + 1) - k) & H = (FSqIntg ((SubFin (M,(k + 1))),|.G.|)) . 2 & ( for x being Element of CarProduct (SubFin (X,k)) holds H . x < +infty ) ) );