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)

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

thus
{} c= dom (PP_inversion p)
by XBOOLE_1:2; :: thesis: verum
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;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