dom
J
=
I
by
PARTFUN1:def 2
;
then
J
.
i
in
rng
J
by
FUNCT_1:def 3
;
hence
J
.
i
is non
empty
TopSpace
by
Def1
;
:: thesis:
verum