now

let n be set ; :: thesis: ( n in dom (rngs F) implies not (rngs F) . n is empty )
assume n in dom (rngs F) ; :: thesis: not (rngs F) . n is empty
then n in dom F by FUNCT_6:60;
then ( (rngs F) . n = rng (F . n) & not F . n is empty ) by FUNCT_1:def 9, FUNCT_6:22;
hence not (rngs F) . n is empty ; :: thesis: verum

end;

hence rngs F is non-empty by FUNCT_1:def 9; :: thesis: verum