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