set M = { (p - (u *' s)) where u is Polynomial of L : 1 = 1 } ;
defpred S₁[ Nat] means ex t being Polynomial of L st
( t in { (p - (u *' s)) where u is Polynomial of L : 1 = 1 } & len t = $1 );
A2: len s <> 0 by A1, POLYNOM4:5;
then (len s) + 1 > 0 + 1 by XREAL_1:6;
then len s >= 1 by NAT_1:13;
then A3: (len s) - 1 >= 1 - 1 by XREAL_1:9;
s . ((len s) - 1) <> 0. L by A2, Lm6;
then A4: s . ((len s) -' 1) <> 0. L by A3, XREAL_0:def 2;
p = p + (0_. L) by POLYNOM3:28
.= p + (- (0_. L)) by Th9
.= p - ((0_. L) *' s) by POLYNOM4:2 ;
then p in { (p - (u *' s)) where u is Polynomial of L : 1 = 1 } ;
then ex t being Polynomial of L st
( t in { (p - (u *' s)) where u is Polynomial of L : 1 = 1 } & len t = len p ) ;
then A5: ex k being Nat st S₁[k] ;
consider k being Nat such that
A6: ( S₁[k] & ( for n being Nat st S₁[n] holds
k <= n ) ) from NAT_1:sch 5(A5);
consider f being Polynomial of L such that
A7: f in { (p - (u *' s)) where u is Polynomial of L : 1 = 1 } and
A8: len f = k by A6;
consider g being Polynomial of L such that
A9: f = p - (g *' s) and
1 = 1 by A7;
take g ; :: thesis:
A10: (g *' s) + (p - (g *' s)) = ((g *' s) + (- (g *' s))) + p by POLYNOM3:26
.= ((g *' s) - (g *' s)) + p
.= (0_. L) + p by POLYNOM3:29
.= p by POLYNOM3:28 ;

suppose A11: f = 0_. L ; :: thesis:

reconsider s9 = deg s as Nat by A1, Lm8;
A12: s9 >= 0 ;
deg f = - 1 by A11, Th20;
hence ex t being Polynomial of L st
( p = (g *' s) + t & deg t < deg s ) by A9, A10, A12; :: thesis:

end;

suppose f <> 0_. L ; :: thesis:

then len f <> 0 by POLYNOM4:5;
then (len f) + 1 > 0 + 1 by XREAL_1:6;
then len f >= 1 by NAT_1:13;
then A13: (len f) - 1 >= 1 - 1 by XREAL_1:9;
then reconsider k9 = (len f) - 1 as Element of NAT by INT_1:3;
A14: k = k9 + 1 by A8;
dom f = NAT by FUNCT_2:def 1;
then A15: k9 in dom f ;

now :: thesis:

assume deg f >= deg s ; :: thesis:
then reconsider degn = (deg f) - (deg s) as Element of NAT by INT_1:5;
set al = (f . ((len f) -' 1)) * ((s . ((len s) -' 1)) ");
set g1 = (0_. L) +* ({degn} --> ((f . ((len f) -' 1)) * ((s . ((len s) -' 1)) ")));

now :: thesis:

let u be object ; :: thesis:
assume u in {degn} ; :: thesis:
then u = degn by TARSKI:def 1;
hence u in NAT ; :: thesis:

end;

then A17: {degn} c= NAT by TARSKI:def 3;
A18: degn in {degn} by TARSKI:def 1;

A19: now :: thesis:

let x9 be object ; :: thesis:
assume x9 in NAT ; :: thesis:
then reconsider x = x9 as Element of NAT ;

per cases ;

suppose A20: x in dom ({degn} --> ((f . ((len f) -' 1)) * ((s . ((len s) -' 1)) "))) ; :: thesis:

then x = degn by TARSKI:def 1;
then ((0_. L) +* ({degn} --> ((f . ((len f) -' 1)) * ((s . ((len s) -' 1)) ")))) . x = ({degn} --> ((f . ((len f) -' 1)) * ((s . ((len s) -' 1)) "))) . degn by A20, FUNCT_4:13
.= (f . ((len f) -' 1)) * ((s . ((len s) -' 1)) ") by A18, FUNCOP_1:7 ;
hence ((0_. L) +* ({degn} --> ((f . ((len f) -' 1)) * ((s . ((len s) -' 1)) ")))) . x9 in the carrier of L ; :: thesis:

end;

suppose not x in dom ({degn} --> ((f . ((len f) -' 1)) * ((s . ((len s) -' 1)) "))) ; :: thesis:

then ((0_. L) +* ({degn} --> ((f . ((len f) -' 1)) * ((s . ((len s) -' 1)) ")))) . x = (0_. L) . x by FUNCT_4:11
.= 0. L ;
hence ((0_. L) +* ({degn} --> ((f . ((len f) -' 1)) * ((s . ((len s) -' 1)) ")))) . x9 in the carrier of L ; :: thesis:

end;

(dom (0_. L)) \/ (dom ({degn} --> ((f . ((len f) -' 1)) * ((s . ((len s) -' 1)) ")))) = NAT by A17, XBOOLE_1:12;
then dom ((0_. L) +* ({degn} --> ((f . ((len f) -' 1)) * ((s . ((len s) -' 1)) ")))) = NAT by FUNCT_4:def 1;
then reconsider g1 = (0_. L) +* ({degn} --> ((f . ((len f) -' 1)) * ((s . ((len s) -' 1)) "))) as sequence of L by A19, FUNCT_2:3;
A21: for j being Nat st j <> degn holds
g1 . j = 0. L

proof

let j be Nat; :: thesis:
A22: j in NAT by ORDINAL1:def 12;
assume j <> degn ; :: thesis:
then not j in dom ({degn} --> ((f . ((len f) -' 1)) * ((s . ((len s) -' 1)) "))) by TARSKI:def 1;
hence g1 . j = (0_. L) . j by FUNCT_4:11
.= 0. L by A22, FUNCOP_1:7 ;
:: thesis:

end;

A23: ex l being Nat st
for i being Nat st i >= l holds
g1 . i = 0. L

proof

take l = degn + 1; :: thesis:

now :: thesis:

let i be Nat; :: thesis:
assume i >= l ; :: thesis:
then i <> degn by NAT_1:13;
hence g1 . i = 0. L by A21; :: thesis:

end;

hence for i being Nat st i >= l holds
g1 . i = 0. L ; :: thesis:

end;

A24: degn in {degn} by TARSKI:def 1;
then degn in dom ({degn} --> ((f . ((len f) -' 1)) * ((s . ((len s) -' 1)) "))) ;
then A25: g1 . degn = ({degn} --> ((f . ((len f) -' 1)) * ((s . ((len s) -' 1)) "))) . degn by FUNCT_4:13
.= (f . ((len f) -' 1)) * ((s . ((len s) -' 1)) ") by A24, FUNCOP_1:7 ;
reconsider g1 = g1 as Polynomial of L by A23, ALGSEQ_1:def 1;
set s1 = p - ((g + g1) *' s);

now :: thesis:

A26: 1 <= degn + 1 by NAT_1:11;
let i be Nat; :: thesis:
A27: dom f = NAT by FUNCT_2:def 1;
assume A28: i >= k9 ; :: thesis:
then A29: i + 1 >= k by A14, XREAL_1:6;
degn + 1 = k - (deg s) by A8;
then A30: degn + 1 <= k by A3, XREAL_1:43;
then A31: (i + 1) - (degn + 1) is Element of NAT by A29, INT_1:5, XXREAL_0:2;
A32: i in NAT by ORDINAL1:def 12;
then consider sf being FinSequence of L such that
A33: len sf = i + 1 and
A34: (g1 *' s) . i = Sum sf and
A35: for m being Element of NAT st m in dom sf holds
sf . m = (g1 . (m -' 1)) * (s . ((i + 1) -' m)) by POLYNOM3:def 9;
A36: dom sf = Seg (len sf) by FINSEQ_1:def 3;
i + 1 >= degn + 1 by A30, A29, XXREAL_0:2;
then A37: degn + 1 in dom sf by A33, A36, A26;

A38: now :: thesis:

let m be Nat; :: thesis:
assume that
A39: m in dom sf and
A40: m <> degn + 1 ; :: thesis:
1 <= m by A36, A39, FINSEQ_1:1;
then m - 1 >= 1 - 1 by XREAL_1:9;
then m -' 1 = m - 1 by XREAL_0:def 2;
then m -' 1 <> degn by A40;
hence g1 . (m -' 1) = 0. L by A21; :: thesis:

end;

now :: thesis:

let i9 be Element of NAT ; :: thesis:
assume that
A41: i9 in dom sf and
A42: i9 <> degn + 1 ; :: thesis:
sf . i9 = (g1 . (i9 -' 1)) * (s . ((i + 1) -' i9)) by A35, A41
.= (0. L) * (s . ((i + 1) -' i9)) by A38, A41, A42
.= 0. L ;
hence sf /. i9 = 0. L by A41, PARTFUN1:def 6; :: thesis:

end;

then A43: Sum sf = sf /. (degn + 1) by A37, POLYNOM2:3
.= sf . (degn + 1) by A37, PARTFUN1:def 6
.= (g1 . ((degn + 1) -' 1)) * (s . ((i + 1) -' (degn + 1))) by A35, A37
.= ((f . ((len f) -' 1)) * ((s . ((len s) -' 1)) ")) * (s . ((i + 1) -' (degn + 1))) by A25, NAT_D:34 ;
A44: (p - ((g + g1) *' s)) - f = (p + (- ((g + g1) *' s))) + ((- p) + (- (- (g *' s)))) by A9, Th11
.= ((p + (- ((g + g1) *' s))) + (- p)) + (- (- (g *' s))) by POLYNOM3:26
.= ((p - p) + (- ((g + g1) *' s))) + (- (- (g *' s))) by POLYNOM3:26
.= ((0_. L) + (- ((g + g1) *' s))) + (- (- (g *' s))) by POLYNOM3:29
.= (- ((g + g1) *' s)) + (- (- (g *' s))) by POLYNOM3:28
.= ((- (g + g1)) *' s) + (- (- (g *' s))) by Th12
.= (((- g) + (- g1)) *' s) + (- (- (g *' s))) by Th11
.= (((- g) + (- g1)) *' s) + (g *' s) by Lm3
.= (((- g) *' s) + ((- g1) *' s)) + (g *' s) by POLYNOM3:32
.= ((- g1) *' s) + (((- g) *' s) + (g *' s)) by POLYNOM3:26
.= ((- g1) *' s) + ((g *' s) - (g *' s)) by Th12
.= ((- g1) *' s) + (0_. L) by POLYNOM3:29
.= (- g1) *' s by POLYNOM3:28
.= - (g1 *' s) by Th12 ;
A45: dom (g1 *' s) = NAT by FUNCT_2:def 1;
p - ((g + g1) *' s) = (p - ((g + g1) *' s)) + (0_. L) by POLYNOM3:28
.= (p - ((g + g1) *' s)) + (f - f) by POLYNOM3:29
.= ((p - ((g + g1) *' s)) + (- f)) + f by POLYNOM3:26
.= f - (g1 *' s) by A44 ;
then A46: (p - ((g + g1) *' s)) . i = (f . i) + ((- (g1 *' s)) . i) by NORMSP_1:def 2
.= (f . i) + (- ((g1 *' s) . i)) by BHSP_1:44
.= (f /. i) + (- ((g1 *' s) . i)) by A32, A27, PARTFUN1:def 6
.= (f /. i) + (- ((g1 *' s) /. i)) by A32, A45, PARTFUN1:def 6 ;
A47: i in NAT by ORDINAL1:def 12;

per cases by A28, XXREAL_0:1;

suppose A48: i > k9 ; :: thesis:

then reconsider e = i - k9 as Element of NAT by INT_1:5;
i - k9 > k9 - k9 by A48, XREAL_1:9;
then e + 1 > 0 + 1 by XREAL_1:6;
then e >= 1 by NAT_1:13;
then (i - k9) - 1 >= 1 - 1 by XREAL_1:9;
then A49: ((i - k9) - 1) + (len s) >= 0 + (len s) by XREAL_1:6;
i + 1 > k9 + 1 by A48, XREAL_1:6;
then i >= len f by NAT_1:13;
then f . i = 0. L by ALGSEQ_1:8;
then A50: f /. i = 0. L by A27, A47, PARTFUN1:def 6;
(i + 1) -' (degn + 1) = (i - k9) + ((len s) - 1) by A31, XREAL_0:def 2;
then s . ((i + 1) -' (degn + 1)) = 0. L by A49, ALGSEQ_1:8;
then Sum sf = 0. L by A43;
hence (p - ((g + g1) *' s)) . i = (0. L) + (- (0. L)) by A45, A46, A34, A47, A50, PARTFUN1:def 6
.= (0. L) + (0. L) by RLVECT_1:12
.= 0. L by RLVECT_1:def 4 ;
:: thesis:

end;

suppose A51: i = k9 ; :: thesis:

(i + 1) -' (degn + 1) = (i + 1) - (degn + 1) by A31, XREAL_0:def 2
.= (len s) -' 1 by A3, A51, XREAL_0:def 2 ;
then Sum sf = (f . ((len f) -' 1)) * (((s . ((len s) -' 1)) ") * (s . ((len s) -' 1))) by A43, GROUP_1:def 3
.= (f . ((len f) -' 1)) * (1_ L) by A4, VECTSP_1:def 10
.= f . ((len f) -' 1)
.= f . ((len f) - 1) by A13, XREAL_0:def 2
.= f /. ((len f) - 1) by A15, PARTFUN1:def 6 ;
hence (p - ((g + g1) *' s)) . i = (f /. ((len f) - 1)) + (- (f /. ((len f) - 1))) by A45, A46, A34, A51, PARTFUN1:def 6
.= 0. L by RLVECT_1:5 ;
:: thesis:

end;

then k9 is_at_least_length_of p - ((g + g1) *' s) by ALGSEQ_1:def 2;
then len (p - ((g + g1) *' s)) <= k9 by ALGSEQ_1:def 3;
then A52: len (p - ((g + g1) *' s)) < k by A14, NAT_1:13;
p - ((g + g1) *' s) in { (p - (u *' s)) where u is Polynomial of L : 1 = 1 } ;
hence contradiction by A6, A52; :: thesis:

end;

hence ex t being Polynomial of L st
( p = (g *' s) + t & deg t < deg s ) by A9, A10; :: thesis:

end;