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