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 Th18
.= (dom f) /\ (dom (f ^ )) by A1, XBOOLE_1:28, XBOOLE_1:36
.= dom (f | (dom (f ^ ))) by RELAT_1:90 ; :: thesis: verum