theorem :: HILB10_7:104

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