per cases ( not D is empty or D is empty ) ;
suppose A1: not D is empty ; :: thesis: D --> TRUE is PartialPredicate of D
set f = D --> TRUE;
A2: dom (D --> TRUE) = D ;
rng (D --> TRUE) = {TRUE} by A1, FUNCOP_1:8;
hence D --> TRUE is PartialPredicate of D by A2, RELSET_1:4, ZFMISC_1:31; :: thesis: verum
end;
suppose D is empty ; :: thesis: D --> TRUE is PartialPredicate of D
then D --> TRUE = {} ;
hence D --> TRUE is PartialPredicate of D by RELSET_1:12; :: thesis: verum
end;
end;