theorem Th26: :: RFUNCT_1:26

for f being complex-valued Function holds (f ^) ^ = f | (dom (f ^))