let Q be Quantum_Mechanics; :: thesis: for s being Element of Sts Q
for p being Element of Prop Q
for E being Event of Borel_Sets st E = (p `2 ) ` holds
(Meas (p `1 ),s) . (p `2 ) = 1 - ((Meas (p `1 ),s) . E)
let s be Element of Sts Q; :: thesis: for p being Element of Prop Q
for E being Event of Borel_Sets st E = (p `2 ) ` holds
(Meas (p `1 ),s) . (p `2 ) = 1 - ((Meas (p `1 ),s) . E)
let p be Element of Prop Q; :: thesis: for E being Event of Borel_Sets st E = (p `2 ) ` holds
(Meas (p `1 ),s) . (p `2 ) = 1 - ((Meas (p `1 ),s) . E)
let E be Event of Borel_Sets ; :: thesis: ( E = (p `2 ) ` implies (Meas (p `1 ),s) . (p `2 ) = 1 - ((Meas (p `1 ),s) . E) )
assume A1: E = (p `2 ) ` ; :: thesis: (Meas (p `1 ),s) . (p `2 ) = 1 - ((Meas (p `1 ),s) . E)
( [#] Borel_Sets = REAL & REAL \ E = E ` ) by PROB_1:def 11;
hence (Meas (p `1 ),s) . (p `2 ) = 1 - ((Meas (p `1 ),s) . E) by A1, PROB_1:68; :: thesis: verum