theorem lemphi2a: :: FIELD_13:36

for F being Field
for E being FieldExtension of F
for T being non empty finite Subset of E
for b being bag of card T
for x being b₃ -evaluating Function of (card T),E holds eval (b,x) in the carrier of (RAdj (F,T))