let R be non degenerated comRing; :: thesis: Polynom-Ring R is Subring of Formal-Series R
set PR = Polynom-Ring R;
set FS = Formal-Series R;
set X = [: the carrier of (Polynom-Ring R), the carrier of (Polynom-Ring R):];
set Y = [: the carrier of (Formal-Series R), the carrier of (Formal-Series R):];
A1: for o being object st o in the carrier of (Polynom-Ring R) holds
o in the carrier of (Formal-Series R)

proof

let o be object ; :: thesis: ( o in the carrier of (Polynom-Ring R) implies o in the carrier of (Formal-Series R) )
assume o in the carrier of (Polynom-Ring R) ; :: thesis: o in the carrier of (Formal-Series R)
then o is Polynomial of R by POLYNOM3:def 10;
hence o in the carrier of (Formal-Series R) by POLYALG1:def 2; :: thesis: verum

end;

A2: the carrier of (Polynom-Ring R) c= the carrier of (Formal-Series R) by A1;
A3: the addF of (Polynom-Ring R) = the addF of (Formal-Series R) || the carrier of (Polynom-Ring R)

proof

A4: dom the addF of (Polynom-Ring R) = [: the carrier of (Polynom-Ring R), the carrier of (Polynom-Ring R):] by FUNCT_2:def 1;
dom the addF of (Formal-Series R) = [: the carrier of (Formal-Series R), the carrier of (Formal-Series R):] by FUNCT_2:def 1;
then A5: (dom the addF of (Formal-Series R)) /\ [: the carrier of (Polynom-Ring R), the carrier of (Polynom-Ring R):] = [: the carrier of (Polynom-Ring R), the carrier of (Polynom-Ring R):] by XBOOLE_1:28, A2, ZFMISC_1:96;
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 (Formal-Series R) . o

proof

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 (Formal-Series R) . o )
assume o in dom the addF of (Polynom-Ring R) ; :: thesis: the addF of (Polynom-Ring R) . o = the addF of (Formal-Series R) . o
then consider o1, o2 being object such that
A6: ( o1 in the carrier of (Polynom-Ring R) & o2 in the carrier of (Polynom-Ring R) & o = [o1,o2] ) by ZFMISC_1:def 2;
reconsider x = o1, y = o2 as Element of the carrier of (Polynom-Ring R) by A6;
reconsider s1 = x, s2 = y as sequence of R by POLYNOM3:def 10;
reconsider x1 = x, y1 = y as Element of the carrier of (Formal-Series R) by A1;
the addF of (Polynom-Ring R) . [x,y] = x + y
.= s1 + s2 by POLYNOM3:def 10
.= x1 + y1 by POLYALG1:def 2
.= the addF of (Formal-Series R) . [x1,y1] ;
hence the addF of (Polynom-Ring R) . o = the addF of (Formal-Series R) . o by A6; :: thesis: verum

end;

hence the addF of (Polynom-Ring R) = the addF of (Formal-Series R) || the carrier of (Polynom-Ring R) by A4, A5, FUNCT_1:46; :: thesis: verum

end;

A7: the multF of (Polynom-Ring R) = the multF of (Formal-Series R) || the carrier of (Polynom-Ring R)

proof

A8: dom the multF of (Formal-Series R) = [: the carrier of (Formal-Series R), the carrier of (Formal-Series R):] by FUNCT_2:def 1;
A9: dom the multF of (Polynom-Ring R) = [: the carrier of (Polynom-Ring R), the carrier of (Polynom-Ring R):] by FUNCT_2:def 1;
A10: (dom the multF of (Formal-Series R)) /\ [: the carrier of (Polynom-Ring R), the carrier of (Polynom-Ring R):] = [: the carrier of (Polynom-Ring R), the carrier of (Polynom-Ring R):] by A8, XBOOLE_1:28, A2, ZFMISC_1:96;
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 (Formal-Series R) . o

proof

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 (Formal-Series R) . o )
assume o in dom the multF of (Polynom-Ring R) ; :: thesis: the multF of (Polynom-Ring R) . o = the multF of (Formal-Series R) . o
then consider o1, o2 being object such that
A11: ( o1 in the carrier of (Polynom-Ring R) & o2 in the carrier of (Polynom-Ring R) & o = [o1,o2] ) by ZFMISC_1:def 2;
reconsider x = o1, y = o2 as Element of the carrier of (Polynom-Ring R) by A11;
reconsider s1 = x, s2 = y as sequence of R by POLYNOM3:def 10;
reconsider x1 = x, y1 = y as Element of the carrier of (Formal-Series R) by A1;
the multF of (Polynom-Ring R) . [x,y] = x * y
.= s1 *' s2 by POLYNOM3:def 10
.= x1 * y1 by POLYALG1:def 2
.= the multF of (Formal-Series R) . [x1,y1] ;
hence the multF of (Polynom-Ring R) . o = the multF of (Formal-Series R) . o by A11; :: thesis: verum

end;

hence the multF of (Polynom-Ring R) = the multF of (Formal-Series R) || the carrier of (Polynom-Ring R) by A9, A10, FUNCT_1:46; :: thesis: verum

end;

A12: 0. (Polynom-Ring R) = 0_. R by POLYNOM3:def 10
.= 0. (Formal-Series R) by POLYALG1:def 2 ;
1. (Polynom-Ring R) = 1_. R by POLYNOM3:def 10
.= 1. (Formal-Series R) by POLYALG1:def 2 ;
hence Polynom-Ring R is Subring of Formal-Series R by A1, TARSKI:def 3, A3, A7, A12, C0SP1:def 3; :: thesis: verum