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)

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)

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;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

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

o in the carrier of (Polynom-Ring F)

hence
the carrier of (Polynom-Ring F) = the carrier of (Polynom-Ring K)
by A, TARSKI:2; :: thesis: verumo 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;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