let R be Ring; :: thesis: for S being RingExtension of R holds the addF of () = the addF of () || the carrier of ()
let S be RingExtension of R; :: thesis: the addF of () = the addF of () || the carrier of ()
set aR = the addF of ();
set aS = the addF of () || the carrier of ();
set cR = the carrier of ();
set cS = the carrier of ();
A1: the carrier of () c= the carrier of () by Th6;
A2: dom ( the addF of () || the carrier of ()) = (dom the addF of ()) /\ [: the carrier of (), the carrier of ():] by RELAT_1:61
.= [: the carrier of (), the carrier of ():] /\ [: the carrier of (), the carrier of ():] by FUNCT_2:def 1
.= [: the carrier of (), the carrier of ():] by
.= dom the addF of () by FUNCT_2:def 1 ;
now :: thesis: for o being object st o in dom the addF of () holds
the addF of () . o = ( the addF of () || the carrier of ()) . o
let o be object ; :: thesis: ( o in dom the addF of () implies the addF of () . o = ( the addF of () || the carrier of ()) . o )
assume A3: o in dom the addF of () ; :: thesis: the addF of () . o = ( the addF of () || the carrier of ()) . o
then consider p, q being object such that
A4: ( p in the carrier of () & q in the carrier of () & o = [p,q] ) by ZFMISC_1:def 2;
reconsider p = p, q = q as Element of the carrier of () by A4;
reconsider p1 = p, q1 = q as Element of the carrier of () by A1;
reconsider p2 = p, q2 = q as Polynomial of R ;
reconsider p3 = p1, q3 = q1 as Polynomial of S ;
thus the addF of () . o = p + q by A4
.= p2 + q2 by POLYNOM3:def 10
.= p3 + q3 by Th10
.= p1 + q1 by POLYNOM3:def 10
.= ( the addF of () || the carrier of ()) . o by ; :: thesis: verum
end;
hence the addF of () = the addF of () || the carrier of () by A2; :: thesis: verum