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 ;

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

hence
the multF of (Polynom-Ring R) = the multF of (Polynom-Ring S) || the carrier of (Polynom-Ring R)
by A2; :: thesis: verumthe 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;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