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:90;
then ( (rngs F) . n = rng (F . n) & not F . n is empty ) by FUNCT_1:def 15, FUNCT_6:31;
hence not (rngs F) . n is empty ; :: thesis: verum

end;

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