let C be non empty set ; :: thesis: for f being PartFunc of C,COMPLEX holds (f ^) ^ = f | (dom (f ^))
let f be PartFunc of C,COMPLEX; :: thesis: (f ^) ^ = f | (dom (f ^))
A1: dom ((f ^) ^) = dom (f | (dom (f ^))) by Th11;

now :: thesis: for c being Element of C st c in dom ((f ^) ^) holds
((f ^) ^) /. c = (f | (dom (f ^))) /. c

let c be Element of C; :: thesis: ( c in dom ((f ^) ^) implies ((f ^) ^) /. c = (f | (dom (f ^))) /. c )
assume A2: c in dom ((f ^) ^) ; :: thesis: ((f ^) ^) /. c = (f | (dom (f ^))) /. c
then c in (dom f) /\ (dom (f ^)) by A1, RELAT_1:61;
then A3: c in dom (f ^) by XBOOLE_0:def 4;
thus ((f ^) ^) /. c = ((f ^) /. c) " by A2, Def2
.= ((f /. c) ") " by A3, Def2
.= (f | (dom (f ^))) /. c by A1, A2, PARTFUN2:15 ; :: thesis: verum

end;

hence (f ^) ^ = f | (dom (f ^)) by A1, PARTFUN2:1; :: thesis: verum