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) is Event of (dom f)
let f be S -valued Function; :: thesis: for judgefunc being Function of S,BOOLEAN holds trueEVENT (judgefunc * f) is Event of (dom f)
let judgefunc be Function of S,BOOLEAN; :: thesis: trueEVENT (judgefunc * f) is Event of (dom f)
for x being object st x in dom (judgefunc * f) holds
x in dom f by FUNCT_1:11;
then dom (judgefunc * f) c= dom f by TARSKI:def 3;
hence trueEVENT (judgefunc * f) is Event of (dom f) by XBOOLE_1:1; :: thesis: verum