theorem Th86: :: CLVECT_2:86

for X being ComplexUnitarySpace
for seq1, seq2 being sequence of X
for k being Nat holds (seq1 + seq2) ^\ k = (seq1 ^\ k) + (seq2 ^\ k)