let C be non empty set ; :: thesis: for f being PartFunc of C,COMPLEX holds dom ((f ^) ^) = dom (f | (dom (f ^)))
let f be PartFunc of C,COMPLEX; :: thesis: dom ((f ^) ^) = dom (f | (dom (f ^)))
A1: dom (f ^) = (dom f) \ (f " {0c}) by Def2;
thus dom ((f ^) ^) = (dom (f ^)) \ ((f ^) " {0c}) by Def2
.= (dom (f ^)) \ {} by Th9
.= (dom f) /\ (dom (f ^)) by A1, XBOOLE_1:28, XBOOLE_1:36
.= dom (f | (dom (f ^))) by RELAT_1:61 ; :: thesis: verum