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