let D be non empty set ; :: thesis: for p being PartialPredicate of D st p is total holds
dom (PP_inversion p) = {}
let p be PartialPredicate of D; :: thesis: ( p is total implies dom (PP_inversion p) = {} )
set q = PP_inversion p;
assume A1: dom p = D ; :: according to PARTFUN1:def 2 :: thesis: dom (PP_inversion p) = {}
A2: dom (PP_inversion p) = { d where d is Element of D : not d in dom p } by Def19;
thus dom (PP_inversion p) c= {} :: according to XBOOLE_0:def 10 :: thesis: {} c= dom (PP_inversion p)
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in dom (PP_inversion p) or x in {} )
assume x in dom (PP_inversion p) ; :: thesis: x in {}
then ex d being Element of D st
( x = d & not d in dom p ) by A2;
hence x in {} by A1; :: thesis: verum
end;
thus {} c= dom (PP_inversion p) by XBOOLE_1:2; :: thesis: verum