reconsider m = n + 1 as non zero Nat ;
defpred S₁[ Nat, set , set ] means ( ex k being non zero Nat ex g being PartFunc of [:(CarProduct (SubFin (X,k))),(ElmFin (X,(k + 1))):],ExtREAL st
( k = m - $1 & g = $2 ) implies ex k being non zero Nat ex g being PartFunc of [:(CarProduct (SubFin (X,k))),(ElmFin (X,(k + 1))):],ExtREAL st
( k = m - $1 & g = $2 & $3 = Integral2 ((ElmFin (M,(k + 1))),g) ) );
A1: for i being Nat st 1 <= i & i < m holds
for x being set ex y being set st S₁[i,x,y]

proof

let i be Nat; :: thesis: ( 1 <= i & i < m implies for x being set ex y being set st S₁[i,x,y] )
assume ( 1 <= i & i < m ) ; :: thesis: for x being set ex y being set st S₁[i,x,y]
let x be set ; :: thesis: ex y being set st S₁[i,x,y]

now :: thesis: ( ex k being non zero Nat ex g being PartFunc of [:(CarProduct (SubFin (X,k))),(ElmFin (X,(k + 1))):],ExtREAL st
( k = m - i & g = x ) implies ex y being set st S₁[i,x,y] )

assume ex k being non zero Nat ex g being PartFunc of [:(CarProduct (SubFin (X,k))),(ElmFin (X,(k + 1))):],ExtREAL st
( k = m - i & g = x ) ; :: thesis: ex y being set st S₁[i,x,y]
then consider k being non zero Nat, g being PartFunc of [:(CarProduct (SubFin (X,k))),(ElmFin (X,(k + 1))):],ExtREAL such that
A2: ( k = m - i & g = x ) ;
reconsider y = Integral2 ((ElmFin (M,(k + 1))),g) as set ;
take y = y; :: thesis: S₁[i,x,y]
thus S₁[i,x,y] by A2; :: thesis: verum

end;

hence ex y being set st S₁[i,x,y] ; :: thesis: verum

end;

consider P being FinSequence such that
A3: ( len P = m & ( P . 1 = f or m = 0 ) & ( for i being Nat st 1 <= i & i < m holds
S₁[i,P . i,P . (i + 1)] ) ) from RECDEF_1:sch 3(A1);
reconsider P = P as n + 1 -element FinSequence by A3, CARD_1:def 7;
take P ; :: thesis: ( P . 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 = P . i & P . (i + 1) = Integral2 ((ElmFin (M,(k + 1))),g) ) ) )
defpred S₂[ Nat] means ( 1 <= $1 & $1 < m implies ex k being non zero Nat ex g being PartFunc of [:(CarProduct (SubFin (X,k))),(ElmFin (X,(k + 1))):],ExtREAL st
( k = m - $1 & g = P . $1 ) );
A4: S₂[ 0 ] ;
A5: for i being Nat st S₂[i] holds
S₂[i + 1]

proof

let i be Nat; :: thesis: ( S₂[i] implies S₂[i + 1] )
assume A6: S₂[i] ; :: thesis: S₂[i + 1]
assume A7: ( 1 <= i + 1 & i + 1 < m ) ; :: thesis: ex k being non zero Nat ex g being PartFunc of [:(CarProduct (SubFin (X,k))),(ElmFin (X,(k + 1))):],ExtREAL st
( k = m - (i + 1) & g = P . (i + 1) )
A8: i + 0 < i + 1 by XREAL_1:8;

per cases ( i = 0 or i <> 0 ) ;

suppose A9: i = 0 ; :: thesis: ex k being non zero Nat ex g being PartFunc of [:(CarProduct (SubFin (X,k))),(ElmFin (X,(k + 1))):],ExtREAL st
( k = m - (i + 1) & g = P . (i + 1) )

reconsider k = m - 1 as non zero Nat ;
reconsider g = f as PartFunc of [:(CarProduct (SubFin (X,k))),(ElmFin (X,(k + 1))):],ExtREAL by Th6;
take k ; :: thesis: ex g being PartFunc of [:(CarProduct (SubFin (X,k))),(ElmFin (X,(k + 1))):],ExtREAL st
( k = m - (i + 1) & g = P . (i + 1) )
take g ; :: thesis: ( k = m - (i + 1) & g = P . (i + 1) )
thus ( k = m - (i + 1) & g = P . (i + 1) ) by A3, A9; :: thesis: verum

end;

suppose A10: i <> 0 ; :: thesis: ex k being non zero Nat ex g being PartFunc of [:(CarProduct (SubFin (X,k))),(ElmFin (X,(k + 1))):],ExtREAL st
( k = m - (i + 1) & g = P . (i + 1) )

then ( 1 <= i & i < m ) by A8, A7, XXREAL_0:2, NAT_1:14;
then consider k being non zero Nat, g being PartFunc of [:(CarProduct (SubFin (X,k))),(ElmFin (X,(k + 1))):],ExtREAL such that
A11: ( k = m - i & g = P . i & P . (i + 1) = Integral2 ((ElmFin (M,(k + 1))),g) ) by A3, A6;
reconsider k1 = m - (i + 1) as non zero Nat by A7, NAT_1:21;
A12: k1 + 1 = k by A11;
then A13: k1 <= k by NAT_1:12;
(m + 1) - i <= (m + 1) - 1 by A10, NAT_1:14, XREAL_1:10;
then A14: k < m by A11, NAT_1:13;
then A15: ( SubFin (X,k) = X | k & SubFin (X,k1) = X | k1 ) by A13, Def5, XXREAL_0:2;
SubFin ((SubFin (X,k)),k1) = (SubFin (X,k)) | k1 by A12, Def5, NAT_1:12;
then A16: SubFin ((SubFin (X,k)),k1) = SubFin (X,k1) by A15, A12, NAT_1:12, FINSEQ_1:82;
ElmFin ((SubFin (X,k)),(k1 + 1)) = (SubFin (X,k)) . (k1 + 1) by A11, Def1;
then A17: ElmFin ((SubFin (X,k)),(k1 + 1)) = X . (k1 + 1) by A11, A15, FINSEQ_1:4, FUNCT_1:49;
CarProduct (SubFin (X,k)) = [:(CarProduct (SubFin ((SubFin (X,k)),k1))),(ElmFin ((SubFin (X,k)),(k1 + 1))):] by Th6, A11;
then CarProduct (SubFin (X,k)) = [:(CarProduct (SubFin (X,k1))),(ElmFin (X,(k1 + 1))):] by A14, A11, A16, A17, Def1;
hence ex k being non zero Nat ex g being PartFunc of [:(CarProduct (SubFin (X,k))),(ElmFin (X,(k + 1))):],ExtREAL st
( k = m - (i + 1) & g = P . (i + 1) ) by A11; :: thesis: verum

end;

end;

end;

A18: for i being Nat holds S₂[i] from NAT_1:sch 2(A4, A5);

now :: thesis: for i being non zero Nat st 1 <= i & i < m holds
ex k being non zero Nat ex g being PartFunc of [:(CarProduct (SubFin (X,k))),(ElmFin (X,(k + 1))):],ExtREAL st
( k = m - i & g = P . i & P . (i + 1) = Integral2 ((ElmFin (M,(k + 1))),g) )

let i be non zero Nat; :: thesis: ( 1 <= i & i < m implies ex k being non zero Nat ex g being PartFunc of [:(CarProduct (SubFin (X,k))),(ElmFin (X,(k + 1))):],ExtREAL st
( k = m - i & g = P . i & P . (i + 1) = Integral2 ((ElmFin (M,(k + 1))),g) ) )
assume A19: ( 1 <= i & i < m ) ; :: thesis: ex k being non zero Nat ex g being PartFunc of [:(CarProduct (SubFin (X,k))),(ElmFin (X,(k + 1))):],ExtREAL st
( k = m - i & g = P . i & P . (i + 1) = Integral2 ((ElmFin (M,(k + 1))),g) )
then ex k being non zero Nat ex g being PartFunc of [:(CarProduct (SubFin (X,k))),(ElmFin (X,(k + 1))):],ExtREAL st
( k = m - i & g = P . i ) by A18;
hence ex k being non zero Nat ex g being PartFunc of [:(CarProduct (SubFin (X,k))),(ElmFin (X,(k + 1))):],ExtREAL st
( k = m - i & g = P . i & P . (i + 1) = Integral2 ((ElmFin (M,(k + 1))),g) ) by A3, A19; :: thesis: verum

end;

hence ( P . 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 = P . i & P . (i + 1) = Integral2 ((ElmFin (M,(k + 1))),g) ) ) ) by A3; :: thesis: verum