for X being set
for C being non empty set
for f being PartFunc of C,COMPLEX holds
( (- f) | X = - (f | X) & (f ^) | X = (f | X) ^ & |.f.| | X = |.(f | X).| )