now :: thesis: for x being object st x in dom (ProjMap f) holds
not (ProjMap f) . x is empty

let x be object ; :: thesis: ( x in dom (ProjMap f) implies not (ProjMap f) . x is empty )
assume x in dom (ProjMap f) ; :: thesis: not (ProjMap f) . x is empty
then (ProjMap f) . x = proj (f,x) by Def2;
hence not (ProjMap f) . x is empty ; :: thesis: verum

end;

hence ProjMap f is non-empty by FUNCT_1:def 9; :: thesis: verum