theorem ConcatPower: :: NUMBER18:73

for f, g being real-valued FinSequence
for m being non zero Nat holds (f ^ g) |^ m = (f |^ m) ^ (g |^ m)