theorem Th33: :: CFUNCT_1:34

for C being non empty set
for f being PartFunc of C,COMPLEX holds (f ^) ^ = f | (dom (f ^))