P . n is Probability of (Trivial-SigmaField_sequence D) . n ;
hence P . n is Probability of Trivial-SigmaField (D . n) by Def12; :: thesis: verum