let P1, P2 be sigmaMeasureFamily of ProdSigmaFldFinSeq S; :: thesis: ( P1 . 1 = M . 1 & ( for i being non zero Nat st i < m holds
ex Mi being sigma_Measure of (Prod_Field (SubFin (S,i))) st
( Mi = P1 . i & P1 . (i + 1) = product_sigma_Measure (Mi,(ElmFin (M,(i + 1)))) ) ) & P2 . 1 = M . 1 & ( for i being non zero Nat st i < m holds
ex Mi being sigma_Measure of (Prod_Field (SubFin (S,i))) st
( Mi = P2 . i & P2 . (i + 1) = product_sigma_Measure (Mi,(ElmFin (M,(i + 1)))) ) ) implies P1 = P2 )
assume that
A26: ( P1 . 1 = M . 1 & ( for i being non zero Nat st i < m holds
ex Mi being sigma_Measure of (Prod_Field (SubFin (S,i))) st
( Mi = P1 . i & P1 . (i + 1) = product_sigma_Measure (Mi,(ElmFin (M,(i + 1)))) ) ) ) and
A27: ( P2 . 1 = M . 1 & ( for i being non zero Nat st i < m holds
ex Mi being sigma_Measure of (Prod_Field (SubFin (S,i))) st
( Mi = P2 . i & P2 . (i + 1) = product_sigma_Measure (Mi,(ElmFin (M,(i + 1)))) ) ) ) ; :: thesis: P1 = P2
A28: ( len P1 = m & len P2 = m ) by CARD_1:def 7;
defpred S₁[ Nat] means ( 1 <= $1 & $1 <= len P1 implies P1 . $1 = P2 . $1 );
A29: S₁[ 0 ] ;
A30: for i being Nat st S₁[i] holds
S₁[i + 1]

proof

let i be Nat; :: thesis: ( S₁[i] implies S₁[i + 1] )
assume A31: S₁[i] ; :: thesis: S₁[i + 1]
assume A32: ( 1 <= i + 1 & i + 1 <= len P1 ) ; :: thesis: P1 . (i + 1) = P2 . (i + 1)

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 A26, A27; :: thesis: verum

end;

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

then reconsider i1 = i as non zero Nat ;
A33: ex Mi1 being sigma_Measure of (Prod_Field (SubFin (S,i1))) st
( Mi1 = P1 . i1 & P1 . (i1 + 1) = product_sigma_Measure (Mi1,(ElmFin (M,(i1 + 1)))) ) by A26, A28, A32, NAT_1:13;
ex Mi2 being sigma_Measure of (Prod_Field (SubFin (S,i1))) st
( Mi2 = P2 . i1 & P2 . (i1 + 1) = product_sigma_Measure (Mi2,(ElmFin (M,(i1 + 1)))) ) by A27, A28, A32, NAT_1:13;
hence P1 . (i + 1) = P2 . (i + 1) by A33, A31, A32, NAT_1:13, NAT_1:14; :: thesis: verum

end;

end;

end;

for i being Nat holds S₁[i] from NAT_1:sch 2(A29, A30);
hence P1 = P2 by A28; :: thesis: verum