let F, K be Field; :: thesis: ( the carrier of F = the carrier of K & 0. F = 0. K implies the carrier of (Polynom-Ring F) = the carrier of (Polynom-Ring K) )
assume AS: ( the carrier of F = the carrier of K & 0. F = 0. K ) ; :: thesis: the carrier of (Polynom-Ring F) = the carrier of (Polynom-Ring K)

A: now :: thesis: for o being object st o in the carrier of (Polynom-Ring F) holds
o in the carrier of (Polynom-Ring K)

let o be object ; :: thesis: ( o in the carrier of (Polynom-Ring F) implies o in the carrier of (Polynom-Ring K) )
assume o in the carrier of (Polynom-Ring F) ; :: thesis: o in the carrier of (Polynom-Ring K)
then reconsider p = o as Polynomial of F by POLYNOM3:def 10;
reconsider p1 = p as sequence of K by AS;
for i being Nat st i >= len p holds
p1 . i = 0. K by AS, ALGSEQ_1:8;
then p1 is finite-Support by ALGSEQ_1:def 1;
hence o in the carrier of (Polynom-Ring K) by POLYNOM3:def 10; :: thesis: verum

end;

now :: thesis: for o being object st o in the carrier of (Polynom-Ring K) holds
o in the carrier of (Polynom-Ring F)

let o be object ; :: thesis: ( o in the carrier of (Polynom-Ring K) implies o in the carrier of (Polynom-Ring F) )
assume o in the carrier of (Polynom-Ring K) ; :: thesis: o in the carrier of (Polynom-Ring F)
then reconsider p = o as Polynomial of K by POLYNOM3:def 10;
reconsider p1 = p as sequence of F by AS;
for i being Nat st i >= len p holds
p1 . i = 0. F by AS, ALGSEQ_1:8;
then p1 is finite-Support by ALGSEQ_1:def 1;
hence o in the carrier of (Polynom-Ring F) by POLYNOM3:def 10; :: thesis: verum

end;

hence the carrier of (Polynom-Ring F) = the carrier of (Polynom-Ring K) by A, TARSKI:2; :: thesis: verum