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
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) )
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
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) )
let S be sigmaFieldFamily of X; :: thesis: 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) )
let M be sigmaMeasureFamily of S; :: thesis: 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) )
let f be PartFunc of (CarProduct X),ExtREAL; :: thesis: 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) )
let g be PartFunc of [:(CarProduct (SubFin (X,n))),(ElmFin (X,(n + 1))):],ExtREAL; :: thesis: ( f = g implies ( (FSqIntg (M,f)) . 1 = f & (FSqIntg (M,f)) . 2 = Integral2 ((ElmFin (M,(n + 1))),g) ) )
assume A1: f = g ; :: thesis: ( (FSqIntg (M,f)) . 1 = f & (FSqIntg (M,f)) . 2 = Integral2 ((ElmFin (M,(n + 1))),g) )
thus (FSqIntg (M,f)) . 1 = f by Def17; :: thesis: (FSqIntg (M,f)) . 2 = Integral2 ((ElmFin (M,(n + 1))),g)
1 < n + 1 by NAT_1:13, NAT_1:14;
then ex k being non zero Nat ex g0 being PartFunc of [:(CarProduct (SubFin (X,k))),(ElmFin (X,(k + 1))):],ExtREAL st
( k = (n + 1) - 1 & g0 = (FSqIntg (M,f)) . 1 & (FSqIntg (M,f)) . (1 + 1) = Integral2 ((ElmFin (M,(k + 1))),g0) ) by Def17;
hence (FSqIntg (M,f)) . 2 = Integral2 ((ElmFin (M,(n + 1))),g) by A1, Def17; :: thesis: verum