theorem :: CSSPACE:64

for X being ComplexUnitarySpace
for seq1, seq2 being sequence of X holds seq1 - seq2 = seq1 + (- seq2)