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

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