theorem Th15: :: SEQM_3:15

for k being Nat
for seq, seq1 being Real_Sequence holds (seq + seq1) ^\ k = (seq ^\ k) + (seq1 ^\ k)