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 ;

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

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;

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