theorem Th24: :: FLEXARY1:24

for r being Real
for f, g being real-valued FinSequence holds r |^ (f ^ g) = (r |^ f) ^ (r |^ g)