theorem Th60: :: NUMBER15:60

for f, g being complex-valued FinSequence holds (f ^ g) " = (f ") ^ (g ")