let R, S be Ring; :: thesis: ( S is RingExtension of R implies the multF of (Polynom-Ring R) = the multF of (Polynom-Ring S) || the carrier of (Polynom-Ring R) )
assume AS: S is RingExtension of R ; :: thesis: the multF of (Polynom-Ring R) = the multF of (Polynom-Ring S) || the carrier of (Polynom-Ring R)
set mR = the multF of (Polynom-Ring R);
set mS = the multF of (Polynom-Ring S) || the carrier of (Polynom-Ring R);
set cR = the carrier of (Polynom-Ring R);
set cS = the carrier of (Polynom-Ring S);
A1: the carrier of (Polynom-Ring R) c= the carrier of (Polynom-Ring S) by AS, Th6;
A2: dom ( the multF of (Polynom-Ring S) || the carrier of (Polynom-Ring R)) = (dom the multF of (Polynom-Ring S)) /\ [: the carrier of (Polynom-Ring R), the carrier of (Polynom-Ring R):] by RELAT_1:61
.= [: the carrier of (Polynom-Ring S), the carrier of (Polynom-Ring S):] /\ [: the carrier of (Polynom-Ring R), the carrier of (Polynom-Ring R):] by FUNCT_2:def 1
.= [: the carrier of (Polynom-Ring R), the carrier of (Polynom-Ring R):] by A1, ZFMISC_1:96, XBOOLE_1:28
.= dom the multF of (Polynom-Ring R) by FUNCT_2:def 1 ;

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

let o be object ; :: thesis: ( o in dom the multF of (Polynom-Ring R) implies the multF of (Polynom-Ring R) . o = ( the multF of (Polynom-Ring S) || the carrier of (Polynom-Ring R)) . o )
assume A3: o in dom the multF of (Polynom-Ring R) ; :: thesis: the multF of (Polynom-Ring R) . o = ( the multF of (Polynom-Ring S) || the carrier of (Polynom-Ring R)) . o
then consider p, q being object such that
A4: ( p in the carrier of (Polynom-Ring R) & q in the carrier of (Polynom-Ring R) & o = [p,q] ) by ZFMISC_1:def 2;
reconsider p = p, q = q as Element of the carrier of (Polynom-Ring R) by A4;
reconsider p1 = p, q1 = q as Element of the carrier of (Polynom-Ring S) by A1;
reconsider p2 = p, q2 = q as Polynomial of R ;
reconsider p3 = p1, q3 = q1 as Polynomial of S ;
thus the multF of (Polynom-Ring R) . o = p * q by A4
.= p2 *' q2 by POLYNOM3:def 10
.= p3 *' q3 by AS, Th12
.= p1 * q1 by POLYNOM3:def 10
.= ( the multF of (Polynom-Ring S) || the carrier of (Polynom-Ring R)) . o by A4, A2, A3, FUNCT_1:47 ; :: thesis: verum

end;

hence the multF of (Polynom-Ring R) = the multF of (Polynom-Ring S) || the carrier of (Polynom-Ring R) by A2; :: thesis: verum