per cases ( not D is empty or D is empty ) ;

suppose A1: not D is empty ; :: thesis: D --> FALSE is PartialPredicate of D

set f = D --> FALSE;
A2: dom (D --> FALSE) = D ;
rng (D --> FALSE) = {FALSE} by A1, FUNCOP_1:8;
hence D --> FALSE is PartialPredicate of D by A2, RELSET_1:4, ZFMISC_1:31; :: thesis: verum

end;

suppose D is empty ; :: thesis: D --> FALSE is PartialPredicate of D

then D --> FALSE = {} ;
hence D --> FALSE is PartialPredicate of D by RELSET_1:12; :: thesis: verum

end;

end;