let S be non empty finite set ; :: thesis: for D being EqSampleSpaces of S
for f, g being Function of S,BOOLEAN holds Prob ((f 'or' g),D) = ((Prob (f,D)) + (Prob (g,D))) - (Prob ((f '&' g),D))
let D be EqSampleSpaces of S; :: thesis: for f, g being Function of S,BOOLEAN holds Prob ((f 'or' g),D) = ((Prob (f,D)) + (Prob (g,D))) - (Prob ((f '&' g),D))
let f, g be Function of S,BOOLEAN; :: thesis: Prob ((f 'or' g),D) = ((Prob (f,D)) + (Prob (g,D))) - (Prob ((f '&' g),D))
set s = the Element of D;
card ((trueEVENT (f * the Element of D)) \/ (trueEVENT (g * the Element of D))) = ((card (trueEVENT (f * the Element of D))) + (card (trueEVENT (g * the Element of D)))) - (card ((trueEVENT (f * the Element of D)) /\ (trueEVENT (g * the Element of D)))) by CARD_2:45;
then Prob ((f 'or' g), the Element of D) = (((card (trueEVENT (f * the Element of D))) + (card (trueEVENT (g * the Element of D)))) - (card ((trueEVENT (f * the Element of D)) /\ (trueEVENT (g * the Element of D))))) / (len the Element of D) by Th24
.= (((card (trueEVENT (f * the Element of D))) / (len the Element of D)) + ((card (trueEVENT (g * the Element of D))) / (len the Element of D))) - ((card ((trueEVENT (f * the Element of D)) /\ (trueEVENT (g * the Element of D)))) / (len the Element of D)) by XCMPLX_1:124
.= ((Prob (f, the Element of D)) + (Prob (g, the Element of D))) - (Prob ((f '&' g), the Element of D)) by Th25
.= ((Prob (f,D)) + (Prob (g, the Element of D))) - (Prob ((f '&' g), the Element of D)) by Def6
.= ((Prob (f,D)) + (Prob (g,D))) - (Prob ((f '&' g), the Element of D)) by Def6
.= ((Prob (f,D)) + (Prob (g,D))) - (Prob ((f '&' g),D)) by Def6 ;
hence Prob ((f 'or' g),D) = ((Prob (f,D)) + (Prob (g,D))) - (Prob ((f '&' g),D)) by Def6; :: thesis: verum