set X = nonConstantPolys F;
set Y = card (nonConstantPolys F);
consider f being Function such that
H: ( f is one-to-one & dom f = nonConstantPolys F & rng f = card (nonConstantPolys F) ) by CARD_1:def 2, WELLORD2:def 4;
reconsider f = f as Function of (nonConstantPolys F),(card (nonConstantPolys F)) by H, FUNCT_2:2;
f is onto by H;
hence ex b₁ being Function of (nonConstantPolys F),(card (nonConstantPolys F)) st b₁ is bijective by H; :: thesis: verum