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 7;
hence (Meas ((p `1),s)) . (p `2) = 1 - ((Meas ((p `1),s)) . E) by A1, PROB_1:32; :: thesis: verum