reconsider A1s = [A1,s] as Element of [: the Observables of Q, the FStates of Q:] ;
the Quantum_Probability of Q . A1s is Element of Probabilities Borel_Sets ;
hence the Quantum_Probability of Q . [A1,s] is Probability of Borel_Sets by Def1; :: thesis: verum