let L be non empty right_complementable add-associative right_zeroed addLoopStr ; :: thesis: for p being Polynomial of L st len p <> 0 holds
ex q being Polynomial of L st
( len q < len p & p = q + (Leading-Monomial p) & ( for n being Element of NAT st n < (len p) - 1 holds
q . n = p . n ) )
let p be Polynomial of L; :: thesis: ( len p <> 0 implies ex q being Polynomial of L st
( len q < len p & p = q + (Leading-Monomial p) & ( for n being Element of NAT st n < (len p) - 1 holds
q . n = p . n ) ) )
deffunc H₁( Element of NAT ) -> Element of the carrier of L = p . $1;
consider q being Polynomial of L such that
A1: len q <= (len p) -' 1 and
A2: for n being Element of NAT st n < (len p) -' 1 holds
q . n = H₁(n) from POLYNOM3:sch 2();
assume len p <> 0 ; :: thesis: ex q being Polynomial of L st
( len q < len p & p = q + (Leading-Monomial p) & ( for n being Element of NAT st n < (len p) - 1 holds
q . n = p . n ) )
then A3: len p >= 0 + 1 by NAT_1:13;
take q ; :: thesis: ( len q < len p & p = q + (Leading-Monomial p) & ( for n being Element of NAT st n < (len p) - 1 holds
q . n = p . n ) )
len q < ((len p) -' 1) + 1 by A1, NAT_1:13;
hence A4: len q < len p by A3, XREAL_1:235; :: thesis: ( p = q + (Leading-Monomial p) & ( for n being Element of NAT st n < (len p) - 1 holds
q . n = p . n ) )

A5: now :: thesis: for k being Nat st k < len p holds
(q + (Leading-Monomial p)) . k = p . k

let k be Nat; :: thesis: ( k < len p implies (q + (Leading-Monomial p)) . b₁ = p . b₁ )
A6: k in NAT by ORDINAL1:def 12;
assume k < len p ; :: thesis: (q + (Leading-Monomial p)) . b₁ = p . b₁
then k + 1 <= len p by NAT_1:13;
then A7: (k + 1) - 1 <= (len p) - 1 by XREAL_1:9;

per cases ( k < (len p) - 1 or k = (len p) - 1 ) by A7, XXREAL_0:1;

suppose k < (len p) - 1 ; :: thesis: (q + (Leading-Monomial p)) . b₁ = p . b₁

then A8: k < (len p) -' 1 by XREAL_0:def 2;
thus (q + (Leading-Monomial p)) . k = (q . k) + ((Leading-Monomial p) . k) by NORMSP_1:def 2
.= (p . k) + ((Leading-Monomial p) . k) by A2, A6, A8
.= (p . k) + (0. L) by A6, A8, Def1
.= p . k by RLVECT_1:def 4 ; :: thesis: verum

end;

suppose k = (len p) - 1 ; :: thesis: (q + (Leading-Monomial p)) . b₁ = p . b₁

then A9: k = (len p) -' 1 by XREAL_0:def 2;
thus (q + (Leading-Monomial p)) . k = (q . k) + ((Leading-Monomial p) . k) by NORMSP_1:def 2
.= (0. L) + ((Leading-Monomial p) . k) by A1, A9, ALGSEQ_1:8
.= (Leading-Monomial p) . k by RLVECT_1:4
.= p . k by A9, Def1 ; :: thesis: verum

end;

end;

end;

A10: len (Leading-Monomial p) = len p by Th15;
then len (q + (Leading-Monomial p)) = max ((len q),(len (Leading-Monomial p))) by A4, Th7
.= len p by A4, A10, XXREAL_0:def 10 ;
hence p = q + (Leading-Monomial p) by A5, ALGSEQ_1:12; :: thesis: for n being Element of NAT st n < (len p) - 1 holds
q . n = p . n
let n be Element of NAT ; :: thesis: ( n < (len p) - 1 implies q . n = p . n )
assume n < (len p) - 1 ; :: thesis: q . n = p . n
then n < (len p) -' 1 by XREAL_0:def 2;
hence q . n = p . n by A2; :: thesis: verum