theorem :: VALUED_2:43

for X being set
for Y being complex-functions-membered set
for f being PartFunc of X,Y holds </> (</> f) = f