for X being ComplexUnitarySpace
for x being Point of X
for seq being sequence of X holds seq - x = seq + (- x)