theorem bij3: :: FIELD_11:24

for F being Field
for m1, m2 being Ordinal st m1 in card (nonConstantPolys F) & m2 in card (nonConstantPolys F) holds
for p1, p2 being non constant Polynomial of F st Poly (m1,p1) = Poly (m2,p2) holds
( m1 = m2 & p1 = p2 )