theorem lift5: :: FIELD_12:43

for F1, F2 being Field
for E being b₁ -algebraic FieldExtension of F1 st F1 == F2 holds
E is b₂ -algebraic FieldExtension of F2