let P1, P2 be n + 1 -element FinSequence; :: thesis: ( P1 . 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 = P1 . i & P1 . (i + 1) = Integral2 ((ElmFin (M,(k + 1))),g) ) ) & P2 . 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 = P2 . i & P2 . (i + 1) = Integral2 ((ElmFin (M,(k + 1))),g) ) ) implies P1 = P2 )
reconsider m = n + 1 as non zero Nat ;
assume that
A20: ( P1 . 1 = f & ( for i being Nat st 1 <= i & i < n + 1 holds
ex j being non zero Nat ex g being PartFunc of [:(CarProduct (SubFin (X,j))),(ElmFin (X,(j + 1))):],ExtREAL st
( j = (n + 1) - i & g = P1 . i & P1 . (i + 1) = Integral2 ((ElmFin (M,(j + 1))),g) ) ) ) and
A21: ( P2 . 1 = f & ( for i being Nat st 1 <= i & i < n + 1 holds
ex j being non zero Nat ex g being PartFunc of [:(CarProduct (SubFin (X,j))),(ElmFin (X,(j + 1))):],ExtREAL st
( j = (n + 1) - i & g = P2 . i & P2 . (i + 1) = Integral2 ((ElmFin (M,(j + 1))),g) ) ) ) ; :: thesis: P1 = P2
defpred S₁[ Nat] means ( 1 <= $1 & $1 <= m implies P1 . $1 = P2 . $1 );
A22: S₁[ 0 ] ;
A23: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let i be Nat; :: thesis: ( S₁[i] implies S₁[i + 1] )
assume A24: S₁[i] ; :: thesis: S₁[i + 1]
assume A25: ( 1 <= i + 1 & i + 1 <= m ) ; :: thesis: P1 . (i + 1) = P2 . (i + 1)
then A26: i < n + 1 by NAT_1:13;

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

suppose i = 0 ; :: thesis: P1 . (i + 1) = P2 . (i + 1)

hence P1 . (i + 1) = P2 . (i + 1) by A20, A21; :: thesis: verum

end;

suppose i <> 0 ; :: thesis: P1 . (i + 1) = P2 . (i + 1)

then reconsider j = i as non zero Nat ;
A27: ex k being non zero Nat ex g being PartFunc of [:(CarProduct (SubFin (X,k))),(ElmFin (X,(k + 1))):],ExtREAL st
( k = m - j & g = P1 . j & P1 . (j + 1) = Integral2 ((ElmFin (M,(k + 1))),g) ) by A20, A26, NAT_1:14;
ex k being non zero Nat ex g being PartFunc of [:(CarProduct (SubFin (X,k))),(ElmFin (X,(k + 1))):],ExtREAL st
( k = m - j & g = P2 . j & P2 . (j + 1) = Integral2 ((ElmFin (M,(k + 1))),g) ) by A21, A26, NAT_1:14;
hence P1 . (i + 1) = P2 . (i + 1) by A27, A24, A25, NAT_1:13, NAT_1:14; :: thesis: verum

end;

end;

end;

A28: for i being Nat holds S₁[i] from NAT_1:sch 2(A22, A23);
( len P1 = m & len P2 = m ) by CARD_1:def 7;
hence P1 = P2 by A28; :: thesis: verum