per
cases
(
n
in
dom
F1
or not
n
in
dom
F1
)
;
suppose
n
in
dom
F1
;
:: thesis:
F1
.
n
is
Subset
of
X
hence
F1
.
n
is
Subset
of
X
by
FINSEQ_2:11
;
:: thesis:
verum
end;
suppose
not
n
in
dom
F1
;
:: thesis:
F1
.
n
is
Subset
of
X
then
F1
.
n
=
{}
by
FUNCT_1:def 2
;
hence
F1
.
n
is
Subset
of
X
by
SUBSET_1:1
;
:: thesis:
verum
end;
end;