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

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