now :: thesis: for n being object st n in dom (rngs F) holds
not (rngs F) . n is empty
let n be object ; :: 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