theorem
for
D being
non-empty V26()
ManySortedSet of
NAT for
P being
Probability_sequence of
Trivial-SigmaField_sequence D holds
(
(Product-Probability (P,D)) . 0 = P . 0 &
(Product-Probability (P,D)) . 1
= Product-Probability (
(D . 0),
(D . 1),
(P . 0),
(P . 1)) & ex
P1 being
Probability of
Trivial-SigmaField [:(D . 0),(D . 1):] st
(
P1 = (Product-Probability (P,D)) . 1 &
(Product-Probability (P,D)) . 2
= Product-Probability (
[:(D . 0),(D . 1):],
(D . 2),
P1,
(P . 2)) ) & ex
P2 being
Probability of
Trivial-SigmaField [:(D . 0),(D . 1),(D . 2):] st
(
P2 = (Product-Probability (P,D)) . 2 &
(Product-Probability (P,D)) . 3
= Product-Probability (
[:(D . 0),(D . 1),(D . 2):],
(D . 3),
P2,
(P . 3)) ) & ex
P3 being
Probability of
Trivial-SigmaField [:(D . 0),(D . 1),(D . 2),(D . 3):] st
(
P3 = (Product-Probability (P,D)) . 3 &
(Product-Probability (P,D)) . 4
= Product-Probability (
[:(D . 0),(D . 1),(D . 2),(D . 3):],
(D . 4),
P3,
(P . 4)) ) )