let R be comRing; :: thesis: for S being RingExtension of R
for f being Element of the carrier of (Polynom-Ring R) holds f is Element of the carrier of (Polynom-Ring S)
let S be RingExtension of R; :: thesis: for f being Element of the carrier of (Polynom-Ring R) holds f is Element of the carrier of (Polynom-Ring S)
let f be Element of the carrier of (Polynom-Ring R); :: thesis: f is Element of the carrier of (Polynom-Ring S)
the carrier of (Polynom-Ring R) c= the carrier of (Polynom-Ring S) by FIELD_4:10;
hence f is Element of the carrier of (Polynom-Ring S) ; :: thesis: verum