let D be non-empty V26() ManySortedSet of NAT ; 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; 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; 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
; ( 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
; (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
; verum