let f be complex-valued Function; :: thesis: dom ((f ^) ^) = dom (f | (dom (f ^)))
A1: dom (f ^) = (dom f) \ (f " {0}) by Def2;
thus dom ((f ^) ^) = (dom (f ^)) \ ((f ^) " {0}) by Def2
.= (dom (f ^)) \ {} by Th4
.= (dom f) /\ (dom (f ^)) by A1, XBOOLE_1:28
.= dom (f | (dom (f ^))) by RELAT_1:61 ; :: thesis: verum