let f, g be FinSequence; :: thesis: ( f ^ g is with_evenly_repeated_values & f is with_evenly_repeated_values implies g is with_evenly_repeated_values )
assume A1: ( f ^ g is with_evenly_repeated_values & f is with_evenly_repeated_values ) ; :: thesis: g is with_evenly_repeated_values
let y be object ; :: according to HILB10_7:def 6 :: thesis: card (g " {y}) is even
A2: card ((f ^ g) " {y}) = (card (f " {y})) + (card (g " {y})) by FINSEQ_3:57;
( card ((f ^ g) " {y}) is even & card (f " {y}) is even ) by A1;
hence card (g " {y}) is even by A2; :: thesis: verum