let S be non empty finite set ; :: thesis: for D being EqSampleSpaces of S
for s being Element of D
for f being Function of S,BOOLEAN holds Prob (('not' f),s) = 1 - (Prob (f,s))
let D be EqSampleSpaces of S; :: thesis: for s being Element of D
for f being Function of S,BOOLEAN holds Prob (('not' f),s) = 1 - (Prob (f,s))
let s be Element of D; :: thesis: for f being Function of S,BOOLEAN holds Prob (('not' f),s) = 1 - (Prob (f,s))
let f be Function of S,BOOLEAN; :: thesis: Prob (('not' f),s) = 1 - (Prob (f,s))
A1: s is Element of S * by FINSEQ_1:def 11;
reconsider s0 = dom s as finite set ;
reconsider CfS = Coim ((f * s),TRUE) as finite set ;
card (Seg (len s)) = len s by FINSEQ_1:57;
then A2: card s0 = len s by FINSEQ_1:def 3;
A3: Coim ((f * s),TRUE) in bool (dom s) by A1, Th18;
trueEVENT (('not' f) * s) = Coim ((('not' f) * s),TRUE)
.= (dom s) \ (Coim ((f * s),TRUE)) by A1, Th23 ;
then A4: card (trueEVENT (('not' f) * s)) = (card s0) - (card CfS) by A3, CARD_2:44;
thus Prob (('not' f),s) = ((card s0) / (len s)) - ((card CfS) / (len s)) by A4, XCMPLX_1:120
.= 1 - (Prob (f,s)) by A2, XCMPLX_1:60 ; :: thesis: verum