theorem Th39: :: MEASUR13:39

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 g being PartFunc of [:(CarProduct (SubFin (X,n))),(ElmFin (X,(n + 1))):],ExtREAL st f = g holds
( (FSqIntg (M,f)) . 1 = f & (FSqIntg (M,f)) . 2 = Integral2 ((ElmFin (M,(n + 1))),g) )