per cases ( n in dom FSi or not n in dom FSi ) ;

suppose n in dom FSi ; :: thesis: FSi . n is Event of Si

then FSi . n in Si by Def10;
hence FSi . n is Event of Si ; :: thesis: verum

end;

suppose not n in dom FSi ; :: thesis: FSi . n is Event of Si

then FSi . n = {} by FUNCT_1:def 4;
hence FSi . n is Event of Si by PROB_1:52; :: thesis: verum

end;

end;