let R be Ring; :: thesis: for S being RingExtension of R holds the carrier of (Polynom-Ring R) c= the carrier of (Polynom-Ring S)
let S be RingExtension of R; :: thesis: the carrier of (Polynom-Ring R) c= the carrier of (Polynom-Ring S)

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

let o be object ; :: thesis: ( o in the carrier of (Polynom-Ring R) implies o in the carrier of (Polynom-Ring S) )
assume o in the carrier of (Polynom-Ring R) ; :: thesis: o in the carrier of (Polynom-Ring S)
then o is Polynomial of R by POLYNOM3:def 10;
then o is Polynomial of S by Th5;
hence o in the carrier of (Polynom-Ring S) by POLYNOM3:def 10; :: thesis: verum

end;

hence the carrier of (Polynom-Ring R) c= the carrier of (Polynom-Ring S) ; :: thesis: verum