let S be non empty finite set ; :: thesis: for f being S -valued Function
for judgefunc being Function of S,BOOLEAN
for n being set st n in dom f holds
( n in trueEVENT (judgefunc * f) iff f . n in trueEVENT judgefunc )
let f be S -valued Function; :: thesis: for judgefunc being Function of S,BOOLEAN
for n being set st n in dom f holds
( n in trueEVENT (judgefunc * f) iff f . n in trueEVENT judgefunc )
let judgefunc be Function of S,BOOLEAN; :: thesis: for n being set st n in dom f holds
( n in trueEVENT (judgefunc * f) iff f . n in trueEVENT judgefunc )
let n be set ; :: thesis: ( n in dom f implies ( n in trueEVENT (judgefunc * f) iff f . n in trueEVENT judgefunc ) )
assume A1: n in dom f ; :: thesis: ( n in trueEVENT (judgefunc * f) iff f . n in trueEVENT judgefunc )
A2: trueEVENT (judgefunc * f) is Subset of (dom f) by Th8;
thus ( n in trueEVENT (judgefunc * f) implies f . n in trueEVENT judgefunc ) :: thesis: ( f . n in trueEVENT judgefunc implies n in trueEVENT (judgefunc * f) )

proof

assume A3: n in trueEVENT (judgefunc * f) ; :: thesis: f . n in trueEVENT judgefunc
then (judgefunc * f) . n in {TRUE} by FUNCT_1:def 7;
then A4: (judgefunc * f) . n = TRUE by TARSKI:def 1;
judgefunc . (f . n) = TRUE by A4, A3, A2, FUNCT_1:13;
then A5: judgefunc . (f . n) in {TRUE} by TARSKI:def 1;
f . n in rng f by A3, A2, FUNCT_1:def 3;
then f . n in S ;
then f . n in dom judgefunc by FUNCT_2:def 1;
hence f . n in trueEVENT judgefunc by A5, FUNCT_1:def 7; :: thesis: verum

end;

assume A6: f . n in trueEVENT judgefunc ; :: thesis: n in trueEVENT (judgefunc * f)
A7: ( f . n in dom judgefunc & judgefunc . (f . n) in {TRUE} ) by A6, FUNCT_1:def 7;
A8: (judgefunc * f) . n in {TRUE} by A7, A1, FUNCT_1:13;
n in dom (judgefunc * f) by A1, A6, FUNCT_1:11;
hence n in trueEVENT (judgefunc * f) by A8, FUNCT_1:def 7; :: thesis: verum