theorem extsubst: :: FIELD_14:24

for F being Field
for E being FieldExtension of F
for p, q being Polynomial of F
for p1, q1 being Polynomial of E st p1 = p & q1 = q holds
Subst (p1,q1) = Subst (p,q)