let y be object ; :: according to HILB10_7:def 7 :: thesis: ( y in F ^ G implies y is finite with_evenly_repeated_values Function )
assume A1: y in F ^ G ; :: thesis: y is finite with_evenly_repeated_values Function
consider p, q being FinSequence such that
A2: ( y = p ^ q & p in F & q in G ) by A1, POLNOT_1:def 2;
( p is with_evenly_repeated_values & q is with_evenly_repeated_values ) by A2, Def7;
hence y is finite with_evenly_repeated_values Function by A2, Th40; :: thesis: verum