let Q be Quantum_Mechanics; 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; 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; 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 ; ( E = (p `2) ` implies (Meas ((p `1),s)) . (p `2) = 1 - ((Meas ((p `1),s)) . E) )
assume A1:
E = (p `2) `
; (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; verum