theorem Th40: :: HILB10_7:40

for f, g being with_evenly_repeated_values FinSequence holds f ^ g is with_evenly_repeated_values