let D be non-empty finite-yielding ManySortedSet of NAT ; :: thesis: 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)) ) )
let P be Probability_sequence of Trivial-SigmaField_sequence D; :: thesis: ( (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)) ) )
thus (Product-Probability (P,D)) . 0 = P . 0 by Def13; :: thesis: ( (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)) ) )
A1: (Product_dom D) . 0 = D . 0 by Th19;
A2: modetrans (((Product-Probability (P,D)) . 0),(Trivial-SigmaField ((Product_dom D) . 0))) = modetrans ((P . 0),(Trivial-SigmaField (D . 0))) by A1, Def13
.= P . 0 by Def11 ;
thus (Product-Probability (P,D)) . 1 = (Product-Probability (P,D)) . (0 + 1)
.= Product-Probability (((Product_dom D) . 0),(D . 1),(modetrans (((Product-Probability (P,D)) . 0),(Trivial-SigmaField ((Product_dom D) . 0)))),(P . 1)) by Def13
.= Product-Probability ((D . 0),(D . 1),(P . 0),(P . 1)) by A2, Th19 ; :: thesis: ( 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)) ) )
consider P1 being Probability of Trivial-SigmaField ((Product_dom D) . 1) such that
A3: ( P1 = (Product-Probability (P,D)) . 1 & (Product-Probability (P,D)) . (1 + 1) = Product-Probability (((Product_dom D) . 1),(D . (1 + 1)),P1,(P . (1 + 1))) ) by Th21;
(Product_dom D) . 1 = [:(D . 0),(D . 1):] by Th19;
then reconsider P1 = P1 as Probability of Trivial-SigmaField [:(D . 0),(D . 1):] ;
A4: (Product-Probability (P,D)) . 2 = Product-Probability ([:(D . 0),(D . 1):],(D . 2),P1,(P . 2)) by A3, Th19;
consider P2 being Probability of Trivial-SigmaField ((Product_dom D) . 2) such that
A5: ( P2 = (Product-Probability (P,D)) . 2 & (Product-Probability (P,D)) . (2 + 1) = Product-Probability (((Product_dom D) . 2),(D . (2 + 1)),P2,(P . (2 + 1))) ) by Th21;
(Product_dom D) . 2 = [:(D . 0),(D . 1),(D . 2):] by Th19;
then reconsider P2 = P2 as Probability of Trivial-SigmaField [:(D . 0),(D . 1),(D . 2):] ;
A6: (Product-Probability (P,D)) . 3 = Product-Probability ([:(D . 0),(D . 1),(D . 2):],(D . 3),P2,(P . 3)) by A5, Th19;
consider P3 being Probability of Trivial-SigmaField ((Product_dom D) . 3) such that
A7: ( P3 = (Product-Probability (P,D)) . 3 & (Product-Probability (P,D)) . (3 + 1) = Product-Probability (((Product_dom D) . 3),(D . (3 + 1)),P3,(P . (3 + 1))) ) by Th21;
(Product_dom D) . 3 = [:(D . 0),(D . 1),(D . 2),(D . 3):] by Th19;
then reconsider P3 = P3 as Probability of Trivial-SigmaField [:(D . 0),(D . 1),(D . 2),(D . 3):] ;
(Product-Probability (P,D)) . 4 = Product-Probability ([:(D . 0),(D . 1),(D . 2),(D . 3):],(D . 4),P3,(P . 4)) by A7, Th19;
hence ( 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)) ) ) by A4, A5, A3, A7, A6; :: thesis: verum