let n be Nat; :: thesis: for F being Field
for E being FieldExtension of F
for a being Element of F
for b being Element of E st a = b holds
a | (n,F) = b | (n,E)
let F be Field; :: thesis: for E being FieldExtension of F
for a being Element of F
for b being Element of E st a = b holds
a | (n,F) = b | (n,E)
let E be FieldExtension of F; :: thesis: for a being Element of F
for b being Element of E st a = b holds
a | (n,F) = b | (n,E)
let a be Element of F; :: thesis: for b being Element of E st a = b holds
a | (n,F) = b | (n,E)
let b be Element of E; :: thesis: ( a = b implies a | (n,F) = b | (n,E) )
assume AS: a = b ; :: thesis: a | (n,F) = b | (n,E)
set ap = a | (n,F);
set bp = b | (n,E);
H: F is Subring of E by FIELD_4:def 1;

now :: thesis: for u being bag of n holds (a | (n,F)) . u = (b | (n,E)) . u

let u be bag of n; :: thesis: (a | (n,F)) . b₁ = (b | (n,E)) . b₁

per cases ( u = EmptyBag n or u <> EmptyBag n ) ;

suppose A: u = EmptyBag n ; :: thesis: (a | (n,F)) . b₁ = (b | (n,E)) . b₁

hence (a | (n,F)) . u = a by POLYNOM7:18
.= (b | (n,E)) . u by AS, A, POLYNOM7:18 ;
:: thesis: verum

end;

suppose A: u <> EmptyBag n ; :: thesis: (a | (n,F)) . b₁ = (b | (n,E)) . b₁

hence (a | (n,F)) . u = 0. F by POLYNOM7:def 7
.= 0. E by H, C0SP1:def 3
.= (b | (n,E)) . u by A, POLYNOM7:def 7 ;
:: thesis: verum

end;

end;

end;

hence a | (n,F) = b | (n,E) ; :: thesis: verum