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 Th20;

now

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:90;
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:32 ; :: thesis: verum

end;

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