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

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