theorem Th13: :: NAT_3:13

for a being Nat
for r being Real
for f being FinSequence of REAL holds (f ^ <*r*>) |^ a = (f |^ a) ^ (<*r*> |^ a)