let S be non empty finite set ; :: thesis: for f being S -valued Function
for judgefunc being Function of S,BOOLEAN holds trueEVENT (judgefunc * f) = f " (trueEVENT judgefunc)
let f be S -valued Function; :: thesis: for judgefunc being Function of S,BOOLEAN holds trueEVENT (judgefunc * f) = f " (trueEVENT judgefunc)
let judgefunc be Function of S,BOOLEAN; :: thesis: trueEVENT (judgefunc * f) = f " (trueEVENT judgefunc)
A1: trueEVENT (judgefunc * f) is Subset of (dom f) by Th8;
for x being object holds
( x in f " (trueEVENT judgefunc) iff x in trueEVENT (judgefunc * f) )

proof

let x be object ; :: thesis: ( x in f " (trueEVENT judgefunc) iff x in trueEVENT (judgefunc * f) )
thus ( x in f " (trueEVENT judgefunc) implies x in trueEVENT (judgefunc * f) ) :: thesis: ( x in trueEVENT (judgefunc * f) implies x in f " (trueEVENT judgefunc) )

proof

assume x in f " (trueEVENT judgefunc) ; :: thesis: x in trueEVENT (judgefunc * f)
then ( x in dom f & f . x in trueEVENT judgefunc ) by FUNCT_1:def 7;
hence x in trueEVENT (judgefunc * f) by Th13; :: thesis: verum

end;

assume A2: x in trueEVENT (judgefunc * f) ; :: thesis: x in f " (trueEVENT judgefunc)
f . x in trueEVENT judgefunc by Th13, A2, A1;
hence x in f " (trueEVENT judgefunc) by A1, A2, FUNCT_1:def 7; :: thesis: verum

end;

hence trueEVENT (judgefunc * f) = f " (trueEVENT judgefunc) by TARSKI:2; :: thesis: verum