let R be comRing; :: thesis: for S being Ring st S is Subring of R holds
for p, q being Polynomial of R st p is Polynomial of S holds
for a being Element of R
for b being Element of S st a = b & b is left_invertible & p = q *' (rpoly (1,a)) holds
q is Polynomial of S
let S be Ring; :: thesis: ( S is Subring of R implies for p, q being Polynomial of R st p is Polynomial of S holds
for a being Element of R
for b being Element of S st a = b & b is left_invertible & p = q *' (rpoly (1,a)) holds
q is Polynomial of S )
assume S is Subring of R ; :: thesis: for p, q being Polynomial of R st p is Polynomial of S holds
for a being Element of R
for b being Element of S st a = b & b is left_invertible & p = q *' (rpoly (1,a)) holds
q is Polynomial of S
then reconsider S1 = S as Subring of R ;
let p, q be Polynomial of R; :: thesis: ( p is Polynomial of S implies for a being Element of R
for b being Element of S st a = b & b is left_invertible & p = q *' (rpoly (1,a)) holds
q is Polynomial of S )
assume A1: p is Polynomial of S ; :: thesis: for a being Element of R
for b being Element of S st a = b & b is left_invertible & p = q *' (rpoly (1,a)) holds
q is Polynomial of S
let a be Element of R; :: thesis: for b being Element of S st a = b & b is left_invertible & p = q *' (rpoly (1,a)) holds
q is Polynomial of S
let c be Element of S; :: thesis: ( a = c & c is left_invertible & p = q *' (rpoly (1,a)) implies q is Polynomial of S )
assume A2: ( a = c & c is left_invertible & p = q *' (rpoly (1,a)) ) ; :: thesis: q is Polynomial of S
reconsider b = c as Element of S1 ;
consider ys being Element of S1 such that
A3: ys * b = 1. S1 by A2, ALGSTR_0:def 27;
( ys in the carrier of S1 & the carrier of S1 c= the carrier of R ) by C0SP1:def 3;
then reconsider y = ys as Element of R ;
A4: a * y = b * ys by A2, FIELD_6:16;
then A5: a * y = 1. R by A3, C0SP1:def 3;
set RP = rpoly (1,a);
defpred S₁[ Nat] means q . $1 in the carrier of S1;
A6: ( (rpoly (1,a)) . 0 = - ((power R) . (a,1)) & - ((power R) . (a,1)) = - a & (rpoly (1,a)) . 1 = 1_ R ) by HURWITZ:25, GROUP_1:50;
A7: ( dom p = NAT & rng p c= the carrier of S ) by A1, RELAT_1:def 19, FUNCT_2:def 1;
A8: S₁[ 0 ]

proof

consider r being FinSequence of the carrier of R such that
A9: ( len r = 0 + 1 & (q *' (rpoly (1,a))) . 0 = Sum r ) and
A10: for k being Element of NAT st k in dom r holds
r . k = (q . (k -' 1)) * ((rpoly (1,a)) . ((0 + 1) -' k)) by POLYNOM3:def 9;
A11: r . 1 = (q . (1 -' 1)) * ((rpoly (1,a)) . ((0 + 1) -' 1)) by A9, FINSEQ_3:25, A10;
p . 0 in rng p by A7, FUNCT_1:def 3;
then reconsider p0 = p . 0 as Element of S1 by A7;
r = <*((q . 0) * ((rpoly (1,a)) . 0))*> by A9, A11, FINSEQ_1:40;
then p . 0 = (q . 0) * (- a) by A2, A9, A6, RLVECT_1:44
.= - ((q . 0) * a) by VECTSP_1:8 ;
then A12: (- (p . 0)) * y = (q . 0) * (a * y) by GROUP_1:def 3;
- (p . 0) = - p0 by FIELD_6:17;
then (- (p . 0)) * y = (- p0) * ys by FIELD_6:16;
hence S₁[ 0 ] by A5, A12; :: thesis: verum

end;

A13: for i being Nat st S₁[i] holds
S₁[i + 1]

proof

let i be Nat; :: thesis: ( S₁[i] implies S₁[i + 1] )
assume A14: S₁[i] ; :: thesis: S₁[i + 1]
consider r being FinSequence of the carrier of R such that
A15: ( len r = (i + 1) + 1 & (q *' (rpoly (1,a))) . (i + 1) = Sum r ) and
A16: for k being Element of NAT st k in dom r holds
r . k = (q . (k -' 1)) * ((rpoly (1,a)) . (((i + 1) + 1) -' k)) by POLYNOM3:def 9;
len r = i + 2 by A15;
then consider r1, r2 being FinSequence of the carrier of R such that
A17: ( len r1 = i & len r2 = 2 & r = r1 ^ r2 ) by FINSEQ_2:23;
for k being Element of NAT st k in dom r1 holds
r1 . k = 0. R

proof

let k be Element of NAT ; :: thesis: ( k in dom r1 implies r1 . k = 0. R )
assume A18: k in dom r1 ; :: thesis: r1 . k = 0. R
( dom r1 c= dom r & r . k = r1 . k ) by A18, A17, FINSEQ_1:26, FINSEQ_1:def 7;
then A19: r1 . k = (q . (k -' 1)) * ((rpoly (1,a)) . (((i + 1) + 1) -' k)) by A18, A16;
A20: k <= i by A17, A18, FINSEQ_3:25;
then k + 0 <= i + 2 by XREAL_1:7;
then A21: (i + 2) -' k = (i + 2) - k by XREAL_1:233;
k - k <= i - k by A20, XREAL_1:9;
then 0 + 2 <= (i - k) + 2 by XREAL_1:6;
then ( (i + 2) -' k <> 0 & (i + 2) -' k <> 1 ) by A21;
then (rpoly (1,a)) . (((i + 1) + 1) -' k) = 0. R by HURWITZ:26;
hence r1 . k = 0. R by A19; :: thesis: verum

end;

then Sum r1 = 0. R by POLYNOM3:1;
then A22: Sum r = (0. R) + (Sum r2) by A17, RLVECT_1:41;
p . (i + 1) in rng p by A7, FUNCT_1:def 3;
then reconsider qi = q . i, pi1 = p . (i + 1) as Element of S1 by A7, A14;
A23: ( (i + 1) -' 1 = (i + 1) - 1 & (i + 1) - 1 = i ) ;
A24: ( ((i + 1) + 1) -' (i + 1) = ((i + 1) + 1) - (i + 1) & ((i + 1) + 1) - (i + 1) = 1 ) ;
1 <= (i + 1) + 1 by NAT_1:11;
then A25: ( (i + 2) -' 1 = (i + 2) - 1 & (i + 2) - 1 = i + 1 ) ;
A26: ((i + 1) + 1) -' (i + 2) = 0 by XREAL_1:232;
( 1 in dom r2 & 2 in dom r2 ) by A17, FINSEQ_3:25;
then ( r2 . 1 = r . (i + 1) & i + 1 in dom r & r2 . 2 = r . (i + 2) & i + 2 in dom r ) by A17, FINSEQ_1:def 7, FINSEQ_1:28;
then ( r2 . 1 = (q . i) * ((rpoly (1,a)) . 1) & r2 . 2 = (q . (i + 1)) * ((rpoly (1,a)) . 0) ) by A16, A23, A24, A25, A26;
then r2 = <*((q . i) * ((rpoly (1,a)) . 1)),((q . (i + 1)) * ((rpoly (1,a)) . 0))*> by A17, FINSEQ_1:44;
then Sum r2 = (Sum <*((q . i) * ((rpoly (1,a)) . 1))*>) + (Sum <*((q . (i + 1)) * ((rpoly (1,a)) . 0))*>) by RLVECT_1:41;
then Sum r2 = (Sum <*((q . i) * ((rpoly (1,a)) . 1))*>) + ((q . (i + 1)) * ((rpoly (1,a)) . 0)) by RLVECT_1:44;
then (p . (i + 1)) * y = ((q . i) + ((q . (i + 1)) * (- a))) * y by A2, A6, A15, A22, RLVECT_1:44;
then A27: ((p . (i + 1)) * y) + (- ((q . i) * y)) = (((q . i) * y) + (((q . (i + 1)) * (- a)) * y)) + (- ((q . i) * y)) by VECTSP_1:def 2
.= (((q . (i + 1)) * (- a)) * y) + (((q . i) * y) + (- ((q . i) * y))) by RLVECT_1:def 3
.= (((q . (i + 1)) * (- a)) * y) + (0. R) by RLVECT_1:5
.= (q . (i + 1)) * ((- a) * y) by GROUP_1:def 3
.= (q . (i + 1)) * (- (a * y)) by VECTSP_1:8
.= (q . (i + 1)) * (- (1. R)) by A4, A3, C0SP1:def 3
.= - ((q . (i + 1)) * (1. R)) by VECTSP_1:8
.= - (q . (i + 1)) ;
(q . i) * y = qi * ys by FIELD_6:16;
then A28: - ((q . i) * y) = - (qi * ys) by FIELD_6:17;
(p . (i + 1)) * y = pi1 * ys by FIELD_6:16;
then ((p . (i + 1)) * y) + (- ((q . i) * y)) = (pi1 * ys) + (- (qi * ys)) by A28, FIELD_6:15;
then - (((p . (i + 1)) * y) + (- ((q . i) * y))) = - ((pi1 * ys) + (- (qi * ys))) by FIELD_6:17;
hence S₁[i + 1] by A27; :: thesis: verum

end;

A29: for i being Nat holds S₁[i] from NAT_1:sch 2(A8, A13);
A30: dom q = NAT by FUNCT_2:def 1;
rng q c= the carrier of S

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng q or y in the carrier of S )
assume y in rng q ; :: thesis: y in the carrier of S
then consider x being object such that
A31: ( x in dom q & q . x = y ) by FUNCT_1:def 3;
reconsider x = x as Nat by A31;
thus y in the carrier of S by A31, A29; :: thesis: verum

end;

then reconsider qs = q as sequence of S by A30, FUNCT_2:2;
qs is finite-Support

proof

0. R = 0. S1 by C0SP1:def 3;
then ex n being Nat st
for i being Nat st i >= n holds
qs . i = 0. S1 by ALGSEQ_1:def 1;
hence qs is finite-Support by ALGSEQ_1:def 1; :: thesis: verum

end;

hence q is Polynomial of S ; :: thesis: verum