let R, S be Ring; ( 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
; 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 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)) . olet o be
object ;
( 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)
;
the multF of (Polynom-Ring R) . o = ( the multF of (Polynom-Ring S) || the carrier of (Polynom-Ring R)) . othen 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
;
verum end;
hence
the multF of (Polynom-Ring R) = the multF of (Polynom-Ring S) || the carrier of (Polynom-Ring R)
by A2; verum