let D be non-empty finite-yielding 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₁[ 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₁[ 0 ] by A1;
A3: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume S₁[k] ; :: thesis: S₁[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₁[k + 1] by A4; :: thesis: verum

end;

for n being Nat holds S₁[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