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

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

hence FSi . n is Event of Si by FINSEQ_2:11; :: thesis: verum

end;

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

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

end;

end;