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 ex Pn being Probability of Trivial-SigmaField ((Product_dom D) . n) st
( Pn = (Product-Probability (P,D)) . n & (Product-Probability (P,D)) . (n + 1) = Product-Probability (((Product_dom D) . n),(D . (n + 1)),Pn,(P . (n + 1))) )
let P be Probability_sequence of Trivial-SigmaField_sequence D; :: thesis: for n being Nat ex Pn being Probability of Trivial-SigmaField ((Product_dom D) . n) st
( Pn = (Product-Probability (P,D)) . n & (Product-Probability (P,D)) . (n + 1) = Product-Probability (((Product_dom D) . n),(D . (n + 1)),Pn,(P . (n + 1))) )
let n be Nat; :: thesis: ex Pn being Probability of Trivial-SigmaField ((Product_dom D) . n) st
( Pn = (Product-Probability (P,D)) . n & (Product-Probability (P,D)) . (n + 1) = Product-Probability (((Product_dom D) . n),(D . (n + 1)),Pn,(P . (n + 1))) )
reconsider Pn = (Product-Probability (P,D)) . n as Probability of Trivial-SigmaField ((Product_dom D) . n) by Th20;
take Pn ; :: thesis: ( Pn = (Product-Probability (P,D)) . n & (Product-Probability (P,D)) . (n + 1) = Product-Probability (((Product_dom D) . n),(D . (n + 1)),Pn,(P . (n + 1))) )
thus Pn = (Product-Probability (P,D)) . n ; :: thesis: (Product-Probability (P,D)) . (n + 1) = Product-Probability (((Product_dom D) . n),(D . (n + 1)),Pn,(P . (n + 1)))
thus (Product-Probability (P,D)) . (n + 1) = Product-Probability (((Product_dom D) . n),(D . (n + 1)),(modetrans (((Product-Probability (P,D)) . n),(Trivial-SigmaField ((Product_dom D) . n)))),(P . (n + 1))) by Def13
.= Product-Probability (((Product_dom D) . n),(D . (n + 1)),Pn,(P . (n + 1))) by Def11 ; :: thesis: verum