set PS = Polynom-Ring S;
set PR = Polynom-Ring R;
A1: the addF of (Polynom-Ring R) = the addF of (Polynom-Ring S) || the carrier of (Polynom-Ring R) by Th11;
A2: the multF of (Polynom-Ring R) = the multF of (Polynom-Ring S) || the carrier of (Polynom-Ring R) by Th13;
( 1. (Polynom-Ring S) = 1. (Polynom-Ring R) & 0. (Polynom-Ring S) = 0. (Polynom-Ring R) ) by Th7, Th9;
hence Polynom-Ring S is Polynom-Ring R -extending by Th6, A1, A2, C0SP1:def 3; :: thesis: verum