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;