let f, g be with_evenly_repeated_values FinSequence; :: thesis: f ^ g is with_evenly_repeated_values
set fg = f ^ g;
let y be object ; :: according to HILB10_7:def 6 :: thesis: card ((f ^ g) " {y}) is even
reconsider c1 = card (f " {y}), c2 = card (g " {y}) as even Nat by Def6;
card ((f ^ g) " {y}) = c1 + c2 by FINSEQ_3:57;
hence card ((f ^ g) " {y}) is even ; :: thesis: verum