let R be Ring; :: thesis: for S being RingExtension of R holds the addF of (Polynom-Ring R) = the addF of (Polynom-Ring S) || the carrier of (Polynom-Ring R)

let S be RingExtension of R; :: thesis: the addF of (Polynom-Ring R) = the addF of (Polynom-Ring S) || the carrier of (Polynom-Ring R)

set aR = the addF of (Polynom-Ring R);

set aS = the addF 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 Th6;

A2: dom ( the addF of (Polynom-Ring S) || the carrier of (Polynom-Ring R)) = (dom the addF 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 addF of (Polynom-Ring R) by FUNCT_2:def 1 ;

let S be RingExtension of R; :: thesis: the addF of (Polynom-Ring R) = the addF of (Polynom-Ring S) || the carrier of (Polynom-Ring R)

set aR = the addF of (Polynom-Ring R);

set aS = the addF 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 Th6;

A2: dom ( the addF of (Polynom-Ring S) || the carrier of (Polynom-Ring R)) = (dom the addF 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 addF of (Polynom-Ring R) by FUNCT_2:def 1 ;

now :: thesis: for o being object st o in dom the addF of (Polynom-Ring R) holds

the addF of (Polynom-Ring R) . o = ( the addF of (Polynom-Ring S) || the carrier of (Polynom-Ring R)) . o

hence
the addF of (Polynom-Ring R) = the addF of (Polynom-Ring S) || the carrier of (Polynom-Ring R)
by A2; :: thesis: verumthe addF of (Polynom-Ring R) . o = ( the addF of (Polynom-Ring S) || the carrier of (Polynom-Ring R)) . o

let o be object ; :: thesis: ( o in dom the addF of (Polynom-Ring R) implies the addF of (Polynom-Ring R) . o = ( the addF of (Polynom-Ring S) || the carrier of (Polynom-Ring R)) . o )

assume A3: o in dom the addF of (Polynom-Ring R) ; :: thesis: the addF of (Polynom-Ring R) . o = ( the addF 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 addF of (Polynom-Ring R) . o = p + q by A4

.= p2 + q2 by POLYNOM3:def 10

.= p3 + q3 by Th10

.= p1 + q1 by POLYNOM3:def 10

.= ( the addF of (Polynom-Ring S) || the carrier of (Polynom-Ring R)) . o by A2, A3, A4, FUNCT_1:47 ; :: thesis: verum

end;assume A3: o in dom the addF of (Polynom-Ring R) ; :: thesis: the addF of (Polynom-Ring R) . o = ( the addF 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 addF of (Polynom-Ring R) . o = p + q by A4

.= p2 + q2 by POLYNOM3:def 10

.= p3 + q3 by Th10

.= p1 + q1 by POLYNOM3:def 10

.= ( the addF of (Polynom-Ring S) || the carrier of (Polynom-Ring R)) . o by A2, A3, A4, FUNCT_1:47 ; :: thesis: verum