:: deftheorem Def17 defines FSqIntg MEASUR13:def 17 :
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
for b₆ being b₁ + 1 -element FinSequence holds
( b₆ = FSqIntg (M,f) iff ( b₆ . 1 = f & ( for i being Nat st 1 <= i & i < n + 1 holds
ex k being non zero Nat ex g being PartFunc of [:(CarProduct (SubFin (X,k))),(ElmFin (X,(k + 1))):],ExtREAL st
( k = (n + 1) - i & g = b₆ . i & b₆ . (i + 1) = Integral2 ((ElmFin (M,(k + 1))),g) ) ) ) );