let R be non degenerated comRing; :: thesis: for S being comRingExtension of R
for n being Ordinal holds Polynom-Ring (n,S) is comRingExtension of Polynom-Ring (n,R)
let S be comRingExtension of R; :: thesis: for n being Ordinal holds Polynom-Ring (n,S) is comRingExtension of Polynom-Ring (n,R)
let n be Ordinal; :: thesis: Polynom-Ring (n,S) is comRingExtension of Polynom-Ring (n,R)
A1: R is Subring of S by FIELD_4:def 1;
then A2: the carrier of R c= the carrier of S by C0SP1:def 3;
A3: 0. S = 0. R by A1, C0SP1:def 3;
X1: for p being Polynomial of n,R holds p is Polynomial of n,S

proof

let p be Polynomial of n,R; :: thesis: p is Polynomial of n,S
rng p c= the carrier of R by RELAT_1:def 19;
then rng p c= the carrier of S by A2;
then reconsider p1 = p as Series of n,S by FUNCT_2:6;

now :: thesis: for o being object st o in Support p1 holds
o in Support p

let o be object ; :: thesis: ( o in Support p1 implies o in Support p )
assume A5: o in Support p1 ; :: thesis: o in Support p
then reconsider b = o as Element of Bags n ;
A6: 0. R <> p . b by A3, A5, POLYNOM1:def 3;
dom p = Bags n by FUNCT_2:def 1;
hence o in Support p by A6, POLYNOM1:def 3; :: thesis: verum

end;

then Support p1 c= Support p ;
hence p is Polynomial of n,S by POLYNOM1:def 5; :: thesis: verum

end;

X2: the carrier of (Polynom-Ring (n,R)) c= the carrier of (Polynom-Ring (n,S))

proof

now :: thesis: for o being object st o in the carrier of (Polynom-Ring (n,R)) holds
o in the carrier of (Polynom-Ring (n,S))

let o be object ; :: thesis: ( o in the carrier of (Polynom-Ring (n,R)) implies o in the carrier of (Polynom-Ring (n,S)) )
assume o in the carrier of (Polynom-Ring (n,R)) ; :: thesis: o in the carrier of (Polynom-Ring (n,S))
then o is Polynomial of n,R by POLYNOM1:def 11;
then o is Polynomial of n,S by X1;
hence o in the carrier of (Polynom-Ring (n,S)) by POLYNOM1:def 11; :: thesis: verum

end;

hence the carrier of (Polynom-Ring (n,R)) c= the carrier of (Polynom-Ring (n,S)) ; :: thesis: verum

end;

X3: 0. (Polynom-Ring (n,R)) = 0_ (n,R) by POLYNOM1:def 11
.= (Bags n) --> (0. R) by POLYNOM1:def 8
.= (Bags n) --> (0. S) by A1, C0SP1:def 3
.= 0_ (n,S) by POLYNOM1:def 8
.= 0. (Polynom-Ring (n,S)) by POLYNOM1:def 11 ;
H: 0_ (n,R) = (Bags n) --> (0. R) by POLYNOM1:def 8
.= (Bags n) --> (0. S) by A1, C0SP1:def 3
.= 0_ (n,S) by POLYNOM1:def 8 ;
X4: 1. (Polynom-Ring (n,R)) = 1_ (n,R) by POLYNOM1:def 11
.= (0_ (n,R)) +* ((EmptyBag n),(1. R)) by POLYNOM1:def 9
.= (0_ (n,S)) +* ((EmptyBag n),(1. S)) by H, A1, C0SP1:def 3
.= 1_ (n,S) by POLYNOM1:def 9
.= 1. (Polynom-Ring (n,S)) by POLYNOM1:def 11 ;
X5: for p, q being Polynomial of n,R
for p1, q1 being Polynomial of n,S st p = p1 & q = q1 holds
p + q = p1 + q1

proof

let p, q be Polynomial of n,R; :: thesis: for p1, q1 being Polynomial of n,S st p = p1 & q = q1 holds
p + q = p1 + q1
let p1, q2 be Polynomial of n,S; :: thesis: ( p = p1 & q = q2 implies p + q = p1 + q2 )
assume A1: ( p = p1 & q = q2 ) ; :: thesis: p + q = p1 + q2
A2: R is Subring of S by FIELD_4:def 1;

now :: thesis: for b being Element of Bags n holds (p + q) . b = (p1 + q2) . b

let b be Element of Bags n; :: thesis: (p + q) . b = (p1 + q2) . b
( p . b = p1 . b & q . b = q2 . b ) by A1;
then A3: [(p1 . b),(q2 . b)] in [: the carrier of R, the carrier of R:] by ZFMISC_1:def 2;
thus (p + q) . b = (p . b) + (q . b) by POLYNOM1:15
.= ( the addF of S || the carrier of R) . ((p1 . b),(q2 . b)) by A1, A2, C0SP1:def 3
.= (p1 . b) + (q2 . b) by A3, FUNCT_1:49
.= (p1 + q2) . b by POLYNOM1:15 ; :: thesis: verum

end;

hence p + q = p1 + q2 ; :: thesis: verum

end;

X6: the addF of (Polynom-Ring (n,R)) = the addF of (Polynom-Ring (n,S)) || the carrier of (Polynom-Ring (n,R))

proof

set aR = the addF of (Polynom-Ring (n,R));
set aS = the addF of (Polynom-Ring (n,S)) || the carrier of (Polynom-Ring (n,R));
set cR = the carrier of (Polynom-Ring (n,R));
set cS = the carrier of (Polynom-Ring (n,S));
A2: dom ( the addF of (Polynom-Ring (n,S)) || the carrier of (Polynom-Ring (n,R))) = (dom the addF of (Polynom-Ring (n,S))) /\ [: the carrier of (Polynom-Ring (n,R)), the carrier of (Polynom-Ring (n,R)):] by RELAT_1:61
.= [: the carrier of (Polynom-Ring (n,S)), the carrier of (Polynom-Ring (n,S)):] /\ [: the carrier of (Polynom-Ring (n,R)), the carrier of (Polynom-Ring (n,R)):] by FUNCT_2:def 1
.= [: the carrier of (Polynom-Ring (n,R)), the carrier of (Polynom-Ring (n,R)):] by X2, ZFMISC_1:96, XBOOLE_1:28
.= dom the addF of (Polynom-Ring (n,R)) by FUNCT_2:def 1 ;

now :: thesis: for o being object st o in dom the addF of (Polynom-Ring (n,R)) holds
the addF of (Polynom-Ring (n,R)) . o = ( the addF of (Polynom-Ring (n,S)) || the carrier of (Polynom-Ring (n,R))) . o

let o be object ; :: thesis: ( o in dom the addF of (Polynom-Ring (n,R)) implies the addF of (Polynom-Ring (n,R)) . o = ( the addF of (Polynom-Ring (n,S)) || the carrier of (Polynom-Ring (n,R))) . o )
assume A3: o in dom the addF of (Polynom-Ring (n,R)) ; :: thesis: the addF of (Polynom-Ring (n,R)) . o = ( the addF of (Polynom-Ring (n,S)) || the carrier of (Polynom-Ring (n,R))) . o
then consider p, q being object such that
A4: ( p in the carrier of (Polynom-Ring (n,R)) & q in the carrier of (Polynom-Ring (n,R)) & o = [p,q] ) by ZFMISC_1:def 2;
reconsider p = p, q = q as Element of the carrier of (Polynom-Ring (n,R)) by A4;
reconsider p1 = p, q1 = q as Element of the carrier of (Polynom-Ring (n,S)) by X2;
reconsider p2 = p, q2 = q as Polynomial of n,R by POLYNOM1:def 11;
reconsider p3 = p1, q3 = q1 as Polynomial of n,S by POLYNOM1:def 11;
thus the addF of (Polynom-Ring (n,R)) . o = p + q by A4
.= p2 + q2 by POLYNOM1:def 11
.= p3 + q3 by X5
.= p1 + q1 by POLYNOM1:def 11
.= ( the addF of (Polynom-Ring (n,S)) || the carrier of (Polynom-Ring (n,R))) . o by A2, A3, A4, FUNCT_1:47 ; :: thesis: verum

end;

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

end;

X7: for p, q being Polynomial of n,R
for p1, q1 being Polynomial of n,S st p = p1 & q = q1 holds
p *' q = p1 *' q1

proof

let p, q be Polynomial of n,R; :: thesis: for p1, q1 being Polynomial of n,S st p = p1 & q = q1 holds
p *' q = p1 *' q1
let p1, qq be Polynomial of n,S; :: thesis: ( p = p1 & q = qq implies p *' q = p1 *' qq )
assume A1: ( p = p1 & q = qq ) ; :: thesis: p *' q = p1 *' qq
A2: R is Subring of S by FIELD_4:def 1;

now :: thesis: for b being bag of n holds (p *' q) . b = (p1 *' qq) . b

let b be bag of n; :: thesis: (p *' q) . b = (p1 *' qq) . b
consider r being FinSequence of the carrier of R such that
A3: ( (p *' q) . b = Sum r & len r = len (decomp b) & ( for k being Element of NAT st k in dom r holds
ex b1, b2 being bag of n st
( (decomp b) /. k = <*b1,b2*> & r /. k = (p . b1) * (q . b2) ) ) ) by POLYNOM1:def 10;
consider r1 being FinSequence of the carrier of S such that
A4: ( (p1 *' qq) . b = Sum r1 & len r1 = len (decomp b) & ( for k being Element of NAT st k in dom r1 holds
ex b1, b2 being bag of n st
( (decomp b) /. k = <*b1,b2*> & r1 /. k = (p1 . b1) * (qq . b2) ) ) ) by POLYNOM1:def 10;
A5: dom r1 = Seg (len r) by A3, A4, FINSEQ_1:def 3
.= dom r by FINSEQ_1:def 3 ;

now :: thesis: for m being Nat st m in dom r holds
r . m = r1 . m

let m be Nat; :: thesis: ( m in dom r implies r . m = r1 . m )
assume A6: m in dom r ; :: thesis: r . m = r1 . m
then consider b1, b2 being bag of n such that
B1: ( (decomp b) /. m = <*b1,b2*> & r /. m = (p . b1) * (q . b2) ) by A3;
consider b11, b22 being bag of n such that
B2: ( (decomp b) /. m = <*b11,b22*> & r1 /. m = (p1 . b11) * (qq . b22) ) by A5, A6, A4;
B3: b11 = <*b1,b2*> . 1 by B1, B2, FINSEQ_1:44
.= b1 ;
B4: b22 = <*b1,b2*> . 2 by B1, B2, FINSEQ_1:44
.= b2 ;
( p . b1 = p1 . b1 & q . b2 = qq . b2 ) by A1;
then A7: [(p1 . b1),(qq . b2)] in [: the carrier of R, the carrier of R:] by ZFMISC_1:def 2;
thus r . m = (p . b1) * (q . b2) by B1, A6, PARTFUN1:def 6
.= ( the multF of S || the carrier of R) . ((p1 . b1),(qq . b2)) by A1, A2, C0SP1:def 3
.= (p1 . b11) * (qq . b22) by B3, B4, A7, FUNCT_1:49
.= r1 . m by B2, A6, A5, PARTFUN1:def 6 ; :: thesis: verum

end;

then r = r1 by A5;
hence (p *' q) . b = (p1 *' qq) . b by A4, A3, A2, FIELD_4:2; :: thesis: verum

end;

hence p *' q = p1 *' qq ; :: thesis: verum

end;

X8: the multF of (Polynom-Ring (n,R)) = the multF of (Polynom-Ring (n,S)) || the carrier of (Polynom-Ring (n,R))

proof

set mR = the multF of (Polynom-Ring (n,R));
set mS = the multF of (Polynom-Ring (n,S)) || the carrier of (Polynom-Ring (n,R));
set cR = the carrier of (Polynom-Ring (n,R));
set cS = the carrier of (Polynom-Ring (n,S));
A2: dom ( the multF of (Polynom-Ring (n,S)) || the carrier of (Polynom-Ring (n,R))) = (dom the multF of (Polynom-Ring (n,S))) /\ [: the carrier of (Polynom-Ring (n,R)), the carrier of (Polynom-Ring (n,R)):] by RELAT_1:61
.= [: the carrier of (Polynom-Ring (n,S)), the carrier of (Polynom-Ring (n,S)):] /\ [: the carrier of (Polynom-Ring (n,R)), the carrier of (Polynom-Ring (n,R)):] by FUNCT_2:def 1
.= [: the carrier of (Polynom-Ring (n,R)), the carrier of (Polynom-Ring (n,R)):] by X2, ZFMISC_1:96, XBOOLE_1:28
.= dom the multF of (Polynom-Ring (n,R)) by FUNCT_2:def 1 ;

now :: thesis: for o being object st o in dom the multF of (Polynom-Ring (n,R)) holds
the multF of (Polynom-Ring (n,R)) . o = ( the multF of (Polynom-Ring (n,S)) || the carrier of (Polynom-Ring (n,R))) . o

let o be object ; :: thesis: ( o in dom the multF of (Polynom-Ring (n,R)) implies the multF of (Polynom-Ring (n,R)) . o = ( the multF of (Polynom-Ring (n,S)) || the carrier of (Polynom-Ring (n,R))) . o )
assume A3: o in dom the multF of (Polynom-Ring (n,R)) ; :: thesis: the multF of (Polynom-Ring (n,R)) . o = ( the multF of (Polynom-Ring (n,S)) || the carrier of (Polynom-Ring (n,R))) . o
then consider p, q being object such that
A4: ( p in the carrier of (Polynom-Ring (n,R)) & q in the carrier of (Polynom-Ring (n,R)) & o = [p,q] ) by ZFMISC_1:def 2;
reconsider p = p, q = q as Element of the carrier of (Polynom-Ring (n,R)) by A4;
reconsider p1 = p, q1 = q as Element of the carrier of (Polynom-Ring (n,S)) by X2;
reconsider p2 = p, q2 = q as Polynomial of n,R by POLYNOM1:def 11;
reconsider p3 = p1, q3 = q1 as Polynomial of n,S by POLYNOM1:def 11;
thus the multF of (Polynom-Ring (n,R)) . o = p * q by A4
.= p2 *' q2 by POLYNOM1:def 11
.= p3 *' q3 by X7
.= p1 * q1 by POLYNOM1:def 11
.= ( the multF of (Polynom-Ring (n,S)) || the carrier of (Polynom-Ring (n,R))) . o by A2, A3, A4, FUNCT_1:47 ; :: thesis: verum

end;

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

end;

Polynom-Ring (n,R) is Subring of Polynom-Ring (n,S) by X2, X3, X4, X6, X8, C0SP1:def 3;
hence Polynom-Ring (n,S) is comRingExtension of Polynom-Ring (n,R) by FIELD_4:def 1; :: thesis: verum