let D be non-empty V26() ManySortedSet of NAT ; :: thesis: for P being Probability_sequence of Trivial-SigmaField_sequence D

for n being Nat holds (Product-Probability (P,D)) . n is Probability of Trivial-SigmaField ((Product_dom D) . n)

let P be Probability_sequence of Trivial-SigmaField_sequence D; :: thesis: for n being Nat holds (Product-Probability (P,D)) . n is Probability of Trivial-SigmaField ((Product_dom D) . n)

defpred S_{1}[ Nat] means (Product-Probability (P,D)) . $1 is Probability of Trivial-SigmaField ((Product_dom D) . $1);

A1: (Product-Probability (P,D)) . 0 = P . 0 by Def13;

D . 0 = (Product_dom D) . 0 by Def10;

then A2: S_{1}[ 0 ]
by A1;

A3: for k being Nat st S_{1}[k] holds

S_{1}[k + 1]
_{1}[n]
from NAT_1:sch 2(A2, A3);

hence for n being Nat holds (Product-Probability (P,D)) . n is Probability of Trivial-SigmaField ((Product_dom D) . n) ; :: thesis: verum

for n being Nat holds (Product-Probability (P,D)) . n is Probability of Trivial-SigmaField ((Product_dom D) . n)

let P be Probability_sequence of Trivial-SigmaField_sequence D; :: thesis: for n being Nat holds (Product-Probability (P,D)) . n is Probability of Trivial-SigmaField ((Product_dom D) . n)

defpred S

A1: (Product-Probability (P,D)) . 0 = P . 0 by Def13;

D . 0 = (Product_dom D) . 0 by Def10;

then A2: S

A3: for k being Nat st S

S

proof

for n being Nat holds S
let k be Nat; :: thesis: ( S_{1}[k] implies S_{1}[k + 1] )

assume S_{1}[k]
; :: thesis: S_{1}[k + 1]

A4: (Product-Probability (P,D)) . (k + 1) = Product-Probability (((Product_dom D) . k),(D . (k + 1)),(modetrans (((Product-Probability (P,D)) . k),(Trivial-SigmaField ((Product_dom D) . k)))),(P . (k + 1))) by Def13;

(Product_dom D) . (k + 1) = [:((Product_dom D) . k),(D . (k + 1)):] by Def10;

hence S_{1}[k + 1]
by A4; :: thesis: verum

end;assume S

A4: (Product-Probability (P,D)) . (k + 1) = Product-Probability (((Product_dom D) . k),(D . (k + 1)),(modetrans (((Product-Probability (P,D)) . k),(Trivial-SigmaField ((Product_dom D) . k)))),(P . (k + 1))) by Def13;

(Product_dom D) . (k + 1) = [:((Product_dom D) . k),(D . (k + 1)):] by Def10;

hence S

hence for n being Nat holds (Product-Probability (P,D)) . n is Probability of Trivial-SigmaField ((Product_dom D) . n) ; :: thesis: verum