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